Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Sintesi Tecnica: Verifica di Sistemi Dinamici Sconosciuti tramite lo Spazio Latente di Autoencoder

Formulazione del Problema
La verifica formale di sistemi dinamici a spazio continuo è essenziale per garantire che i sistemi autonomi soddisfino specifiche di sicurezza e di vivacità, spesso espresse nella Logica Temporale Lineare (LTL). Gli approcci standard prevedono la costruzione di astrazioni a stati finiti per abilitare il model checking. Tuttavia, queste tecniche affrontano sfide di scalabilità severe in contesti ad alta dimensionalità, poiché la dimensione dell'astrazione cresce esponenzialmente con la dimensione dello spazio degli stati. Questo problema è esacerbato nei sistemi abilitati dall'intelligenza artificiale (ad esempio, quelli controllati da reti neurali che elaborano dati LiDAR o da telecamere), dove le dinamiche sono complesse, parzialmente sconosciute o a scatola nera. Sebbene le tecniche di riduzione della dimensionalità basate sui dati, come gli autoencoder, offrano una potenziale soluzione per la scalabilità, esse tipicamente mancano di garanzie formali di correttezza. Nello specifico, mappare specifiche ad alta dimensionalità in uno spazio latente appreso e garantire che le dinamiche latenti apprese rappresentino fedelmente il comportamento del sistema originale (incluso il non determinismo) rimane una sfida aperta. I metodi esistenti spesso scambiano la correttezza con la flessibilità o si basano su forti assunzioni riguardo alle dinamiche del sistema che non valgono per le rappresentazioni apprese.

Metodologia
Il framework proposto affronta queste sfide combinando la riduzione della dimensionalità con la verifica basata su astrazioni per fornire garanzie formali per sistemi ad alta dimensionalità con dinamiche sconosciute. L'approccio consta di quattro fasi principali:

1. Architettura di Autoencoder Convesso: Per garantire che lo spazio latente sia interpretabile e supporti un ragionamento corretto, gli autori impiegano un Autoencoder Convesso. Il codificatore è vincolato a essere una Rete Neurale Convessa in Input (ICNN) con specifiche restrizioni strutturali: funzioni di attivazione strettamente monotone (per agire come omeomorfismi), primo strato e strati di salto iniettivi, e matrici dei pesi a rango completo. Questa architettura, denominata rete "Input Connesso-Output Connesso" (CICO), garantisce che la controimmagine di qualsiasi insieme connesso nello spazio latente sia un insieme connesso nello spazio degli stati originale. Questa proprietà è cruciale per gestire la non iniettività della mappatura quando la dimensione latente è inferiore alla realizzazione minima del sistema.

2. Apprendimento di Dinamiche di Inclusione Latenti: Poiché la riduzione della dimensionalità può comportare una perdita di informazioni, l'evoluzione nello spazio latente è modellata come dinamiche di inclusione (a valori di insieme) piuttosto che come equazioni alle differenze deterministiche. Gli autori introducono le "Gaussian Process di Inclusione" (Inclusion GPs), una formulazione innovativa della Regressione con Processi Gaussiani (GPR) per dinamiche a valori di insieme. Questo metodo eleva le dinamiche a uno spazio di dimensione superiore dove seguono equazioni alle differenze che coinvolgono un parametro non osservato $c$. Imparando un kernel profondo che incorpora questa coordinata non osservata, il metodo prevede l'evoluzione del sistema come un insieme (specificamente, una sfera nello spazio latente) e fornisce limiti di errore rigorosi basati sull'analisi dello Spazio di Hilbert a Kernel Riproducente (RKHS).

3. Costruzione di un'Astrazione Finita Corretta: Utilizzando l'Inclusion GP appreso, gli autori costruiscono un Sistema di Transizione Non Deterministico (NTS) nello spazio latente.

   • Mappatura delle Regioni: Regioni di interesse ad alta dimensionalità (insiemi sicuri, insicuri e obiettivo) sono mappate nello spazio latente. La convessità del codificatore consente un'approssimazione inferiore basata sul campionamento efficiente e un'approssimazione superiore probabilistica (utilizzando $\epsilon$-RandUp) di questi insiemi.
   • Relazione di Transizione: Le transizioni tra stati astratti sono calcolate propagando le regioni attraverso il modello Inclusion GP, tenendo conto degli errori di regressione e del parametro non osservato $c$. Ciò garantisce che l'astrazione catturi conservativamente tutti i comportamenti possibili del sistema originale.
   • Garanzie di Correttezza: Il framework dimostra che se uno stato nell'NTS latente soddisfa una specifica di raggiungimento-evitamento, allora tutte le traiettorie corrispondenti nel sistema originale ad alta dimensionalità soddisfano la specifica con un alto livello di confidenza ($1-\delta$).

4. Verifica e Decodifica: Strumenti standard di model checking sono applicati all'NTS latente per identificare gli stati garantiti a soddisfare la specifica ($Q_{yes}$), gli stati che non possono soddisfarla ($Q_{no}$) e gli stati incerti ($Q_?$). Poiché il codificatore è convesso, gli stati latenti soddisfacenti possono essere decodificati efficientemente nello spazio originale ad alta dimensionalità utilizzando l'ottimizzazione convessa per identificare l'insieme degli stati iniziali nel sistema originale che sono garantiti come sicuri.

Contributi Chiave
Il paper apporta quattro contributi principali:

1. Mappatura Provabilmente Corretta: Un metodo per mappare specifiche di alto livello in uno spazio latente utilizzando un codificatore CICO, abilitando un ragionamento efficiente su rappresentazioni compresse preservando al contempo garanzie formali.
2. Inclusion GPs: Una formulazione innovativa della regressione con Processi Gaussiani per dinamiche a valori di inclusione (a valori di insieme), che permette l'apprendimento di dinamiche latenti governate da inclusioni alle differenze senza richiedere la conoscenza esplicita dei parametri sottostanti non osservati.
3. Framework di Astrazione Corretto: Un framework completo per generare astrazioni finite corrette nello spazio latente basato su Inclusion GPs, inclusi procedimenti per mappare le garanzie di soddisfazione al sistema originale con prove di correttezza.
4. Validazione Empirica: Dimostrazione dell'approccio su più sistemi, incluso un sistema a 26 dimensioni controllato da una rete neurale (utilizzando input LiDAR), che mostra miglioramenti significativi di scalabilità rispetto ai metodi di astrazione tradizionali.

Risultati
L'approccio è stato valutato su tre studi di caso:

• Da 3D a 2D: Un sistema a realizzazione minima dove il metodo ha verificato con successo l'intero spazio latente, mentre l'astrazione basata sui dati tradizionale nello spazio originale 3D non è riuscita a verificare la raggiungibilità a causa dell'incertezza nelle dimensioni a movimento lento.
• Da 6D a 2D: Un sistema sovraparametrizzato con osservazioni non lineari. Il metodo ha verificato il 100% dello spazio latente per il caso senza ostacoli e il 59,78% per il caso con un ostacolo. Al contrario, il tentativo di astrazione nello spazio originale 6D ha portato a un'esplosione degli stati, non riuscendo a verificare alcuna regione oltre l'obiettivo stesso entro il limite di tempo.
• Da 26D a 2D: Un compito di navigazione robotica con input LiDAR e un controllore a rete neurale. Il metodo ha appreso con successo uno spazio latente 2D che ha catturato le dinamiche del sistema con un non determinismo minimo, verificando il 50,0001% dello spazio latente. Ciò ha dimostrato la capacità di gestire spazi di osservazione ad alta dimensionalità dove i metodi tradizionali sono non fattibili.

Significato
Il paper afferma di colmare un divario critico tra riduzione della dimensionalità e verifica formale. Fornendo garanzie di correttezza sia per la mappatura delle specifiche sia per le dinamiche latenti apprese, il lavoro elimina i falsi positivi nei risultati di verifica, un problema comune nel controllo basato sull'apprendimento. Gli autori sottolineano che il loro approccio abilita una verifica scalabile per sistemi ad alta dimensionalità con dinamiche sconosciute, una capacità precedentemente irraggiungibile con i metodi formali esistenti. Sebbene il framework sia corretto, gli autori notano modestamente le limitazioni, inclusa la restrizione a codificatori convessi (che limita l'espressività) e questioni aperte riguardo all'incorporazione del rumore e alla sintesi del controllo, che sono identificate come direzioni per lavori futuri.