Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies

Sintesi Tecnica: Iniezione Neuro-Simbolica di Vincoli LTLf in Politiche di Reinforcement Learning Autoregressive

Definizione del Problema
Nel Reinforcement Learning (RL) offline, gli agenti apprendono le politiche esclusivamente da dataset pre-raccolti senza interazione online. Sebbene approcci recenti basati sulla modellazione di sequenze, come i Trajectory Transformers (TT) e i Decision Transformers (DT), abbiano con successo inquadrato l'RL come un problema di generazione di sequenze, essi ottimizzano tipicamente solo il reward cumulativo. Ciò crea una lacuna critica nei domini critici per la sicurezza (ad es., robotica, navigazione autonoma) dove le politiche devono aderire a vincoli di alto livello e temporalmente estesi. L'ottimizzazione standard basata sul reward non può garantire che una politica soddisfi complessi requisiti di logica temporale, come "raggiungere eventualmente l'obiettivo evitando sempre i pericoli", specialmente quando le violazioni non possono essere corrette tramite esplorazione per tentativi ed errori in un contesto offline.

Metodologia
Gli autori propongono un framework neuro-simbolico che inietta vincoli di Logica Temporale Lineare su tracce finite (LTL$_f$) direttamente nel processo di addestramento di politiche basate su transformer autoregressivi. La metodologia principale prevede tre componenti fondamentali:

1. Compilazione da LTL$_f$ a DFA: Le specifiche temporali di alto livello vengono compilate in Automi a Stati Finiti Deterministici (DFA). Questa traduzione permette ai vincoli logici di essere rappresentati come sistemi di transizione di stato in grado di elaborare sequenze di token.
2. Perdita Logica Differenziabile: Per integrare questi automi discreti nell'ottimizzazione continua delle reti neurali, gli autori impiegano una rappresentazione differenziabile.
   • Segnali di Soddisfacimento Soft: Invece del campionamento hard, il framework utilizza il campionamento Gumbel-Softmax per generare vettori di token "near-one-hot" differenziabili durante l'addestramento.
   • Integrazione DeepDFA: Questi token "soft" vengono inseriti in un "DeepDFA", una rilassazione neurale dello standard DFA. Questo modulo calcola un segnale di soddisfacimento probabilistico che indica la probabilità che la traiettoria generata soddisfi la formula LTL$_f$.
   • Regolarizzazione: Una funzione di perdita logica ($L_\phi$) viene derivata dal log-probabilità negativa del soddisfacimento. Questa viene combinata con la standard perdita di modellazione di sequenza supervisionata ($L_{\mathcal{D}}$) tramite una somma pesata: $L = \alpha L_\phi + (1 - \alpha) L_{\mathcal{D}}$, dove $\alpha$ è un parametro di trade-off.
3. Agnosticismo Architetturale: Il framework è progettato per essere agnostico rispetto al modello all'interno della classe dei modelli di sequenza autoregressivi. Utilizza un "logic adapter" condiviso per gestire le mappature token-simbolo e i rollout del DFA, rendendolo applicabile sia alle architetture TT che DT senza alterarne le strutture sottostanti.

Contributi Chiave
Il documento delinea tre contributi primari:

• Framework Neuro-Simbolico Unificato: Un metodo per iniettare vincoli LTL$_f$ nelle politiche di RL offline basate su transformer utilizzando moduli basati su automi che sono agnostici rispetto all'architettura.
• Stack di Valutazione Canonico: Una pipeline di valutazione coerente alla fine dell'episodio che allinea la serializzazione del dataset, la mappatura token-simbolo e la valutazione logica, prevenendo discrepanze semantiche tra l'addestramento e la valutazione della logica temporale.
• Analisi Empirica: Una valutazione sistematica in domini di navigazione che dimostra i trade-off tra le prestazioni del compito (return) e la soddisfazione dei vincoli sotto diversi livelli di guida logica.

Risultati Sperimentali
Il framework è stato valutato nell'ambiente di navigazione ColourBomb, testando due tipi di specifiche: Sicurezza Invariante ($G(\neg \text{bomb})$) e Raggiungi-mentre-Sei-Sicuro ($G(\neg \text{bomb}) \land F(\text{goal})$).

• Decision Transformers (DT):
  • I DT vanilla (senza regolarizzazione logica) hanno fallito completamente, colpendo celle con bombe e fallendo nel raggiungere gli obiettivi.
  • L'introduzione della regolarizzazione logica con un alto parametro di trade-off ($\alpha = 0.8$) ha ottenuto il 100% di soddisfazione per entrambe le specifiche di sicurezza e reach-while-safe.
  • Fondamentalmente, questa impostazione ad alto vincolo ha migliorato anche il return medio (da -1.460 a -0.780) eliminando i fallimenti catastrofici (urti con bombe), dimostrando che la soddisfazione dei vincoli può allinearsi alle prestazioni in contesti offline.
• Trajectory Transformers (TT):
  • I TT vanilla hanno mostrato una parziale conformità alla sicurezza ma un basso raggiungimento degli obiettivi.
  • La regolarizzazione logica ha migliorato i tassi di soddisfazione e ridotto i tassi di urto con le bombe. Per il compito di sicurezza invariante, $\alpha = 0.8$ ha prodotto i risultati migliori. Per il compito più complesso di reach-while-safe, un peso inferiore ($\alpha = 0.1$) ha fornito il bilanciamento ottimale, migliorando sia la soddisfazione che il return rispetto al baseline.
  • Gli autori osservano che, sebbene siano stati osservati miglioramenti, questi sono stati più moderati nei TT rispetto ai DT, una discrepanza lasciata a investigazioni future.

Significatività e Claim
Il documento sostiene che l'integrazione della conoscenza simbolica di background direttamente nell'obiettivo di apprendimento — piuttosto che modificare la rappresentazione dei dati o fare affidamento sulla modellazione del reward (reward shaping) — è una direzione promettente per migliorare l'affidabilità delle politiche in RL offline critici per la sicurezza.

Le principali affermazioni riguardanti la significatività del metodo includono:

• Iniezione Diretta dei Vincoli: A differenza degli approcci che si affidano allo "shielding" (che richiede modelli espliciti dell'ambiente) o al reward shaping (che può essere difficile da progettare), questo metodo inietta la conoscenza della logica temporale direttamente nella funzione di perdita dell'addestramento.
• Generalità: Il framework supporta formule LTL$_f$ arbitrarie, estendendosi oltre il "frammento di sicurezza" per includere liveness e combinazioni temporali complesse.
• Preservazione delle Prestazioni: I risultati suggeriscono che l'imposizione di rigorosi vincoli logici non degrada necessariamente le prestazioni del compito; nei scenari testati, ha effettivamente migliorato i return prevenendo esiti catastrofici che i modelli vanilla incontravano frequentemente.

Gli autori mantengono un tono modesto, riconoscendo che l'approccio è attualmente limitato agli ambienti offline e che i miglioramenti osservati nei TT sono stati meno pronunciati rispetto ai DT. Identificano come lavoro futuro l'estensione della valutazione ad altri benchmark, architetture di modello e la conduzione di ampi confronti end-to-end con framework di Safe RL stabiliti.