Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks

Sintesi Tecnica: Apprendimento di Funzioni di Lyapunov per il Controllo Robusto tramite Reti Neurali Lipschitziane

Problematica
Il documento affronta la sfida di progettare controllori stabilizzanti per sistemi dinamici non lineari soggetti a disturbi additivi. Sebbene le funzioni di Lyapunov siano uno strumento fondamentale per l'analisi della stabilità, la loro costruzione automatica per sistemi non lineari generici rimane un problema aperto. I metodi computazionali esistenti, come Sum-of-Squares (SOS) o le Disuguaglianze Lineari Matriciali (LMI), spesso faticano con la scalabilità o la generalità. Inoltre, i recenti approcci di deep learning che apprendono Funzioni di Lyapunov per il Controllo (CLF) utilizzando reti neurali si concentrano tipicamente su dinamiche esatte senza disturbi o si affidano a metodi di verifica che sono computazionalmente costosi o conservativi (ad esempio, utilizzando solo informazioni di ordine zero). La sfida specifica affrontata qui è l'apprendimento di una Funzione di Lyapunov per il Controllo Robusto (RCLF) e di un corrispondente controllore a feedback di stato che garantisca la Stabilità Limite Uniforme (UUB) in presenza di disturbi additivi dipendenti dallo stato, assicurando al contempo che la verifica di queste condizioni sia computazionalmente trattabile.

Metodologia
Il framework proposto integra Reti Neurali Lipschitziane (LNN) con un algoritmo di verifica Branch-and-Bound (BnB) di ordine superiore.

1. Reti Neurali Lipschitziane (LNN):
   Gli autori utilizzano LNN per apprendere congiuntamente la RCLF ($V_{\theta_1}$) e il controllore stabilizzante ($\pi_{\theta_2}$). A differenza delle reti standard, le LNN impongono una costante di Lipschitz predefinita attraverso specifiche parametrizzazioni degli strati (ad esempio, Normalizzazione Spettrale, Strati Ortogonali o Strati Sandwich). Questo vincolo è critico perché permette di derivare limiti espliciti e stretti sulle derivate di ordine superiore (Essiana e derivate del terzo ordine) dell'output della rete rispetto al suo input. La RCLF è definita come l'output di una rete traslata per garantire la condizione di equilibrio $V(0)=0$.

2. Algoritmo di Addestramento:
   Il processo di addestramento minimizza una funzione di perdita composita su uno spazio di stato campionato e sul confine. I termini di perdita impongono:

   • Definitezza Positiva: Garantire che $V(x) > 0$ per $x \neq 0$.
   • Condizione di Decrescita: Garantire che la derivata temporale $\dot{V}$ sia negativa al di fuori di una piccola sfera attorno all'origine, tenendo conto del caso peggiore di disturbo. Ciò comporta la stima superiore del termine di disturbo utilizzando il limite del disturbo noto $\epsilon(x)$ e le costanti di Lipschitz della rete e delle dinamiche del sistema.
   • Confine e Copertura: Incoraggiare il sotto-livello di $V$ a coprire la porzione massima dello spazio di stato e a mantenere un valore coerente sul confine.
     L'algoritmo inizializza i parametri utilizzando le soluzioni del Regolatore Lineare Quadratico (LQR) e li affina iterativamente, memorizzando i parametri che producono la regione di invarianza del semiasse empiricamente verificata più grande.

3. Verifica di Ordine Superiore (Branch-and-Bound):
   Viene introdotto un nuovo algoritmo BnB compatibile con le GPU per verificare formalmente la RCLF appresa. A differenza dei solutori tradizionali (ad esempio, dReal) che si affidano a limiti di ordine zero o ai solutori SMT che affrontano limiti di scalabilità, questo metodo sfrutta la regolarità delle LNN.

   • Limiti di Ordine Superiore: Gli autori derivano espliciti limiti della norma spettrale per l'Essiana e le derivate del terzo ordine delle LNN. Questi limiti vengono utilizzati per costruire limiti inferiori e superiori stretti sull'output della rete tramite espansioni di Taylor (fino al secondo ordine).
   • Efficienza dell'Algoritmo: Incorporando informazioni del primo e secondo ordine, l'algoritmo crea involucri significativamente più stretti dei valori della funzione all'interno dei rettangoli di ricerca. Ciò consente una rimozione (pruning) più aggressiva dello spazio di ricerca rispetto ai metodi di ordine zero.
   • Complessità: Il documento stabilisce i limiti della complessità temporale nel caso peggiore, mostrando che il numero di rettangoli valutati scala polinomialmente con la dimensione del sistema e inversamente con la tolleranza, ma è drasticamente ridotto nella pratica grazie ai limiti più stretti.

Contributi Chiave

1. Framework Innovativo: Un approccio unificato per apprendere RCLF robuste e controllori stabilizzanti per sistemi non lineari con disturbi additivi dipendenti dallo stato utilizzando LNN.
2. Limiti delle Derivate: L'instaurazione di espliciti limiti della norma spettrale per l'Essiana e le derivate del terzo ordine delle LNN. Questi limiti sono più stretti di quelli derivati solo da informazioni di ordine zero o primo, affrontando la non-convessità della verifica di Lyapunov.
3. Verifica Compatibile con GPU: Lo sviluppo di un algoritmo BnB che utilizza questi limiti di ordine superiore e supporta la valutazione in batch su GPU. Ciò accelera significativamente il processo di verifica rispetto ai solutori SMT basati su CPU.
4. Validazione Empirica: Simulazioni estese su sei sistemi dinamici (pendolo inverso, unicycle, sistema del terzo ordine, cartpole, quadrotor 2D e braccio SCARA) che dimostrano la capacità del metodo di verificare la stabilità e superare gli strumenti esistenti (dReal, $\alpha,\beta$-CROWN) in termini di velocità e scalabilità.

Risultati
Il documento presenta i risultati delle simulazioni confrontando il metodo proposto con dReal (SMT basato su CPU) e $\alpha,\beta$-CROWN (propagazione dei limiti basata su GPU).

• Velocità di Verifica: Il proposto algoritmo BnB basato su GPU supera costantemente dReal, riducendo spesso il tempo di verifica da ore (o timeout) a secondi, anche per sistemi con dimensioni di stato più elevate (ad esempio, braccio SCARA con $n_x=8$).
• Scalabilità: Mentre dReal fallisce nel verificare sistemi con più di 2-3 strati in un tempo ragionevole, il metodo proposto verifica con successo reti fino a 4 strati.
• Regioni di Invarianza in Avanti: I controllori appresi ottengono regioni di invarianza in avanti significativamente più grandi rispetto agli approcci LQR standard e ai non-robusti CLF neurali (NLC). Per il pendolo inverso, il metodo proposto ha ottenuto un rapporto di regione di invarianza in avanti di circa il 75%, rispetto al 23% circa di LQR.
• Robustezza: La verifica conferma che i controllori appresi soddisfano la condizione UUB, mantenendo le traiettorie all'interno di una regione limitata nonostante la presenza di disturbi.

Significatività e Rivendicazioni
Il documento afferma che la sua principale significatività risiede nel colmare il divario tra l'espressività del deep learning e i requisiti rigorosi della verifica del controllo robusto. Sfruttando la struttura specifica delle reti Lipschitziane per derivare limiti delle derivate di ordine superiore, gli autori consentono un processo di verifica che è sia matematicamente rigoroso che computazionalmente efficiente.

Gli autori dichiarano esplicitamente che il loro framework non certifica la stabilità per un modello sconosciuto senza un limite di errore noto; piuttosto, fornisce una garanzia deterministica di robustezza contro un disallineamento del modello certificato o un disturbo limitato. Il lavoro evidenzia che, sebbene le LNN possano avere un'espressività ridotta rispetto alle reti non vincolate, il compromesso è giustificato dalla capacità di eseguire una verifica di ordine superiore efficiente, essenziale per le applicazioni di controllo critiche per la sicurezza. Il documento conclude che questo approccio rende la verifica formale di controllori appresi e robusti per sistemi non lineari complessi praticamente fattibile.