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

Technische Samenvatting: SMT-Compilatie van Kleine Fourier Neural Operators

Probleemstelling
Fourier Neural Operators (FNO's) bieden aanzienlijke versnelling voor simulaties van partiële differentiaalvergelijkingen (PDE's), maar missen vaak formele garanties met betrekking tot fysische beperkingen, zoals behoud van massa of positiviteit van concentraties. Waar standaardvalidatie steunt op Monte Carlo (MC)-tests of op gradiënten gebaseerde falsificatie, bemonsteren deze methoden slechts specifieke invoeren en kunnen ze geen exhaustieve garanties bieden over continue invoergebieden. Bestaande verificatietools voor neurale netwerken zijn voornamelijk ontworpen voor classifiers of besturingsbeleid en handelen geen spectrale convoluties, invoer in functieruimten of PDE-specifieke eigenschappen zoals behoudswetten op een native manier.

Methodologie
De auteurs stellen voor om getrainde FNO's te compileren naar Satisfiability Modulo Theories (SMT)-oplossers, specifiek Z3, om formele verificatie mogelijk te maken. Het kerninzicht is dat op een vast rooster met vaste getrainde gewichten de spectrale convolutie in een FNO een lineaire afbeelding is. Bijgevolg is een FNO met ReLU-niet-lineariteiten een stuksgewijs lineaire afbeelding die exact kan worden weergegeven in de lineaire reële rekenkunde van Z3 zonder de voorwaartse doorgang te benaderen.

De methodologie omvat twee primaire coderingsstrategieën:

1. Exacte Codering: De spectrale convolutie wordt gecompileerd tot een expliciete dichte matrix ($W^{spec}$) door de operatie toe te passen op standaardbasisvectoren. De volledige voorwaartse doorgang wordt weergegeven als een samenstelling van affiene afbeeldingen en coördinaatgewijze ReLU-functies. Deze codering is sound; een "UNSAT"-resultaat bewijst dat de eigenschap geldt voor alle toelaatbare invoeren, en een "SAT"-resultaat levert een geldig contra-exemplaar. De complexiteit schaalt echter als $O(N^2H^2L)$, wat dit beperkt tot kleine roostergroottes ($N \le 32$).
2. Bevroren Codering: Om te schalen naar grotere roosters ($N \le 64$) wordt het spectrale pad vervangen door een constante afgeleid van een referentie-invoer. Dit reduceert de complexiteit tot $O(NH^2L)$ en maakt checks in minder dan een seconde mogelijk. Dit is echter een benadering; "UNSAT"-resultaten certificeren slechts de bevroren surrogaat, niet de originele FNO, en "SAT"-resultaten vereisen validatie op het originele model.

De experimenten richten zich op 1D-advectie-diffusie-reactie (ADR)-vergelijkingen met periodieke randvoorwaarden. De studie verifieert twee eigenschappen:

• Massa-niet-toename: Controleren of de discrete massa van de uitvoer de invoermassa overschrijdt met een tolerantie $\epsilon = 0,05$.
• Positiviteit: Controleren of niet-negatieve invoeren niet-negatieve uitvoeren produceren op alle roosterpunten.

Belangrijkste Bijdragen

• Exacte Compilatie: Het artikel presenteert de eerste exacte compilatie van vaste-rooster FNO's naar de lineaire reële rekenkunde van Z3 door expliciete spectrale matrices te construeren.
• Eerste Formele Bewijzen: Het biedt de eerste sound formele bewijzen voor een neurale PDE-operator, specifiek het genereren van positiviteitscertificaten voor lineaire (ReLU-vrije) FNO's bij roostergroottes tot 16.
• Vergelijkende Analyse: Het werk vergelijkt Z3 met op gradiënten gebaseerde falsificatie en Monte Carlo-tests over 10 kleine modellen (85–117 parameters).
• Grens tussen Soundheid en Schaalbaarheid: De auteurs karakteriseren de afweging tussen exacte verificatie en schaalbaarheid, en tonen aan dat exacte coderingen bewijzen ondersteunen voor kleine lineaire modellen en contra-exemplaren voor matige ReLU-modellen, terwijl benaderende coderingen verder schalen maar formele soundheid voor het originele model verliezen.

Resultaten

• Massa-niet-toename: Met behulp van de exacte codering vond Z3 sound massa-schendende contra-exemplaren voor alle 10 modellen. Op 7 van de 10 modellen ontdekte Z3 ernstiger schendingen dan zowel op gradiënten gebaseerde falsificatie als MC-tests. Voor lineaire modellen optimaliseerde Z3 globaal om diepere schendingen te vinden; voor ReLU-modellen bleef gradiëntzoekcompetitief.
• Positiviteit:
  • Lineaire Modellen (L=1): Z3 produceerde 2 sound positiviteitsbewijzen (voor roostergroottes $N=8$ en $N=16$) en vond 4 sound contra-exemplaren op andere lineaire modellen.
  • ReLU-modellen (L=2): Z3 vond 1 sound contra-exemplaar, maar liep vast op de overige 3 positiviteitsvragen door de combinatorische explosie van activatiepatronen ($2^{NH}$). Gradiëntfalsificatie vond succesvol schendingen op alle 4 ReLU-modellen, vaak met grotere ernst dan Z3.
• Bevroren Codering: Deze benadering verifieerde succesvol positiviteit op 8 grotere modellen ($N=32$ tot $64$) en vond massa-contra-exemplaren op 4 daarvan. Deze resultaten zijn echter benaderend; de positiviteitsbewijzen gelden alleen voor de bevroren surrogaat, en massa-contra-exemplaren vereisten hervalidatie op het originele model (3 bevestigd, 1 onbevestigd).

Betekenis en Claims
Het artikel positioneert zichzelf als een bewijs van concept in plaats van een oplossing voor verificatie op productieschaal. De auteurs stellen expliciet dat hun resultaten de verificatie van FNO's op schaal niet oplossen; de geteste modellen zijn "speelgoed-grootte" met bevroren verborgen lagen en beperkte parameters.

De betekenis ligt in het aantonen dat:

1. FNO's exact kunnen worden gecompileerd tot stuksgewijs lineaire vormen, wat het gebruik van SMT-oplossers voor door de fysica gemotiveerde eigenschappen mogelijk maakt.
2. Formele verificatie haalbaar is voor kleine, lineaire neurale operatoren, wat leidt tot de eerste sound certificaten voor dergelijke systemen.
3. Er een duidelijke grens bestaat: exacte bewijzen zijn momenteel alleen praktisch voor kleine lineaire modellen, terwijl exacte contra-exemplaren zich uitstrekken tot matige ReLU-modellen. Grotere operatoren vereisen ofwel benaderende coderingen of integratie met gespecialiseerde, schaalbare verificatoren voor neurale netwerken (bijv. $\alpha$-$\beta$-CROWN) in plaats van algemene SMT-oplossers.

De auteurs concluderen dat dit werk de gemeenschap voor formele verificatie aanmoedigt om zich te bezighouden met neurale PDE-surrogaten en suggereert dat de gemeenschap voor operator-learning verifieerbaarheid moet behandelen als een ontwerpcriterium.