Deterministic World Models for Verification of Closed-loop Vision-based Systems

1. Il Problema: Verifica Formale di Controller Visivi End-to-End

Il lavoro affronta la sfida critica di verificare formalmente il comportamento in ciclo chiuso di sistemi di controllo basati su visione end-to-end (dove le immagini raw della telecamera sono mappate direttamente in azioni di controllo). Sebbene questi sistemi siano sempre più utilizzati in ambiti safety-critical (veicoli autonomi, robotica), la loro verifica formale rimane aperta a causa di due ostacoli fondamentali:

1. Mancanza di un modello stato-immagine: Non esiste un'equazione analitica chiusa che mappi uno stato fisico (es. posizione, velocità) all'immagine generata dalla telecamera. Senza questa mappatura, il ciclo di verifica non può essere chiuso.
2. Crescita esponenziale dell'approssimazione: Anche se si utilizzano modelli generativi (come le GAN condizionate, cGAN) per sostituire la telecamera, questi modelli introducono variabili latenti stocastiche (rumore casuale). Durante la propagazione degli insiemi di stati attraverso le reti neurali, queste variabili latenti non interpretabili fisicamente costringono a usare limiti di approssimazione molto ampi, portando a un'esplosione degli insiemi raggiungibili (reachable sets) e a falsi positivi (segnalare traiettorie sicure come pericolose).

2. Metodologia Proposta: Deterministic World Model (DWM)

Gli autori propongono un approccio innovativo basato su tre pilastri principali per superare le limitazioni dei metodi esistenti:

A. Deterministic World Model (DWM)

Invece di utilizzare modelli generativi stocastici con variabili latenti, gli autori introducono un Decoder Neurale Latent-Free.

• Funzionamento: Il DWM mappa direttamente lo stato fisico $s$ (es. coordinate, angoli) all'immagine sintetizzata $\hat{I}$.
• Vantaggio: Rimuovendo la variabile latente stocastica, ogni immagine nell'insieme considerato corrisponde a uno stato fisicamente realizzabile. Questo riduce drasticamente la variabilità dell'immagine e mantiene l'input del modello di verifica alla dimensione dello stato fisico, evitando l'esplosione computazionale.

B. Strategia di Addestramento con Doppia Loss

Per garantire che il modello sintetico sia non solo visivamente accurato ma anche sicuro per il controllo, il DWM viene addestrato con una funzione di perdita combinata:

1. Loss di Ricostruzione Pixel (Pixel-level Reconstruction): Minimizza l'errore tra l'immagine reale e quella sintetizzata, con pesi maggiori assegnati alle regioni critiche per il controllo (es. il palo o il veicolo) rispetto allo sfondo.
2. Loss di Coerenza di Controllo (Control-Consistent Loss): Penalizza la discrepanza tra l'azione di controllo generata dall'immagine reale e quella generata dall'immagine sintetizzata. Questo assicura che piccole imperfezioni visive non portino a comportamenti di controllo divergenti.

C. Pipeline di Verifica in Ciclo Chiuso basata su Star-Set

Il DWM viene integrato in una pipeline di verifica formale:

• Propagazione degli Insiemi: Utilizzando la rappresentazione Star-set (che codifica gli stati come trasformazioni affini di uno spazio predicatorio), il sistema propaga gli insiemi di stati attraverso il DWM (per ottenere l'insieme delle immagini), poi attraverso il controller CNN (per ottenere l'insieme delle azioni) e infine attraverso le dinamiche non lineari dell'impianto.
• Analisi: Questo permette di calcolare i "tubi raggiungibili" (reachable tubes) in modo efficiente e rigoroso.

D. Garanzie per il Sistema Reale tramite Conformal Prediction (CP)

Poiché il DWM è un modello surrogato e non perfetto, gli autori utilizzano la Conformal Prediction per trasferire le garanzie di sicurezza dal modello al sistema reale:

• Si calcola una bound statistica (senza assunzioni sulla distribuzione) sulla deviazione massima delle traiettorie tra il sistema reale e quello simulato dal DWM.
• Gli insiemi raggiungibili calcolati sul DWM vengono "gonfiati" (inflated) di questa bound.
• Risultato: Si ottiene una garanzia probabilistica (es. con probabilità $1-\alpha$) che le traiettorie del sistema reale siano contenute negli insiemi verificati.

3. Contributi Chiave

1. Modellazione Deterministica: Un approccio di world modeling che rimuove le variabili latenti stocastiche, creando surrogati generativi verificabili per i sensori a telecamera.
2. Estensione Star-based: La prima estensione dell'analisi di raggiungibilità basata su Star-set per la verifica in ciclo chiuso di sistemi basati su visione.
3. Garanzie Realistiche: L'uso della Conformal Prediction per trasferire rigorosamente i risultati di verifica del modello surrogato al sistema fisico reale.
4. Validazione Sperimentale: Dimostrazione empirica su quattro benchmark (CartPole, MountainCar, Pendulum, Sistema di Frenata) che il metodo supera significativamente le baseline esistenti.

4. Risultati Sperimentali

Gli esperimenti confrontano il DWM con baseline basate su cGAN (Conditional GAN):

• Precisione degli Insiemi Raggiungibili: Il DWM produce insiemi raggiungibili molto più stretti rispetto alle cGAN. Le cGAN, a causa delle variabili latenti, generano immagini con incertezza spaziale eccessiva e rumore di fondo, portando a insiemi raggiungibili che coprono l'intero spazio degli stati (rendendo la verifica inutilmente conservativa).
• Punteggi F1: Il DWM ottiene punteggi F1 superiori in tutti i benchmark (es. 0.9842 per il sistema di frenatura contro 0.6639 della baseline).
• Analisi di Conservatorismo: Mentre le cGAN falliscono nel distinguere le regioni sicure (TNR = 0.0 in alcuni casi, classificando tutto come insicuro), il DWM mantiene un TNR perfetto (1.0) e una precisione del 100%, dimostrando di non generare falsi allarmi.
• Impatto della Loss di Coerenza: L'ablation study mostra che l'aggiunta della Control-Consistent Loss riduce ulteriormente la bound di Conformal Prediction, migliorando la fedeltà della traiettoria simulata rispetto a quella reale.
• Garanzie Reali: L'applicazione della Conformal Prediction riduce leggermente la recall in sistemi altamente sensibili agli errori (come CartPole) a causa dell'espansione necessaria degli insiemi, ma garantisce che le conclusioni di sicurezza siano valide per il sistema fisico reale con alta probabilità.

5. Significato e Impatto

Questo lavoro è significativo perché risolve il "nodo gordiano" della verifica formale per i sistemi di controllo basati su visione:

• Superamento del compromesso Diversità/Verificabilità: Dimostra che è possibile rinunciare alla diversità generativa (variabili latenti) per ottenere modelli deterministici adatti alla verifica formale, senza sacrificare la qualità della ricostruzione per il controllo.
• Sicurezza Garantita: Fornisce un framework che non si limita a simulare il comportamento, ma offre garanzie matematiche rigorose sulla sicurezza del sistema reale, colmando il divario tra modello surrogato e realtà fisica.
• Scalabilità: Offre una via praticabile per verificare sistemi complessi in ambienti non strutturati, dove i modelli geometrici simbolici falliscono.

In sintesi, il paper propone un cambio di paradigma: passare da modelli generativi stocastici (ottimi per la diversità visiva ma pessimi per la verifica) a modelli deterministici guidati dallo stato fisico, integrati con tecniche statistiche moderne per garantire la sicurezza nel mondo reale.