STLCG

Boîte à outils JAX pour la robustesse différentiable de la logique temporelle de signaux

Licence

BSD-2-Clause

Aperçu

STLCG (distribué sous la forme de la bibliothèque JAX stljax) est une boîte à outils permettant de calculer la robustesse de formules de la logique temporelle de signaux (Signal Temporal Logic, STL) à l'aide de graphes de calcul. La STL est un langage formel permettant d'exprimer des exigences spatio-temporelles telles que « entrer dans la région cible en moins de 10 secondes et y rester pendant 5 secondes », et sa mesure de robustesse quantifie à quel point un signal satisfait ou viole une spécification. stljax réimplémente en JAX le stlcg PyTorch original du Stanford ASL de 2019, en remplaçant l'évaluation récurrente séquentielle par une formulation entièrement parallélisable fondée sur le masquage, qui s'exécute jusqu'à environ 1000 fois plus vite sur GPU. Comme l'ensemble du pipeline est différentiable, les spécifications STL peuvent être intégrées directement dans l'optimisation de trajectoire par gradient, le façonnage de récompense en apprentissage par renforcement et l'exploration de paramètres. Publié dans IEEE Robotics and Automation Letters (RA-L) 2025 ; installable via pip sous le nom stljax.

stljax permet aux ingénieurs en robotique de transformer des spécifications de mission en logique temporelle, lisibles par l'humain, en termes d'objectif et de contrainte différentiables. Vous construisez des formules STL à partir d'Expressions et de Prédicats, vous évaluez leur robustesse sur un signal ou une trajectoire et — parce que tout est implémenté en JAX — vous obtenez une évaluation par lots via vmap ainsi que des gradients exacts utilisables au sein d'optimiseurs et de boucles d'apprentissage. Le choix de conception clé est une reformulation fondée sur le masquage des opérateurs temporels (Always/Eventually/Until) qui parallélise ce qui était auparavant un calcul récurrent séquentiel, offrant des accélérations d'un ordre de grandeur tout en répartissant correctement les gradients sur l'ensemble des opérations min/max.

Pourquoi c'est important

La logique temporelle de signaux donne à la robotique un moyen précis et lisible par l'humain de spécifier des exigences de mission temporelles et spatiales, mais pendant des années le calcul de sa robustesse était séquentiel, lent et difficile à différencier — ce qui maintenait la STL à l'écart des pipelines modernes d'apprentissage et d'optimisation. stljax lève cet obstacle : une implémentation parallélisée et nativement compatible avec l'autodifférenciation rend la STL suffisamment rapide pour le contrôle en temps réel et l'entraînement par grands lots, de sorte que les spécifications peuvent servir directement d'objectifs de planificateur, de récompenses RL ou de signaux de vérification.

Le problème résolu

Les outils antérieurs de robustesse STL reposaient sur un calcul récurrent séquentiel lent et difficile à différencier, ce qui limitait l'utilisation de spécifications formelles de logique temporelle au sein de l'optimisation de trajectoire par gradient et de l'apprentissage.

Points clés

• Robustesse STL parallèle fondée sur le masquage, jusqu'à environ 1000 fois plus rapide que les méthodes récurrentes sur GPU
• Natif JAX : traitement par lots via vmap et gradients exacts, avec une répartition correcte des gradients sur min/max
• API Expression et Prédicat pour construire des formules Always/Eventually/Until
• Spécifications différentiables utilisables comme objectifs/contraintes en optimisation de trajectoire et en RL
• Installable via pip (stljax) ; RA-L 2025 ; successeur du stlcg PyTorch du Stanford ASL

Pour qui

• Chercheurs en planification de mouvement et en optimisation de trajectoire
• Chercheurs en contrôle et en méthodes formelles
• Concepteurs de récompenses en apprentissage par renforcement
• Ingénieurs en autonomie sûre et en vérification

Limites

• Nécessite une familiarité avec la logique temporelle de signaux pour rédiger des spécifications utiles
• Le lissage/l'approximation de la fonction de robustesse introduit des compromis entre précision et gradient
• Dépendance à JAX et à sa chaîne d'outils
• Une bibliothèque d'évaluation de spécifications — n'inclut pas elle-même de planificateur ou de contrôleur