Riepilogo Tecnico: Verifica Esatta delle Reti Neurali su Grafi con Risoluzione Incrementale di Vincoli

Enunciato del Problema

Le Reti Neurali su Grafi (GNN) sono sempre più impiegate in ambiti ad alto rischio come il rilevamento delle frodi, l'assistenza sanitaria e la guida autonoma. Tuttavia, come altre architetture neurali, sono vulnerabili ad attacchi avversari in cui lievi perturbazioni degli attributi dei nodi o della struttura del grafo (aggiunta/rimozione di archi) possono alterare le previsioni. Sebbene la verifica formale offra un metodo rigoroso per dimostrare la robustezza, le tecniche esistenti di verifica esatta per le GNN sono limitate. Nello specifico, i metodi attuali supportano principalmente solo l'aggregazione per somma e spesso limitano le perturbazioni strutturali alla sola rimozione di archi. Manca il supporto per altre funzioni di aggregazione comuni (massimo e media) e per l'aggiunta di archi, che sono fondamentali per modellare scenari di attacco reali e sono supportati da librerie standard come GraphSAGE. Inoltre, gli approcci esistenti spesso faticano con la scalabilità su grafi di grandi dimensioni a causa della rapida espansione delle codifiche dei vincoli.

Metodologia

Gli autori propongono GNNev, uno strumento di verifica esatta (corretto e completo) per le GNN basate sul passaggio di messaggi. Il metodo formula il compito di verifica della robustezza avversaria come un Problema di Soddisfacimento di Vincoli (CSP) e lo risolve utilizzando la Programmazione Intera Mista (MIP) con capacità di risoluzione incrementale.

1. Codifica CSP

Il compito di verifica è codificato per determinare se esiste una perturbazione ammissibile (entro budget specifici di attributi e strutturali) che causi un cambiamento nella previsione di un nodo target.

• Perturbazione di Input: La codifica modella le perturbazioni degli attributi tramite variabili a valori reali entro limiti definiti e le perturbazioni strutturali tramite variabili booleane che rappresentano l'aggiunta o la rimozione di archi.
• Architettura GNN: I livelli della rete sono codificati livello per livello. Gli autori estendono le codifiche MIP esistenti per supportare tre funzioni di aggregazione:
  • Somma: Codificata tramite vincoli lineari.
  • Massimo: Codificata utilizzando le capacità native del solver o vincoli big-M.
  • Media: Codificata utilizzando vincoli big-M per gestire la divisione per il grado variabile, che cambia in base alle perturbazioni degli archi.
• Obiettivo: L'obiettivo di verifica controlla se il margine nel caso peggiore tra la classe prevista e le altre classi può essere non positivo (ovvero, se una classificazione errata è fattibile).

2. Strategie di Raffinamento dei Limiti

Per migliorare l'efficienza del solver, gli autori introducono strategie specializzate di raffinamento dei limiti per le aggregazioni non lineari (massimo e media).

• Aggregazione Massimo: Il metodo calcola limiti superiori e inferiori stretti analizzando i casi in cui l'attaccante rimuove archi esistenti o ne aggiunge di nuovi entro il budget. Utilizza una selezione basata su heap per identificare in modo efficiente i limiti $k$-esimi più grandi/piccoli.
• Aggregazione Media: Il problema è ridotto a sottoproblemi in cui i budget di rimozione e inserimento sono fissati separatamente. Gli autori dimostrano che i limiti per questi sottoproblemi possono essere calcolati tramite scelte greedy e sfruttano la unimodalità della sequenza risultante per ottenere una complessità di $O((s+N)\log s)$, dove $s$ è il budget e $N$ è il numero di variabili.
• Garanzia Teorica: Il documento dimostra che questi limiti derivati sono stretti, il che significa che esistono insiemi di perturbazioni specifici che raggiungono esattamente questi limiti.

3. Algoritmo di Risoluzione Incrementale

Per affrontare il problema della scalabilità, in cui la codifica dell'intero vicinato di un nodo target porta a un'esplosione nel numero di variabili, gli autori adottano un approccio di risoluzione incrementale (Algoritmo 1).

• Invece di codificare l'intera rete a $K$ livelli in una sola volta, l'algoritmo inizia con l'obiettivo di verifica (ultimo livello) e aggiunge iterativamente vincoli per i livelli precedenti ($K-1, K-2, \dots$).
• Sfrutta le capacità di risoluzione incrementale dei moderni solver MIP (in particolare Gurobi), riutilizzando lo stato di ricerca e i tagli (vincoli ridondanti) generati nelle iterazioni precedenti.
• Questo approccio riduce significativamente la dimensione della codifica iniziale, in particolare per i compiti di classificazione dei nodi in cui il numero di vicini cresce esponenzialmente con la profondità.

Contributi Chiave

1. Prima Verifica Esatta per Aggregazioni Massimo/Media: Il documento introduce il primo metodo di verifica esatta per le GNN che supporta le funzioni di aggregazione massimo e media, oltre alla somma. Progetta strategie specializzate di propagazione di limiti raffinati per queste funzioni non lineari.
2. Risoluzione Incrementale di Vincoli: Gli autori propongono un algoritmo che codifica i livelli delle GNN all'indietro e utilizza la risoluzione incrementale per accelerare le prestazioni mantenendo l'esattezza. Ciò è particolarmente efficace per i compiti di classificazione dei nodi con grandi vicinati.
3. Verificatore Versatile (GNNev): L'implementazione di GNNev, che supporta sia la classificazione dei nodi che quella dei grafi, gestisce sia le perturbazioni degli attributi che quelle strutturali (inclusa l'aggiunta di archi) e si integra con PyTorch Geometric.
4. Valutazione Completa: Lo strumento è valutato su reti di citazione standard (Cora, CiteSeer), dataset reali di frodi (Amazon, Yelp) e dataset biochimici (MUTAG, ENZYMES).

Risultati Sperimentali

• Confronto con le Baseline: Sulle GNN con aggregazione per somma e rimozione di archi, GNNev supera SCIP-MPNN (l'unico verificatore esatto basato su MIP noto per questa configurazione) sia nel tempo di esecuzione che nel numero di compiti risolti su vari dataset e budget di perturbazione. Ad esempio, su CiteSeer, GNNev ha risolto compiti impegnativi per i quali SCIP-MPNN ha superato il limite di tempo.
• Prestazioni di Aggregazione: GNNev verifica con successo le GNN con aggregazioni massimo e media. Gli esperimenti mostrano che, sebbene l'aggregazione massimo diventi computazionalmente più difficile con budget più ampi (a causa delle sfide della codifica big-M), lo strumento rimane efficace.
• Insight sulla Robustezza: La valutazione rivela che le GNN con aggregazione media sono significativamente più vulnerabili alle perturbazioni avversarie rispetto alle varianti somma o massimo. Nei dataset di rilevamento delle frodi, la perturbazione di una singola dimensione dell'attributo ha portato a classificazioni errate in fino al 75,8% dei compiti per i modelli con aggregazione media.
• Studi di Ablazione: La rimozione dell'algoritmo di risoluzione incrementale o delle strategie di raffinamento dei limiti ha portato a tempi di esecuzione significativamente più lunghi e a un numero inferiore di compiti risolti, confermando l'efficacia di questi componenti.

Significato e Affermazioni

Il documento afferma che GNNev fornisce un metodo deterministico ed esatto per verificare la robustezza avversaria delle GNN, offrendo garanzie più forti rispetto ai metodi approssimati o probabilistici. Supportando le aggregazioni massimo e media e l'aggiunta di archi, affronta lacune critiche nel panorama attuale della verifica, consentendo l'analisi delle GNN utilizzate in librerie standard come GraphSAGE.

Gli autori sottolineano che il loro metodo è particolarmente prezioso per le applicazioni ad alto rischio (ad esempio, frodi finanziarie, diagnosi mediche) in cui risultati di verifica non conclusivi sono insufficienti. La capacità di identificare vulnerabilità specifiche (ad esempio, la suscettibilità dei modelli con aggregazione media) fornisce informazioni attuabili per sviluppatori e distributori di modelli. Il documento riconosce una limitazione: la complessità computazionale cresce con la dimensione dell'insieme di archi fragili, suggerendo lavori futuri su ricerche euristica e framework distribuiti per migliorare la scalabilità.