Sintesi Tecnica: Veriphi – Verifica di Reti Neurali Guidata da Attacchi con Metodi di Addestramento Dipendenti dal Dataset

1. Definizione del Problema

L'impiego del deep learning in domini critici per la sicurezza richiede una verifica robusta delle reti neurali. Sebbene l'addestramento avversario (es. PGD) offra una robustezza empirica, esso manca di garanzie formali. Al contrario, i metodi di addestramento certificato (es. Interval Bound Propagation, IBP) forniscono prove matematiche di robustezza, ma spesso faticano con la scalabilità e l'accuratezza su dataset complessi.

Esiste una lacuna critica nella letteratura riguardante la selezione del metodo: i professionisti mancano di orientamento su se dare priorità all'addestramento certificato o all'addestramento avversario per specifici contesti problematici. Inoltre, gli strumenti di verifica esistenti spesso affrontano sfide nel bilanciare l'efficienza computazionale con la necessità di limiti formali, in particolare quando si passa dai benchmark accademici a modelli di dimensioni produttive.

2. Metodologia: Il Framework Veriphi

Gli autori presentano Veriphi, un sistema di verifica accelerato tramite GPU progettato per affrontare queste sfide attraverso una strategia a due fasi e una valutazione sistematica delle metodologie di addestramento.

2.1 Architettura di Verifica

Veriphi impiega una strategia di verifica guidata dall'attacco composta da due fasi:

1. Falsificazione Rapida (Fase 1): Il sistema tenta prima di trovare controesempi utilizzando attacchi avversari rapidi (FGSM e I-FGSM) con un timeout configurabile (default 10s). Se un attacco riesce a falsificare l'output della rete, il processo termina immediatamente con un risultato "FALSIFIED", bypassando la verifica formale costosa.
2. Verifica Formale (Fase 2): Se la fase di attacco fallisce nel trovare un controesempio, il sistema invoca il framework $\alpha, \beta$-CROWN (tramite la libreria auto-LiRPA) per calcolare i limiti certificati. Una rete è verificata se il limite inferiore della classe vera supera i limiti superiori di tutte le altre classi entro il budget di perturbazione $\epsilon$ nella norma $L_\infty$.

2.2 Metodologie di Addestramento

Lo studio confronta sistematicamente tre approcci di addestramento:

• Baseline: Minimizzazione standard della cross-entropy.
• Addestramento Avversario PGD: Ottimizza la perdita nel caso peggiore su un budget di perturbazione utilizzando la Projected Gradient Descent.
• Addestramento Certificato IBP: Ottimizza un limite esterno convesso della perdita utilizzando l'Interval Bound Propagation, con un fattore di ponderazione $\kappa$ che aumenta linearmente durante l'addestramento.

2.3 Architettura del Modello e Setup Sperimentale

Gli esperimenti utilizzano Modelli Ricorsivi Tiny (TRM-MLP), un'architettura favorevole alla verifica caratterizzata da attivazioni ReLU e operazioni lineari senza batch normalization.

• Dataset: MNIST (semplice, 784 dimensioni) e CIFAR-10 (complesso, 3.072 dimensioni).
• Scala di Produzione: Un problema reale di ottimizzazione della logistica aerospaziale (Airbus Beluga) che coinvolge un modello da 105,8 milioni di parametri.
• Hardware: Supercomputer VSC-5 con dual GPU A100.

3. Risultati Chiave

3.1 Efficacia dell'Addestramento Dipendente dal Dataset

Il risultato più significativo è che l'efficacia dei metodi di addestramento è fondamentalmente dipendente dalla complessità del dataset:

• Dataset Semplici (MNIST): L'addestramento certificato IBP supera significativamente l'addestramento avversario. A $\epsilon = 0,06$, IBP raggiunge un'accuratezza verificata del 77% rispetto al 63% di PGD.
• Dataset Complessi (CIFAR-10): L'addestramento IBP non riesce a fornire una certificazione significativa, raggiungendo solo l'1% di accuratezza verificata a $\epsilon \geq 0,006$, mentre l'addestramento avversario PGD mantiene prestazioni elevate (58–94%).
• Interpretazione: Gli autori attribuiscono il fallimento di IBP su CIFAR-10 all'accumulo di errori di sovra-approssimazione nell'aritmetica degli intervalli all'aumentare della dimensionalità dell'input (da 784 a 3.072), portando a limiti vacui. PGD, essendo empirico, rimane robusto a questo aumento di dimensionalità.

3.2 Efficienza della Verifica

L'approccio guidato dall'attacco produce miglioramenti sostanziali di velocità:

• Accelerazione GPU di 5,5×: Falsificando i campioni vulnerabili precocemente (in <0,1s), il sistema riduce il tempo medio di verifica da 1,21s (formale puro) a 0,22s.
• Terminazione Anticipata: Su MNIST con $\epsilon=0,1$, gli attacchi falsificano con successo il 40% dei campioni, evitando completamente la verifica formale per tali casi.

3.3 Confronto tra Metodi di Limite (Bound)

Un confronto tra CROWN, $\alpha$-CROWN e $\beta$-CROWN rivela rendimenti decrescenti:

• Limiti più stretti ($\alpha, \beta$-CROWN) forniscono meno del 5% di miglioramento nell'accuratezza verificata rispetto allo standard CROWN.
• Questo miglioramento comporta un aumento del 20–30% del tempo di calcolo, suggerendo che lo standard CROWN offre il miglior compromesso tra accuratezza ed efficienza per applicazioni pratiche.

3.4 Validazione su Scala di Produzione

Veriphi è stato scalato con successo a un modello da 105,8 milioni di parametri per la logistica aerospaziale Airbus Beluga.

• Il sistema ha verificato la soddisfazione dei vincoli (capacità di volo, capacità del rack, vincoli temporali) sotto perturbazioni dei parametri del 5%.
• Ha raggiunto un tasso di robustezza verificata del 40% sui problemi campionati con un tempo medio di verifica di 2,6 secondi per problema, dimostrando l'applicabilità oltre i benchmark accademici.

4. Significato e Rivendicazioni

Il paper sostiene che sfida l'assunto prevalente secondo cui l'addestramento certificato supera universalmente l'addestramento avversario. Invece, pone l'accento sul fatto che il contesto è critico:

• Per dataset semplici e a bassa dimensionalità: L'addestramento certificato (IBP) è superiore per ottenere una robustezza verificabile.
• Per dataset complessi e ad alta dimensionalità: L'addestramento avversario (PGD) è più efficace per ottenere tassi di certificazione significativi, poiché i limiti di IBP diventano troppo ampi per essere utili.

Gli autori sottolineano che il loro lavoro fornisce il primo confronto sistematico che stabilisce la complessità del dataset come fattore primario per la selezione del metodo. Inoltre, l'integrazione della falsificazione guidata dall'attacco con la verifica formale offre una via pratica per scalare la verifica a modelli di dimensioni produttive, colmando il divario tra garanzie teoriche e implementazione nel mondo reale nella logistica aerospaziale critica per la sicurezza.

Il paper conclude che, sebbene i limiti più stretti ($\alpha, \beta$-CROWN) offrano guadagni marginali, la combinazione di robustezza empirica (PGD) con la certificazione selettiva su sottospazi a bassa dimensionalità potrebbe rappresentare la direzione più pratica per il futuro, un'ipotesi lasciata alla futura esplorazione.