Riepilogo Tecnico: Stress-Testing dei Verificatori di Reti Neurali con Istanze Provabilmente Robuste

Enunciato del Problema

I verificatori di reti neurali sono progettati per fornire garanzie formali sul comportamento del modello, certificando specificamente che un modello addestrato si comporta in modo robusto sotto perturbazioni di input limitate. Tuttavia, la valutazione di tali verificatori è fondamentalmente limitata dalla mancanza di etichette di verità fondamentale (ground-truth labels) nei benchmark esistenti. Senza sapere a priori se un'istanza di verifica è realmente robusta o non robusta, la valutazione si affida a euristiche indirette, come il voto di maggioranza tra i verificatori o l'assunzione di correttezza quando non viene trovato alcun controesempio. Questo approccio impedisce una valutazione esatta, oscura specifici modi di fallimento e rende difficile stress-testare sistematicamente i verificatori su istanze sempre più difficili. Inoltre, i benchmark attuali offrono informazioni diagnostiche limitate riguardo al perché un verificatore fallisce (ad esempio, a causa di rilassamenti lassi, geometria locale complessa o problemi numerici).

Metodologia

Gli autori introducono VeriStress-GT (Stress-Testing del Verificatore tramite Verità Fondamentale), un framework modulare per generare istanze di verifica di reti neurali con etichette di verità fondamentale di robustezza provate analiticamente. A differenza dei benchmark tradizionali che si basano sull'addestramento di modelli su dataset, VeriStress-GT costruisce istanze in cui la robustezza è garantita dalla costruzione matematica.

1. Costruzioni Robuste

Il framework definisce una collezione di "costruttori", ciascuno mirato a classi architetturali specifiche o a colli di bottiglia dei verificatori. Questi costruttori generano istanze in cui l'etichetta di verità fondamentale è nota a priori:

• Costruttori di Reti ReLU:
  • Raggio Esatto tramite MILP: Calcola il raggio esatto di robustezza utilizzando la Programmazione Lineare Intera Mista per creare istanze robuste vicine al confine.
  • Incorporamento Costante su Box: Costruisce reti in cui uno strato latente intermedio è costante sull'insieme delle perturbazioni, garantendo la robustezza indipendentemente dalla complessità a valle.
  • Pattern di Attivazione Mutualmente Esclusivi (MEAP): Crea coppie di neuroni che sono individualmente instabili (che passano da attivi a inattivi) ma accoppiati in modo tale che almeno uno sia sempre attivo, costringendo i verificatori a gestire dipendenze complesse dei pattern di attivazione.
  • Stress dell'Angolo di Input: Genera istanze in cui la robustezza dipende dalla convessità della funzione di margine, richiedendo la verifica agli angoli del box di perturbazione piuttosto che attraverso rilassamenti locali.
• Costruttori CNN:
  • CNN Contrattiva Profonda: Forza le perturbazioni a contrarsi attraverso la profondità utilizzando blocchi convoluzionali vincolati da Lipschitz.
  • CNN a Bias Accoppiati: Un analogo convoluzionale del MEAP, in cui canali accoppiati condividono filtri ma hanno bias ordinati, garantendo una differenza non negativa nonostante l'instabilità individuale.
• Costruttori di Moduli di Attenzione:
  • Attenzione Softmax a Ordine Fisso: Certifica la robustezza assicurando che l'ordinamento dei punteggi delle teste di attenzione rimanga stabile sotto perturbazione.
  • Attenzione Lineare a Chiave Dominante: Impone una chiave dominante nei meccanismi di attenzione lineare, limitando la deriva dell'output di attenzione.
• Costruttore di Reti Polinomiali: Genera istanze controllando esplicitamente la geometria del confine decisionale (una ipersuperficie algebrica reale) e posizionando l'input vicino a questo confine con un buffer noto.

2. Profilo di Difficoltà dell'Istanza di Verifica

Per analizzare sistematicamente le prestazioni del verificatore, gli autori propongono il Profilo di Difficoltà, una tupla di cinque quantità stimabili che caratterizzano la durezza dell'istanza indipendentemente da qualsiasi verificatore specifico:

1. Margine Minimo ($\hat{M}_{min}$): Una stima empirica della prossimità a un controesempio tramite campionamento.
2. Gap Relativo IBP ($G_{IBP}$): Misura la lassità della Propagazione dei Confini di Intervallo (IBP) rispetto al margine empirico.
3. Frazione Instabile ($U$): La frazione di unità non lineari il cui stato di attivazione è ambiguo sull'insieme di input.
4. Complessità della Regione Locale ($A_\tau$): Stima il numero di comportamenti affini locali distinti (o approssimazioni di Taylor) necessari per coprire il paesaggio del margine sull'insieme delle perturbazioni.
5. Dimensionalità Effettiva del Gradiente ($d_{eff}$): Misura quanto è distribuita la sensibilità del margine attraverso le coordinate di input (correlata al Rapporto di Partecipazione).

Contributi Chiave

1. Framework VeriStress-GT: Il primo framework riutilizzabile per generare istanze di verifica di reti neurali con etichette di verità fondamentale indipendenti dal verificatore e parametri di difficoltà controllabili.
2. Profilo di Difficoltà: Un framework unificato per caratterizzare la durezza delle istanze di verifica, consentendo la valutazione sistematica della scalabilità e dei modi di fallimento del verificatore oltre le semplici metriche di runtime.
3. Valutazione Empirica: Una valutazione completa di cinque verificatori all'avanguardia (inclusi $\alpha,\beta$-CROWN, Marabou, NeuralSAT, PyRAT e nnenum) utilizzando il nuovo framework.

Risultati

La valutazione di cinque verificatori all'avanguardia su 225 istanze VeriStress-GT e benchmark esterni (MNIST_fc, oval21) ha prodotto tre scoperte principali:

1. Rivelazione di Affermazioni Errate: Le etichette di verità fondamentale hanno esposto che più verificatori hanno restituito affermazioni di robustezza false (SAT) su istanze che erano analiticamente robuste (UNSAT). Questi errori sono stati attribuiti in gran parte a limitazioni della tolleranza numerica. Inoltre, i test con istanze provatamente non robuste hanno rivelato un bug specifico nell'implementazione di un verificatore popolare riguardante i vincoli di output disgiuntivi, che è stato successivamente corretto.
2. Timeout Diagnostici: Il Profilo di Difficoltà ha trasformato esiti di timeout opachi in modi di fallimento diagnosticabili. Ad esempio, valori elevati di $G_{IBP}$ si sono correlati a fallimenti dovuti a un'estrema lassità del rilassamento degli intervalli, mentre valori elevati di $d_{eff}$ si sono correlati a timeout in scenari di sensibilità del margine ad alta dimensionalità.
3. Stress-Testing Mirato: Diversi costruttori hanno isolato modi di fallimento distinti. Le istanze MEAP hanno messo sotto stress le decisioni di diramazione e l'ambiguità dei pattern di attivazione, mentre le istanze Input-Corner hanno isolato la lassità del rilassamento dalla complessità della regione non lineare. Questo permette agli sviluppatori di mirare a miglioramenti specifici (ad esempio, rilassamenti più stretti rispetto a euristiche di diramazione migliori).

Significato e Affermazioni

Il documento afferma di riproporre il benchmarking della verifica da una valutazione euristica a sperimentazione controllata basata sulla verità fondamentale. Fornendo istanze con etichette note, il framework:

• Consente il rilevamento di bug nell'implementazione e instabilità numeriche che altrimenti sarebbero mascherate da una valutazione basata sul consenso.
• Fornisce obiettivi azionabili per migliorare aspetti specifici della pipeline di verifica, come l'affidabilità numerica, la qualità del rilassamento e il comportamento di ricerca.
• Offre un modo sistematico per studiare i modi di fallimento del verificatore correlando componenti specifici del profilo di difficoltà con le prestazioni del verificatore.

Gli autori sottolineano che, sebbene il framework esponga limitazioni nei verificatori attuali, funge anche da strumento per guidare lo sviluppo futuro verso sistemi di verifica più robusti e affidabili. Il codice e i dataset sono disponibili pubblicamente per facilitare questa ricerca in corso.