Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

Riepilogo Tecnico: Compilazione SMT di Piccoli Operatori Neurali di Fourier

Enunciato del Problema
Gli Operatori Neurali di Fourier (FNO) offrono un'accelerazione significativa per le simulazioni di Equazioni alle Derivate Parziali (PDE), ma spesso mancano di garanzie formali riguardo ai vincoli fisici, come la conservazione della massa o la positività delle concentrazioni. Sebbene la validazione standard si basi su test Monte Carlo (MC) o falsificazione basata su gradienti, questi metodi campionano solo input specifici e non possono fornire garanzie esaustive su regioni di input continue. Gli strumenti esistenti di verifica delle reti neurali sono progettati principalmente per classificatori o politiche di controllo e non gestiscono nativamente le convoluzioni spettrali, gli input nello spazio delle funzioni o le proprietà specifiche delle PDE come le leggi di conservazione.

Metodologia
Gli autori propongono di compilare FNO addestrati in risolutori Satisfiability Modulo Theories (SMT), specificamente Z3, per abilitare la verifica formale. L'idea centrale è che, su una griglia fissa con pesi addestrati fissi, la convoluzione spettrale in un FNO è una mappa lineare. Di conseguenza, un FNO con non linearità ReLU è una mappa lineare a tratti che può essere rappresentata esattamente nell'aritmetica lineare reale di Z3 senza approssimare il passaggio in avanti.

La metodologia coinvolge due strategie di codifica principali:

1. Codifica Esatta: La convoluzione spettrale viene compilata in una matrice densa esplicita ($W^{spec}$) applicando l'operazione ai vettori della base standard. L'intero passaggio in avanti è rappresentato come una composizione di mappe affini e funzioni ReLU coordinate per coordinate. Questa codifica è corretta (sound), il che significa che un risultato "UNSAT" prova che la proprietà vale per tutti gli input ammissibili, e un risultato "SAT" fornisce un controesempio valido. Tuttavia, la complessità scala come $O(N^2H^2L)$, limitandola a dimensioni di griglia piccole ($N \le 32$).
2. Codifica Congelata (Frozen): Per scalare a griglie più grandi ($N \le 64$), il percorso spettrale viene sostituito con una costante derivata da un input di riferimento. Questo riduce la complessità a $O(NH^2L)$ e abilita controlli in meno di un secondo. Tuttavia, si tratta di un'approssimazione; i risultati "UNSAT" certificano solo il surrogato congelato, non l'FNO originale, e i risultati "SAT" richiedono una convalida sul modello originale.

Gli esperimenti si concentrano su equazioni di advezione-diffusione-reazione (ADR) 1D con condizioni al contorno periodiche. Lo studio verifica due proprietà:

• Non Aumento della Massa: Verifica se la massa discreta dell'output supera la massa di input di una tolleranza $\epsilon = 0.05$.
• Positività: Verifica se input non negativi producono output non negativi in tutti i punti della griglia.

Contributi Chiave

• Compilazione Esatta: Il paper presenta la prima compilazione esatta di FNO su griglia fissa nell'aritmetica lineare reale di Z3 costruendo matrici spettrali esplicite.
• Prime Prove Formali: Fornisce le prime prove formali corrette per un operatore neurale di PDE, generando specificamente certificati di positività per FNO lineari (senza ReLU) a dimensioni di griglia fino a 16.
• Analisi Comparativa: Il lavoro confronta Z3 con la falsificazione basata su gradienti e i test Monte Carlo su 10 modelli piccoli (85–117 parametri).
• Confine Correttezza-Scalabilità: Gli autori caratterizzano il compromesso tra verifica esatta e scalabilità, dimostrando che le codifiche esatte supportano prove per modelli lineari piccoli e controesempi per modelli ReLU moderati, mentre le codifiche approssimate scalano ulteriormente ma perdono la correttezza formale per il modello originale.

Risultati

• Non Aumento della Massa: Utilizzando la codifica esatta, Z3 ha trovato controesempi validi di violazione della massa per tutti i 10 modelli. Su 7 dei 10 modelli, Z3 ha scoperto violazioni più gravi sia rispetto alla falsificazione basata su gradienti che ai test MC. Per i modelli lineari, Z3 ha ottimizzato globalmente per trovare violazioni più profonde; per i modelli ReLU, la ricerca basata su gradienti è rimasta competitiva.
• Positività:
  • Modelli Lineari (L=1): Z3 ha prodotto 2 prove di positività corrette (per dimensioni di griglia $N=8$ e $N=16$) e ha trovato 4 controesempi corretti su altri modelli lineari.
  • Modelli ReLU (L=2): Z3 ha trovato 1 controesempio corretto ma ha superato il tempo limite sulle rimanenti 3 query di positività a causa dell'esplosione combinatoria dei pattern di attivazione ($2^{NH}$). La falsificazione basata su gradienti ha trovato con successo violazioni su tutti i 4 modelli ReLU, spesso con maggiore gravità rispetto a Z3.
• Codifica Congelata: Questo approccio ha verificato con successo la positività su 8 modelli più grandi ($N=32$ a $64$) e ha trovato controesempi di massa su 4 di essi. Tuttavia, questi risultati sono approssimativi; le prove di positività si applicano solo al surrogato congelato e i controesempi di massa hanno richiesto una ricontrolla sul modello originale (3 confermati, 1 non confermato).

Significato e Affermazioni
Il paper si posiziona come una prova di concetto piuttosto che come una soluzione per la verifica su scala produttiva. Gli autori affermano esplicitamente che i loro risultati non risolvono la verifica degli FNO su larga scala; i modelli testati sono di "dimensione giocattolo" con strati nascosti congelati e parametri limitati.

Il significato risiede nel dimostrare che:

1. Gli FNO possono essere compilati esattamente in forme lineari a tratti, abilitando l'uso di risolutori SMT per proprietà motivate dalla fisica.
2. La verifica formale è fattibile per piccoli operatori neurali lineari, producendo i primi certificati corretti per tali sistemi.
3. Esiste un confine chiaro: le prove esatte sono attualmente pratiche solo per piccoli modelli lineari, mentre i controesempi esatti si estendono a modelli ReLU moderati. Operatori più grandi richiederanno o codifiche approssimate o l'integrazione con verificatori di reti neurali specializzati e scalabili (ad esempio $\alpha$-$\beta$-CROWN) piuttosto che risolutori SMT generici.

Gli autori concludono che questo lavoro incoraggia la comunità della verifica formale a impegnarsi con i surrogati di PDE neurali e suggerisce che la comunità dell'apprendimento di operatori dovrebbe trattare la verificabilità come un criterio di progettazione.