Repair Instead of Retraining: A Constraint-Guided Framework for Neural Network Repair

Sintesi Tecnica: Riparare invece di Riqualificare: Un Framework Guidato da Vincoli per la Riparazione di Reti Neurali

Problematica
Le reti neurali profonde (DNN) impiegate in applicazioni critiche per la sicurezza rimangono vulnerabili a perturbazioni avversarie e attacchi backdoor. Sebbene il riaddestramento o il fine-tuning possano mitigare tali problemi, questi approcci sono computazionalmente costosi, difficili da applicare selettivamente a modelli già distribuiti e rischiano di introdurre un deriva comportamentale incontrollabile oltre il difetto specifico osservato. I metodi di riparazione esistenti spesso si affidano a ricerche euristiche (grey-box) con interpretabilità limitata o richiedono trasformazioni architettoniche formali e vincoli politoipici specificati manualmente (metodi provabili) che faticano con la scalabilità. È necessario un approccio di riparazione post-hoc che bilanci interpretabilità, fedeltà comportamentale e costo computazionale senza un riaddestramento completo.

Metodologia
Gli autori propongono un framework configurabile e guidato da vincoli che tratta la riparazione di reti neurali come un problema di ottimizzazione consapevole della logica su un insieme sparso di parametri localizzati. Il framework opera in quattro fasi accoppiate:

1. Localizzazione del Difetto: Il sistema utilizza DeepSHAP per calcolare maschere di attribuzione a livello di neurone sia per input benigni che avversari. Identifica i neuroni "solo-attacco" — quelli con alta attribuzione sotto input avversari ma bassa attribuzione sotto input benigni. Questa attribuzione contrastiva funge da segnale per localizzare l'insieme sparso di pesi rilevanti per il difetto.
2. Selezione del Target di Riparazione: Una maschera binaria sparsa ($\Theta_S$) viene generata sui parametri della rete basandosi sui neuroni localizzati. Il framework esplora uno spazio di progettazione definito da:
   • Direzione del Peso: Modifica dei pesi in entrata, dei pesi in uscita o dei bias dei neuroni critici.
   • Politica di Selezione: Selezione dei pesi tramite soglie percentili (es. top 5% per magnitudo) o budget fissi casuali ($k$).
3. Specificazione dei Vincoli di Percorso: L'intento di riparazione è codificato come vincoli a livello di percorso tramite esecuzione concolica (tramite PyCT).
   • Vincoli Hard: Derivati da tracce benigne per preservare la corretta logica di branching interna.
   • Vincoli Soft: Derivati da tracce avversarie per forzare il modello a reindirizzare l'esecuzione lontano dai percorsi difettosi osservati.
   • Reti Surrogate: Per affrontare l'intrattabilità di codificare reti su scala completa in solver Max-SMT, il framework introduce due surrogate di analisi:
     • $N^\Delta_w$ (Surrogate Ternaria): Mappa i pesi non soggetti a riparazione in $\{-1, 0, +1\}$ in base alla magnitudo, riducendo la complessità della formula.
     • $N^\Delta_i$ (Surrogate con Gate di Attivazione): Potatura degli archi non soggetti a riparazione in base alla magnitudo dell'attivazione dell'input.
   • Crucialmente, i pesi da riparare ($\Theta_S$) rimangono incognite simboliche esatte in tutte le formulazioni, mentre le componenti non soggette a riparazione sono semplificate o filtrate.
4. Riparazione Guidata da Vincoli e Validazione: Il sistema risolve un problema Top-K Max-SMT (usando Z3) per sintetizzare aggiornamenti dei pesi candidati. I candidati sono classificati in base a un punteggio bilanciato calcolato tramite validazione fedele sulla rete originale distribuita $N$ (usando operazioni affini esatte), garantendo che i parametri riportati riflettano il reale comportamento a runtime piuttosto che artefatti delle surrogate.

Contributi Chiave

• Framework Configurabile Consapevole della Logica: Una pipeline unificata che combina localizzazione DeepSHAP, estrazione di vincoli di percorso concolici, surrogate ternarie/con gate di attivazione e ottimizzazione Max-SMT.
• Spazio di Progettazione della Riparazione Formalizzato: Gli autori caratterizzano esplicitamente l'interazione tra sorgente del neurone (solo-attacco vs intersezione), direzione del peso (in entrata, in uscita, bias) e politiche di selezione per colonna, dimostrando che non esiste una singola "ricetta" universalmente ottimale.
• Semplificazioni Rigide in Fase di Codifica: Tecniche come l'eliminazione delle sottoespressioni comuni, la normalizzazione della negazione e la potatura delle espressioni sono introdotte per mantenere trattabili i vincoli concolici per il Max-SMT senza alterare la semantica della riparazione.
• Formulazioni Surrogate: L'introduzione di $N^\Delta_w$ e $N^\Delta_i$ permette di raccogliere vincoli di percorso su modelli semplificati mantenendo una rappresentazione simbolica esatta per le variabili di riparazione.
• Protocollo di Validazione Fedele: Un metodo di valutazione rigoroso in cui tutti i parametri di accuratezza e tassi di successo dell'attacco (ASR) sono misurati sulla rete originale $N$, disaccoppiando la raccolta dei vincoli dalla valutazione finale delle prestazioni.

Risultati Sperimentali
Il framework è stato valutato attraverso 4.737 esecuzioni su sei benchmark (Fashion-MNIST, MNIST-BD, CIFAR-10, GTSRB, MNIST-6 e ResNet18). Le scoperte chiave includono:

• Benchmark Backdoor: Su Fashion-MNIST e MNIST-BD, il framework ha ottenuto una rimozione quasi completa della backdoor. Nello specifico, l'ASR è sceso da >98% a <8% (es. 99,77% $\to$ 6,66% su Fashion-MNIST) preservando o migliorando leggermente l'accuratezza pulita. La configurazione più efficace ha utilizzato la modifica del peso in uscita con la surrogate con gate di attivazione ($N^\Delta_i$).
• Benchmark Avversari: Una scoperta critica è stata l'efficacia della riparazione solo del bias. Su MNIST-6, la riparazione della direzione del bias ha ridotto l'ASR dal 100% al 5,81% preservando il 100% dell'accuratezza pulita. Su ResNet18, ha ridotto l'ASR dall'85,51% al 40,42%. Questa direzione era precedentemente inesplorata e sarebbe stata ignorata da metodi focalizzati esclusivamente su pesi in entrata o in uscita.
• Limiti di Scalabilità: CIFAR-10 e GTSRB si sono rivelati impegnativi sotto riparazione a singolo strato. Sebbene siano stati osservati miglioramenti parziali, GTSRB ha mostrato una riduzione minima dell'ASR, evidenziando un compromesso tra trattabilità e fedeltà in cui i vincoli a singolo strato sono insufficienti per difetti complessi e distribuiti.
• Confronto con CARE: Rispetto al metodo grey-box CARE (localizzazione basata su causalità + PSO), il framework proposto ha generalmente ottenuto un ASR inferiore e una migliore preservazione dell'accuratezza pulita su Fashion-MNIST e MNIST-BD, con tempi di esecuzione significativamente inferiori (es. 74,4s vs 8.745s su MNIST-BD). Tuttavia, CARE ha ottenuto la rimozione completa della backdoor su GTSRB, suggerendo che l'ambito a singolo strato del metodo proposto sia un fattore limitante per certe architetture.

Significatività e Rivendicazioni
Il paper sostiene che l'esplorazione sistematica dello spazio di progettazione della riparazione sia essenziale per scoprire configurazioni efficaci, poiché nessuna euristica domina in tutti gli scenari. Gli autori sottolineano che la riparazione della direzione del bias è un'opzione critica, precedentemente inesplorata, per la correzione avversaria, scopribile solo attraverso questo approccio sistematico.

Il lavoro si posiziona come una via di mezzo tra la ricerca euristica e la verifica formale: offre maggiore interpretabilità e controllo logico rispetto ai metodi grey-box senza richiedere le trasformazioni architettoniche o i politoipi specificati manualmente dei sistemi di riparazione provabili. Gli autori riconoscono con modestia che il loro framework è guidato da vincoli ma non formalmente certificato; sebbene utilizzi il Max-SMT per la sintesi, le garanzie finali sono empiriche, basate sulla validazione fedele sulla rete di distribuzione piuttosto che su prove formali sull'intero spazio di input. I risultati evidenziano un compromesso fondamentale tra trattabilità e fedeltà: semplificazioni più forti (maggiore $\Delta$ nelle surrogate) riducono il tempo di esecuzione del solver ma possono distorcere la guida alla riparazione se non calibrate correttamente.