STLCG

Toolbox JAX per la robustezza differenziabile di Signal Temporal Logic

Licenza

BSD-2-Clause

Panoramica

STLCG (distribuito come libreria JAX stljax) è un toolbox per calcolare la robustezza delle formule di Signal Temporal Logic (STL) mediante grafi computazionali. STL è un linguaggio formale per esprimere requisiti spazio-temporali come "entra nella regione obiettivo entro 10 secondi e restaci per 5 secondi", e la sua misura di robustezza quantifica quanto fortemente un segnale soddisfa o viola una specifica. stljax reimplementa in JAX l'originale stlcg in PyTorch dello Stanford ASL del 2019, sostituendo la valutazione ricorrente sequenziale con una formulazione basata su maschere, completamente parallelizzabile, che su GPU è fino a ~1000x più veloce. Poiché l'intera pipeline è differenziabile, le specifiche STL si possono incorporare direttamente nell'ottimizzazione delle traiettorie basata sul gradiente, nella definizione delle ricompense per l'apprendimento per rinforzo e nell'estrazione dei parametri. Pubblicato su IEEE Robotics and Automation Letters (RA-L) 2025; installabile con pip come stljax.

stljax permette agli ingegneri robotici di trasformare specifiche di missione in logica temporale, leggibili dalle persone, in termini differenziabili di obiettivo e di vincolo. Si costruiscono formule STL da Expression e Predicate, se ne valuta la robustezza su un segnale o una traiettoria e, poiché tutto è implementato in JAX, si ottengono la valutazione in batch tramite vmap e gradienti esatti da usare dentro ottimizzatori e cicli di apprendimento. La scelta progettuale chiave è una riformulazione basata su maschere degli operatori temporali (Always/Eventually/Until) che parallelizza quello che prima era un calcolo ricorrente sequenziale, ottenendo accelerazioni di un ordine di grandezza e distribuendo al tempo stesso correttamente i gradienti su tutte le operazioni di min/max.

Perché è importante

Signal Temporal Logic offre alla robotica un modo preciso e leggibile per specificare i requisiti temporali e spaziali di una missione, ma per anni il calcolo della sua robustezza è stato sequenziale, lento e scomodo da differenziare, tenendo STL fuori dalle moderne pipeline di apprendimento e ottimizzazione. stljax elimina questa barriera: un'implementazione parallelizzata e nativa per la differenziazione automatica rende STL abbastanza veloce per il controllo in tempo reale e l'addestramento su grandi batch, così le specifiche possono fungere direttamente da obiettivi del pianificatore, ricompense RL o segnali di verifica.

Il problema che risolve

I precedenti strumenti di robustezza STL si basavano su un calcolo ricorrente sequenziale, lento e difficile da differenziare, il che limitava l'uso di specifiche formali in logica temporale all'interno dell'ottimizzazione delle traiettorie e dell'apprendimento basati sul gradiente.

Punti chiave

• Robustezza STL parallela basata su maschere, fino a ~1000x più veloce dei metodi ricorrenti su GPU
• Nativo JAX: batch con vmap e gradienti esatti, con una distribuzione corretta del gradiente su min/max
• API Expression e Predicate per costruire formule Always/Eventually/Until
• Specifiche differenziabili utilizzabili come obiettivi/vincoli nell'ottimizzazione delle traiettorie e nell'RL
• Installabile con pip (stljax); RA-L 2025; successore di stlcg in PyTorch dello Stanford ASL

A chi si rivolge

• Ricercatori di pianificazione del movimento e ottimizzazione delle traiettorie
• Ricercatori di controllo e metodi formali
• Progettisti di ricompense per l'apprendimento per rinforzo
• Ingegneri di autonomia sicura e di verifica

Limiti

• Richiede familiarità con Signal Temporal Logic per scrivere specifiche utili
• Lo smoothing/l'approssimazione della funzione di robustezza introduce compromessi tra precisione e gradiente
• La dipendenza da JAX e dalla sua toolchain
• È una libreria per valutare le specifiche: non include di per sé un pianificatore o un controller