Sintesi Tecnica: Zonotopi Differenziali per la Verifica della Robustezza Globale delle DNN

1. Definizione del Problema

Le Reti Neurali Profonde (DNN) sono sempre più impiegate in domini critici per la sicurezza, come il trasporto e l'assistenza sanitaria, dove la loro robustezza rispetto alle perturbazioni degli input è essenziale. Mentre la robustezza locale (garantire che le predizioni non cambino per piccole perturbazioni attorno a un input specifico) è una proprietà di sicurezza ben studiata, la robustità globale è un requisito strettamente più forte. La robustezza globale richiede che per tutte le coppie di input entro una certa distanza, le predizioni del modello rimangano coerenti.

Formalmente, la robustezza globale è una proprietà di 2-sicurezza, che richiede la verifica di una relazione tra due tracce di esecuzione universalmente quantificate, piuttosto che una singola traccia. Questa complessità rende la verifica globale significativamente più difficile rispetto alla verifica locale. I metodi esistenti per la robustezza globale basata sulla confidenza (che limita le garanzie alle predizioni ad alta confidenza per evitare i confini decisionali) si affidano a solver di soddisfacibilità specializzati ma soffrono di scarsa scalabilità, essendo attualmente limitati a reti con solo decine di neuroni.

2. Metodologia

Il lavoro propone un nuovo framework di analisi statica basato su zonotopi a alone differenziale per verificare efficientemente la robustezza globale.

2.1 Zonotopi a Alone Differenziale

L'innovazione tecnica centrale è l'estensione del dominio astratto dello zonotopo. Gli zonotopi standard rappresentano insiemi di punti tramite un centro e una matrice di generatori. Per verificare la robustezza globale, gli autori devono tracciare simultaneamente due esecuzioni della stessa DNN con input diversi.

• Sfida: Le adattamenti ingenui dei zonotopi differenziali (precedentemente utilizzati per la verifica di equivalenza delle DNN dove gli input sono identici) falliscono per la robustezza globale. Inizializzare gli input come identici o utilizzare generatori completamente indipendenti porta a una mancanza di correttezza (unsoundness) o a un eccessivo sovrastima (perdita di precisione).
• Soluzione: Gli autori introducono le forme affini a alone differenziale. Questa codifica distribuisce il limite di perturbazione $\epsilon$ tra due generatori:
  1. Un generatore primario condiviso tra le due esecuzioni per mantenere la correlazione.
  2. Generatori secondari che sono indipendenti per ciascuna esecuzione per modellare la perturbazione.
• Meccanismo: Questa struttura a "alone" permette al sistema di codificare in modo corretto e preciso la condizione per cui due input $x$ e $y$ si trovano all'interno di un bounding box $[l, u]$ e soddisfano $|x - y| \le \epsilon$. Lo zonotopo differenziale $\mathcal{Z}_\Delta$ traccia la differenza tra le esecuzioni in sincronia, producendo limiti più stretti sulla divergenza rispetto alla sottrazione di singoli zonotopi.

2.2 Robustezza Globale Simmetrica Basata sulla Confidenza

Il documento identifica un limite nella definizione esistente di robustezza globale basata sulla confidenza (la variante asimmetrica), che richiede che un input ad alta confidenza $x$ non possa essere perturbato in una classe diversa $y$, indipendentemente dalla confidenza di $y$. Gli autori sostengono che questo sia eccessivamente restrittivo, poiché una perturbazione che porta a una predizione diversa ma a bassa confidenza è praticamente accettabile (ad esempio, attivando una revisione manuale).

Propongono una variante simmetrica:

• Definizione: Per qualsiasi coppia di input $x, y$ entro la distanza $\epsilon$, se entrambi sono classificati con una confidenza superiore a una soglia $\tau$, devono appartenere alla stessa classe.
• Vantaggio: Questa rilassamento ammette una classe più ampia di reti come "robuste", pur rimanendo significativo per le applicazioni critiche per la sicurezza dove gli output a bassa confidenza vengono gestiti tramite meccanismi di fallback.

2.3 Algoritmo di Verifica

Il processo di verifica (implementato nello strumento TwoSafe) segue questi passaggi:

1. Inizializzazione: Costruzione di uno zonotopo a alone differenziale che rappresenta lo spazio di input e i vincoli di perturbazione.
2. Propagazione: Propagazione dello zonotopo attraverso i livelli della DNN. Per le attivazioni ReLU, il metodo introduce nuovi generatori per sovrastimare la non linearità, mantenendo la struttura differenziale.
3. Controllo della Proprietà: All'output, il sistema formula un problema di Programmazione Lineare (LP) per verificare se esistono coppie di output in cui le classi differiscono mentre entrambe soddisfano la soglia di confidenza $\tau$.
4. Raffinamento: Se il controllo è inconcludente (a causa della sovrastima), l'algoritmo esegue lo splitting dei generatori. A differenza dello splitting standard dell'input, questo divide i generatori dello zonotopo a alone differenziale per raffinare l'approssimazione senza perdere la copertura dello spazio di perturbazione.

3. Contributi Chiave

1. Zonotopi a Alone Differenziale: Un nuovo dominio astratto che estende gli zonotopi per propagare congiuntamente coppie di input perturbati in sincronia, delimitando strettamente la loro divergenza. Ciò consente la verifica di proprietà di 2-sicurezza con una precisione maggiore rispetto all'analisi individuale.
2. Robustezza Globale Simmetrica Basata sulla Confidenza: Una nuova definizione di robustezza globale che richiede coerenza solo tra predizioni ad alta confidenza. Questa definizione è strettamente meno restrittiva della variante asimmetrica e permette una verifica efficiente all'interno del framework proposto.
3. Prova di Correttezza (Soundness): Una prova formale della correttezza dell'analisi statica basata sugli zonotopi differenziali, con i risultati principali formalizzati in Isabelle.
4. Strumento TwoSafe ed Valutazione: Implementazione dell'approccio in un nuovo strumento, TwoSafe, che supera significativamente lo stato dell'arte (baseline CGR) sia in precisione che in scalabilità.

4. Risultati Sperimentali

Gli autori hanno valutato TwoSafe su quattro benchmark: Law (piccolo), LHC (classificazione delle particelle), ACAS Xu (evitamento collisioni) e HAR (riconoscimento dell'attività umana).

• Scalabilità: TwoSafe ha verificato con successo la robustezza globale su reti con fino a 500 neuroni ReLU e 561 dimensioni di input (benchmark HAR). Al contrario, la baseline (CGR) ha subito timeout o esaurimento della memoria su queste reti più grandi.
• Precisione: La baseline ha spesso riportato controesempi spurii a causa di approssimazioni grossolane della softmax, particolarmente su reti con molte classi di output. TwoSafe ha evitato questi falsi positivi.
• Prestazioni: TwoSafe ha dimostrato incrementi di velocità significativi. Ad esempio, sul benchmark LHC, ha verificato la robustezza in meno di 3 secondi, laddove la baseline andava in timeout dopo 2 ore.
• Simmetrica vs Asimmetrica: La proprietà simmetrica ha permesso la verifica riuscita in regimi di parametri in cui la proprietà asimmetrica era inconcludente o falliva. Ad esempio, sul benchmark HAR con $\epsilon=0.01$, la proprietà simmetrica era verificabile mentre la variante asimmetrica andava in timeout.

5. Significato e Rivendicazioni

Il lavoro sostiene di aver risolto la tensione intrinseca tra la forza delle garanzie di robustezza e la scalabilità degli strumenti di verifica. Passando dalla verifica della robustezza locale a quella globale e utilizzando gli zonotopi a alone differenziale, gli autori dimostrano che è possibile verificare reti significativamente più ampie e profonde di quanto precedentemente possibile.

L'introduzione della robustezza globale simmetrica basata sulla confidenza è presentata come un avanzamento pratico, offrendo una "nozione significativa di robustezza" che si applica a una classe più ampia di reti, riconoscendo che le predizioni a bassa confidenza sono spesso gestite diversamente nei sistemi reali. Il lavoro stabilisce che la verifica differenziale, quando adattata alle proprietà di 2-sicurezza, può scalare a reti di un ordine di grandezza più grandi rispetto a quelle gestite dalle tecniche precedenti, rendendo la certificazione della robustezza globale fattibile per modelli implementati nel mondo reale.