STLCG

Conjunto de herramientas en JAX para la robustez diferenciable de Signal Temporal Logic

Licencia

BSD-2-Clause

Resumen

STLCG (distribuido como la biblioteca de JAX stljax) es un conjunto de herramientas para calcular la robustez de fórmulas de Signal Temporal Logic (STL) mediante grafos de cómputo. STL es un lenguaje formal para expresar requisitos espaciotemporales como «entrar en la región objetivo en menos de 10 segundos y permanecer en ella durante 5 segundos», y su medida de robustez cuantifica con qué intensidad una señal satisface o viola una especificación. stljax reimplementa en JAX el stlcg original de 2019 del Stanford ASL, escrito en PyTorch, reemplazando la evaluación recurrente secuencial por una formulación basada en enmascaramiento totalmente paralelizable que se ejecuta hasta ~1000x más rápido en GPU. Dado que todo el flujo es diferenciable, las especificaciones STL pueden incrustarse directamente en la optimización de trayectorias basada en gradientes, en el modelado de recompensas de aprendizaje por refuerzo y en la minería de parámetros. Publicado en IEEE Robotics and Automation Letters (RA-L) 2025; instalable con pip como stljax.

stljax permite a los ingenieros de robótica convertir especificaciones de misión en lógica temporal legibles por humanos en términos de objetivo y restricción diferenciables. Construyes fórmulas STL a partir de Expressions y Predicates, evalúas su robustez sobre una señal o trayectoria y —dado que todo está implementado en JAX— obtienes evaluación por lotes mediante vmap y gradientes exactos para usarlos dentro de optimizadores y bucles de aprendizaje. La decisión de diseño clave es una reformulación basada en enmascaramiento de los operadores temporales (Always/Eventually/Until) que paraleliza lo que antes era un cálculo recurrente secuencial, ofreciendo aceleraciones de varios órdenes de magnitud y distribuyendo además correctamente los gradientes a través de todas las operaciones min/max.

Por qué importa

Signal Temporal Logic ofrece a la robótica una forma precisa y legible por humanos de especificar requisitos de misión temporales y espaciales, pero durante años su cálculo de robustez fue secuencial, lento y difícil de diferenciar, lo que mantuvo a STL fuera de los flujos modernos de aprendizaje y optimización. stljax elimina esa barrera: una implementación paralelizada y nativa de diferenciación automática hace que STL sea lo bastante rápido para el control en tiempo real y el entrenamiento con grandes lotes, de modo que las especificaciones puedan actuar directamente como objetivos del planificador, recompensas de RL o señales de verificación.

Qué problema resuelve

Las herramientas previas de robustez STL dependían de un cálculo recurrente secuencial que era lento y difícil de diferenciar, lo que limitaba el uso de especificaciones formales de lógica temporal dentro de la optimización de trayectorias y el aprendizaje basados en gradientes.

Puntos clave

Robustez STL paralela basada en enmascaramiento, hasta ~1000x más rápida que los métodos recurrentes en GPU
Nativa de JAX: agrupación por lotes con vmap y gradientes exactos, con distribución correcta del gradiente a través de min/max
APIs de Expression y Predicate para construir fórmulas Always/Eventually/Until
Especificaciones diferenciables utilizables como objetivos/restricciones en la optimización de trayectorias y en RL
Instalable con pip (stljax); RA-L 2025; sucesor del stlcg en PyTorch del Stanford ASL

Para quién es

Investigadores de planificación de movimiento y optimización de trayectorias
Investigadores de control y métodos formales
Diseñadores de recompensas de aprendizaje por refuerzo
Ingenieros de autonomía segura y verificación

Limitaciones

Requiere familiaridad con Signal Temporal Logic para redactar especificaciones útiles
El suavizado/aproximación de la función de robustez introduce compromisos de precisión/gradiente
Dependencia de JAX y su cadena de herramientas
Una biblioteca de evaluación de especificaciones: no incluye un planificador ni un controlador en sí misma