Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

1. Il Problema

La sicurezza dei sistemi di controllo autonomi (come veicoli aerei o terrestri e manipolatori robotici) è fondamentale per il loro dispiegamento nel mondo reale. Per garantire che questi sistemi rimangano all'interno di un "insieme sicuro", si utilizzano le Funzioni di Barriera di Controllo (CBF).
Recentemente, le CBF sono state rappresentate come Reti Neurali (Neural CBFs) per gestire dinamiche non lineari complesse e vincoli di sicurezza non convessi, superando i limiti dei metodi basati su programmazione polinomiale (come SOS).

Tuttavia, il principale collo di bottiglia è la verifica post-hoc: dimostrare che una rete neurale addestrata soddisfi effettivamente le condizioni matematiche di una CBF valida.

• I metodi esistenti basati su SMT (Satisfiability Modulo Theories) o MIP (Mixed-Integer Programming) non scalano bene con la dimensione della rete neurale o la dimensionalità del sistema.
• I metodi basati su branch-and-bound sono spesso limitati a funzioni di attivazione ReLU, rendendo difficile l'uso di funzioni non lineari più espressive (come tanh o sigmoid) necessarie per problemi complessi.

L'obiettivo del paper è superare queste limitazioni, permettendo la verifica di reti neurali più grandi e con funzioni di attivazione arbitrarie, mantenendo un costo computazionale accettabile.

2. Metodologia

L'approccio proposto evita l'uso di solutori SMT per ragionare direttamente sulle condizioni non lineari esatte. Invece, deriva condizioni lineari sufficienti (sovrastime e sottostime) per verificare la validità della CBF. La metodologia si articola in tre fasi principali:

A. Propagazione dei Limiti Lineari (LBP) Estesa

Il cuore dell'approccio è l'estensione della Linear Bound Propagation (LBP).

• Valori e Gradienti: Mentre la LBP standard calcola limiti lineari per l'output della rete ($B_\theta(x)$), gli autori estendono il metodo per calcolare limiti lineari anche sui gradienti della rete ($\nabla B_\theta(x)$).
• Gestione della Non Linearità: Per gestire i gradienti, che coinvolgono prodotti bilineari tra i pesi della rete e le derivate delle funzioni di attivazione, l'approccio utilizza rilassamenti di McCormick. Questo permette di ottenere limiti lineari superiori e inferiori per il Jacobiano della rete senza bisogno di passaggi in avanti aggiuntivi della rete stessa.
• Supporto Generale: Il metodo è agnostico rispetto alla funzione di attivazione (supporta tanh, ReLU, Leaky-ReLU, sigmoid), purché semidifferenziabile.

B. Modellazione delle Dinamiche e Surrogato Lineare

Per verificare la condizione di invarianza della CBF (che include termini come $\nabla B \cdot f(x)$ e $\sup_u \nabla B \cdot g(x)u$), il metodo:

1. Applica espansioni di Taylor del primo ordine certificate per limitare le dinamiche del sistema $f(x)$ e $g(x)$ all'interno di un dominio.
2. Combina i limiti della rete neurale (valori e gradienti) con i limiti delle dinamiche utilizzando nuovamente i rilassamenti di McCormick.
3. Costruisce un surrogato lineare conservativo ($\phi_{linear}$) della formula di verifica originale. Se questo surrogato lineare è soddisfatto, allora anche la condizione non lineare originale è soddisfatta.

C. Strategia di Raffinamento Adattivo

Poiché i limiti lineari possono essere troppo conservativi su domini ampi, gli autori introducono una strategia di raffinamento:

• Invece di dividere lo spazio degli stati in iperrettangoli (comune nei metodi precedenti), utilizzano una mesh di simplessi (partizione in simplex).
• Se la verifica è inconcludente su un simplex, questo viene diviso lungo il suo spigolo più lungo.
• Questa strategia è parallelizzabile: i calcoli sui limiti e la verifica dei surrogati possono essere eseguiti in batch su GPU, permettendo di gestire migliaia di regioni simultaneamente.

3. Contributi Chiave

1. Nuovo Metodo di Verifica Scalabile: Introduzione di una tecnica che combina LBP e rilassamenti di McCormick per verificare le CBF neurali, eliminando la dipendenza da solutori SMT costosi.
2. Estensione ai Gradienti: Sviluppo di un metodo per calcolare limiti lineari sui gradienti delle reti neurali, essenziale per le condizioni di invarianza delle CBF in tempo continuo.
3. Strategia di Raffinamento su Simplessi: Creazione di una strategia di raffinamento adattivo parallela basata su mesh di simplessi, che riduce la conservatività dei limiti in modo più efficace rispetto alle partizioni iperrettangolari.
4. Supporto per Funzioni di Attivazione Arbitrarie: Il metodo non è limitato alle reti ReLU, permettendo l'uso di funzioni di attivazione più espressive per catturare dinamiche complesse.

4. Risultati Sperimentali

Gli autori hanno valutato il metodo su diversi benchmark standard e nuovi (inclusi sistemi 2D-Control e Cart-Pole con input di controllo).

• Scalabilità: Il metodo è stato in grado di verificare reti neurali significativamente più grandi (es. architetture fino a [128, 256, 128]) rispetto alle tecniche SMT-based (come dreal), che hanno fallito o richiesto timeout su reti più piccole.
• Efficienza: In tutti i test, il tempo di verifica del metodo proposto è stato drasticamente inferiore rispetto ai solutori SMT (es. 1.66s vs 635s per il benchmark "Barrier 2").
• Accuratezza: Il metodo ha certificato il 100% dello spazio degli stati per i benchmark testati, dimostrando che la conservatività introdotta dai rilassamenti è gestibile grazie alla strategia di raffinamento adattivo.
• Gestione degli Input di Controllo: A differenza di molti approcci precedenti, il metodo gestisce nativamente il termine $\sup_{u \in U}$, rendendolo adatto per applicazioni con filtri di sicurezza.

5. Significato e Impatto

Questo lavoro rappresenta un passo avanti significativo verso l'adozione pratica delle CBF neurali in sistemi di sicurezza critica.

• Superamento del Collo di Bottiglia: Risolve il problema principale che ha finora limitato l'uso delle CBF neurali: la difficoltà di verifica su reti di dimensioni utili.
• Flessibilità: Abilita l'uso di architetture neurali più complesse e funzioni di attivazione non lineari, permettendo di trovare insiemi invarianti di controllo più ampi e meno conservativi.
• Integrazione Futura: L'approccio è compatibile con framework "learner-verifier" (apprendimento-verifica), dove la rete viene addestrata e verificata iterativamente, accelerando lo sviluppo di controllori sicuri per robotica e sistemi autonomi.

In sintesi, il paper propone un framework di verifica scalabile, efficiente e generalizzabile, che trasforma la verifica delle CBF neurali da un problema computazionalmente intrattabile per reti grandi a un processo fattibile e pratico.