Sintesi Tecnica: Certificati Neurali di Raggiungimento-Mentre-Si-Evita Cooperativi per Sistemi Interconnessi

1. Definizione del Problema

Il documento affronta la sfida fondamentale di fornire garanzie formali di stabilità e sicurezza per sistemi interconnessi su larga scala controllati da policy basate su reti neurali. Sebbene i controllori basati sull'apprendimento (ad esempio, il Deep Reinforcement Learning) eccellano nel gestire dinamiche complesse e incerte in applicazioni come il trasporto intelligente e la robotica, la loro natura "black-box" impedisce una verifica rigorosa. I metodi formali esistenti spesso si affidano a modelli di sistema accurati o non riescono a scalare, mentre gli attuali approcci di certificazione neurale tipicamente trascurano le interazioni cooperative e le strutture di vicinato dinamiche intrinseche nei sistemi multi-agente.

Il problema specifico formulato è il compito di Multi-Agent Reach-While-Avoid (MARWA). Un team di $q$ agenti deve:

1. Raggiungere (Reach): Convergere verso un insieme di obiettivo $X_{i,G}$ (liveness).
2. Evitare (Avoid): Non entrare mai in un insieme non sicuro $X_{i,U}$ (safety).
3. Cooperare: Operare sotto range di comunicazione limitati in cui gli agenti interagiscono solo con i vicini entro un raggio di rilevamento $R_c$, e tali vicinati cambiano dinamicamente in base allo stato.

Le funzioni di Lyapunov e di barriera scalari standard sono considerate intrattabili per sistemi su larga scala a causa dell'elevata dimensionalità dello spazio di stato congiunto.

2. Metodologia

Gli autori propongono un framework centrato su Certificati Neurali di Reach-While-Avoid Cooperativo (Co-RWA), che combina garanzie di controllo teorico con la sintesi di reti neurali scalabili.

A. Fondamenti Teorici: DL-VCLFs e DL-VCBFs

Per gestire la decentralizzazione e le interazioni dinamiche, il documento introduce due nuovi concetti di certificati vettoriali:

• Funzioni di Controllo Lyapunov Vettoriali Dinamico-Localizzate (DL-VCLFs): Garantiscono la Stabilità Esponenziale Globale (GES). A differenza delle funzioni scalari, le DL-VCLF utilizzano un vettore $V(x) = (V_1, \dots, V_q)$ dove ogni componente $V_i$ dipende dallo stato locale e da un indicatore di vicinato dinamico $A_i(x)$. La condizione di stabilità è governata da una matrice Metzler e Hurwitz $\Lambda$, assicurando che il tasso di decadimento della funzione di Lyapunov di ogni agente dipenda dagli stati dei suoi attuali vicini.
• Funzioni di Barriera di Controllo Vettoriali Dinamico-Localizzate (DL-VCBFs): Garantiscono la sicurezza (invarianza in avanti). Similmente alle DL-VCLF, utilizzano un vettore $h(x)$ e una matrice Metzler $\Upsilon$ per imporre che il sistema rimanga all'interno di un insieme sicuro $C = \prod C_i$, anche quando la struttura del vicinato cambia.

Insieme, questi formano il Certificato Co-RWA, fornendo garanzie decentralizzate che gli agenti raggiungeranno cooperativamente gli obiettivi evitando al contempo le collisioni.

B. Sintesi Scalabile e Framework di Verifica

Il documento sviluppa un ciclo di Sintesi Induttiva Guidata da Controesempi (CEGIS) per addestrare congiuntamente controllori e certificati:

1. Formulazione dell'Addestramento: Il problema è inquadrato come un'ottimizzazione vincolata che minimizza una funzione di perdita che bilancia:
   • L'imitazione di un controllore nominale (ad esempio, da RL).
   • La fattibilità delle condizioni DL-VCLF (decadimento di Lyapunov).
   • La fattibilità delle condizioni DL-VCBF (sicurezza della barriera).
   • Margini di sicurezza stretti ($h \geq \epsilon_0$ nelle regioni sicure, $h < 0$ nelle regioni non sicure).
2. Verifica con Errori di Modellazione: Poiché gli strumenti di verifica operano su modelli a tempo discreto, gli autori derivano condizioni sufficienti (Teorema 3) che tengono conto di:
   • Errore di discretizzazione: Differenze tra dinamiche continue ed approssimazioni di Eulero.
   • Errore di approssimazione: Differenze tra dinamiche reali e surrogati di reti neurali.
     Questi errori sono limitati e propagati nelle disuguaglianze del certificato, assicurando che se il modello neurale a tempo discreto soddisfa le condizioni, il vero sistema a tempo continuo è garantito essere sicuro e stabile.
3. Raffinamento Iterativo: Se un verificatore formale trova un controesempio (uno stato che viola il certificato), i dati vengono aumentati e la rete viene riaddestrata.

C. Riutilizzo Strutturale per la Scalabilità

Per superare il collo di bottiglia computazionale della verifica di grandi sistemi, gli autori introducono un meccanismo di riutilizzo strutturale.

• Isomorfismo di Sottostruttura: Definito come una mappatura in cui un sottosistema più piccolo condivide dinamiche locali e topologie di vicinato identiche con un sistema più grande.
• Trasferibilità: Il Teorema 4 dimostra che se un sistema più piccolo è sottostrutturalmente isomorfo a uno più grande, i controllori e i certificati appresi possono essere direttamente trasferiti senza riaddestramento o riverifica. Ciò consente di scalare da piccoli testbed a implementazioni su larga scala.

3. Contributi Chiave

1. Certificati Neurali Co-RWA: L'iniziazione di certificati neurali che modellano esplicitamente le dinamiche cooperative e i vicinati dipendenti dallo stato tramite funzioni vettoriali dinamico-localizzate, fornendo garanzie teoriche di stabilità esponenziale e sicurezza.
2. Framework di Verifica Scalabile: Un pipeline unificato di addestramento e verifica che incorpora gli errori di modellazione (discretizzazione e approssimazione) nelle condizioni di verifica, garantendo le garanzie formali per il sistema continuo sottostante.
3. Meccanismo di Riutilizzo Strutturale: Un metodo per trasferire controllori e certificati tra sistemi sottostrutturalmente isomorfi, migliorando significativamente la scalabilità per sistemi interconnessi su larga scala.
4. Validazione Empirica: Dimostrazione del framework su scenari di coordinamento multi-robot e convogli di veicoli, mostrando un'esecuzione Co-RWA di successo con forti metriche di controllo.

4. Risultati e Validazione

La metodologia è stata validata attraverso estese simulazioni numeriche:

• Scenari: Il framework è stato testato su robot omnidirezionali e convogli di veicoli.
• Performance: I risultati hanno dimostrato che i controllori sintetizzati hanno garantito con successo che gli agenti raggiungessero i loro insiemi di obiettivo evitando rigorosamente le regioni non sicure (collisioni).
• Scalabilità: Il meccanismo di riutilizzo strutturale ha permesso il trasferimento di certificati da sistemi più piccoli a sistemi più grandi, validando l'affermazione che il framework può gestire sistemi interconnessi su larga scala senza costi computazionali proibitivi.
• Verifica: L'inclusione dei limiti di errore nel processo di verifica ha garantito che le garanzie formali rimanessero valide nonostante l'uso di surrogati di reti neurali e approssimazioni a tempo discreto.

5. Significato e Rivendicazioni

Il documento sostiene di affrontare una lacuna critica nello spiegamento di controllori basati sull'apprendimento per sistemi su larga scala e critici per la sicurezza. La sua importanza risiede nel:

• Andare oltre i vincoli "morbidi" (funzioni di perdita) per raggiungere garanzie formali e rigorose sia per la stabilità che per la sicurezza in contesti multi-agente cooperativi.
• Risolvere il collo di bottiglia della scalabilità che ha precedentemente impedito la verifica formale di sistemi interconnessi su larga scala, principalmente attraverso l'introduzione di certificati vettoriali e il riutilizzo strutturale.
• Fornire un ciclo di sintesi pratico (CEGIS) che colma il divario tra la teoria del controllo e il deep learning moderno, rendendo possibile l'addestramento di controllori neurali che siano provabilmente sicuri e stabili anche in presenza di incertezze di modellazione.

Gli autori posizionano questo lavoro come un passo verso lo spiegamento sicuro di sistemi autonomi in ambienti complessi e reali dove la cooperazione e la sicurezza sono fondamentali.