SCORE: Statistical Certification of Regions of Attraction via Extreme Value Theory

Titolo

SCORE: Certificazione Statistica delle Regioni di Attrazione tramite Teoria dei Valori Estremi

1. Il Problema

La certificazione della Region of Attraction (ROA) per sistemi dinamici non lineari ad alta dimensionalità rappresenta un collo di bottiglia computazionale severo.

• Limiti dei metodi deterministici: Le tecniche di verifica tradizionali, come la programmazione Sum-of-Squares (SOS) e i risolutori Satisfiability Modulo Theories (SMT), forniscono garanzie deterministiche rigide ma soffrono della "maledizione della dimensionalità".
  • L'SOS soffre di esplosioni combinatorie nelle matrici per polinomi di alto grado.
  • Gli SMT incontrano problemi NP-hard nella risoluzione di vincoli, specialmente con rappresentazioni dense come le Funzioni di Lyapunov Neurali (NLF).
• Conseguenza: Questi metodi falliscono tipicamente oltre 20 dimensioni, rendendo impossibile la verifica formale di sistemi complessi, densi e ad alta dimensionalità (es. 500 dimensioni).

2. Metodologia: Il Framework SCORE

Gli autori propongono SCORE, un framework di certificazione statistica che abbandona la ricerca di garanzie deterministiche assolute a favore del bounding del peggior caso di violazione della sicurezza con alta confidenza statistica.

Il metodo si basa su due pilastri principali:

1. Projected Stochastic Gradient Langevin Dynamics (PSGLD):

   • Invece di esplorare l'intero volume dello stato, l'algoritmo campiona la derivata di Lyapunov $\dot{V}(x)$ esclusivamente sulla varietà di vincolo definita dal bordo del sottoinsieme di livello ($M = \{x | V(x) = \rho\}$).
   • Utilizza un processo stocastico (PSGLD) proiettato su questa varietà per esplorare i picchi locali di $\dot{V}(x)$, prevenendo il collasso in minimi locali grazie al rumore iniettato.

2. Teoria dei Valori Estremi (EVT):

   • Il problema di trovare il massimo globale di $\dot{V}(x)$ viene riformulato come un problema di stima di valori estremi vincolati.
   • Giustificazione Teorica: Dimostrano che modellando l'ottimizzazione come una diffusione stocastica su una varietà compatta, i massimi locali della derivata di Lyapunov appartengono al dominio di attrazione di Weibull (un tipo di distribuzione dei valori estremi generalizzati, GEV).
   • La proprietà chiave del dominio di Weibull è l'esistenza di un estremo destro finito. Questo permette di calcolare un limite superiore statistico rigoroso per il massimo globale di $\dot{V}(x)$.

Algoritmo di Certificazione:

1. Campionamento: Eseguire catene PSGLD per raccogliere campioni di $\dot{V}(x)$.
2. Blocchi di Massimi (Block Maxima): Dividere i campioni in blocchi non sovrapposti ed estrarre il massimo di ciascun blocco.
3. Fitting GEV: Adattare una distribuzione GEV ai massimi dei blocchi utilizzando la Massima Verosimiglianza (MLE).
4. Stima del Confidenza: Poiché la distribuzione appartiene al dominio di Weibull ($\xi < 0$), si calcola un limite superiore finito ($z^*$). Si utilizza il bootstrapping per costruire un intervallo di confidenza superiore rigoroso ($CI_{upper}$).
5. Decisione: Se $CI_{upper} < 0$ e il test di bontà di adattamento (Kolmogorov-Smirnov) è superato, la regione è certificata con un livello di confidenza specificato (es. 99.99%).

3. Contributi Chiave

• Nuovo Framework Statistico: Integrazione di EVT e PSGLD per trasformare la certificazione della ROA in un problema di stima di valori estremi vincolati, aggirando i limiti dei metodi deterministici.
• Garanzia Teorica di Limitatezza: Dimostrazione che i massimi locali su una varietà compatta seguono una distribuzione di Weibull, permettendo un limite superiore statistico rigoroso.
• Scalabilità Senza Precedenti: Validazione empirica che l'approccio scala fino a 500 dimensioni per sistemi ODE densi e non strutturati, superando di gran lunga i limiti attuali delle pipeline di verifica formale.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su due fronti:

• Accuratezza (Benchmark 2D - Oscillatore di Van der Pol):
  • Confronto con metodi SOS esatti e verifiche SMT su reti neurali.
  • L'approccio SCORE, quando applicato a un candidato Lyapunov generato via SOS, ha certificato il 83% dell'area della ROA reale, rispetto al 95% ottenuto dall'SOS esatto. Questo dimostra che il metodo statistico è molto stretto e rigoroso, con la maggior parte della conservatività dovuta alla sintesi del candidato e non alla certificazione.
• Scalabilità (Sistemi ad Alta Dimensionalità):
  • Test su un sistema dissipativo lineare denso fino a $N=500$.
  • Confronto:
    • Metodi SMT + Reti Neurali (ICNN, PINN, NLF): Falliscono oltre $N=2$ o $N=10$.
    • SOS Classico: Fallisce a $N=20$.
    • SCORE (Proposto): Ha certificato con successo il sistema a 500 dimensioni entro un timeout di 10 minuti, con un livello di confidenza del 99.99%.

5. Significato e Impatto

Il lavoro di SCORE rappresenta un cambio di paradigma nella verifica formale dei sistemi di controllo:

• Superamento della Maledizione della Dimensionalità: Sposta il focus dalla risoluzione combinatoria esatta (impossibile per sistemi ad alta dimensione) alla stima statistica di limiti superiori rigorosi.
• Fattibilità Pratica: Permette di certificare sistemi complessi, densi e non strutturati (come quelli che appaiono nell'apprendimento automatico o nella dinamica dei fluidi) che erano precedentemente intrattabili per gli strumenti di verifica formale.
• Robustezza: Fornisce garanzie di sicurezza con un livello di confidenza quantificabile (es. 99.99%), offrendo un compromesso pratico e teoricamente fondato tra rigore matematico e scalabilità computazionale.

In sintesi, SCORE dimostra che è possibile ottenere certificazioni di sicurezza affidabili per sistemi ad altissima dimensionalità sfruttando le proprietà statistiche dei valori estremi, aprendo la strada alla verifica di sistemi critici moderni che i metodi deterministici non possono gestire.