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

Technischer Überblick: SMT-Kompilierung kleiner Fourier-Neural-Operatoren

Problemstellung
Fourier-Neural-Operatoren (FNOs) bieten eine erhebliche Beschleunigung für Simulationen partieller Differentialgleichungen (PDEs), fehlen jedoch oft formale Garantien bezüglich physikalischer Randbedingungen, wie etwa Massenerhaltung oder Positivität von Konzentrationen. Während die Standardvalidierung auf Monte-Carlo-Tests (MC) oder gradientenbasierter Falsifikation beruht, sampeln diese Methoden nur spezifische Eingaben und können keine exhaustiven Garantien über kontinuierliche Eingabebereiche liefern. Bestehende Werkzeuge zur Verifikation neuronaler Netze sind primär für Klassifikatoren oder Steuerungsrichtlinien konzipiert und behandeln spektrale Faltungen, Eingaben im Funktionenraum oder PDE-spezifische Eigenschaften wie Erhaltungssätze nicht nativ.

Methodik
Die Autoren schlagen vor, trainierte FNOs in Satisfiability Modulo Theories (SMT)-Löser, speziell Z3, zu kompilieren, um eine formale Verifikation zu ermöglichen. Die zentrale Erkenntnis besteht darin, dass die spektrale Faltung in einem FNO auf einem festen Gitter mit festen trainierten Gewichten eine lineare Abbildung darstellt. Folglich ist ein FNO mit ReLU-Nichtlinearitäten eine stückweise lineare Abbildung, die sich exakt in der linearen reellen Arithmetik von Z3 darstellen lässt, ohne den Vorwärtspass zu approximieren.

Die Methodik umfasst zwei primäre Kodierungsstrategien:

1. Exakte Kodierung: Die spektrale Faltung wird durch Anwendung der Operation auf Standardbasisvektoren in eine explizite dichte Matrix ($W^{spec}$) kompiliert. Der vollständige Vorwärtspass wird als Komposition affiner Abbildungen und koordinatenweiser ReLU-Funktionen dargestellt. Diese Kodierung ist sound; ein Ergebnis „UNSAT" beweist, dass die Eigenschaft für alle zulässigen Eingaben gilt, und ein Ergebnis „SAT" liefert ein gültiges Gegenbeispiel. Die Komplexität skaliert jedoch mit $O(N^2H^2L)$, was sie auf kleine Gittergrößen ($N \le 32$) beschränkt.
2. Eingefrorene Kodierung: Um auf größere Gitter ($N \le 64$) zu skalieren, wird der spektrale Pfad durch eine Konstante ersetzt, die von einer Referenzeingabe abgeleitet wird. Dies reduziert die Komplexität auf $O(NH^2L)$ und ermöglicht Prüfungen im Subsekundenbereich. Dies ist jedoch eine Approximation; „UNSAT"-Ergebnisse zertifizieren nur den eingefrorenen Surrogat, nicht den ursprünglichen FNO, und „SAT"-Ergebnisse erfordern eine Validierung am ursprünglichen Modell.

Die Experimente konzentrieren sich auf 1D-Advektions-Diffusions-Reaktions-(ADR)-Gleichungen mit periodischen Randbedingungen. Die Studie verifiziert zwei Eigenschaften:

• Massen-Nicht-Zunahme: Prüfung, ob die diskrete Masse der Ausgabe die Eingabemasse um eine Toleranz $\epsilon = 0.05$ überschreitet.
• Positivität: Prüfung, ob nicht-negative Eingaben an allen Gitterpunkten nicht-negative Ausgaben produzieren.

Hauptbeiträge

• Exakte Kompilierung: Der Artikel präsentiert die erste exakte Kompilierung von FNOs auf festem Gitter in die lineare reelle Arithmetik von Z3 durch Konstruktion expliziter spektraler Matrizen.
• Erste formale Beweise: Er liefert die ersten sounden formalen Beweise für einen neuronalen PDE-Operator, insbesondere die Generierung von Positivitätszertifikaten für lineare (ReLU-freie) FNOs bei Gittergrößen bis zu 16.
• Vergleichende Analyse: Die Arbeit vergleicht Z3 mit gradientenbasierter Falsifikation und Monte-Carlo-Tests über 10 kleine Modelle (85–117 Parameter).
• Grenze zwischen Soundness und Skalierbarkeit: Die Autoren charakterisieren den Kompromiss zwischen exakter Verifikation und Skalierbarkeit und zeigen, dass exakte Kodierungen Beweise für kleine lineare Modelle und Gegenbeispiele für moderate ReLU-Modelle unterstützen, während approximative Kodierungen weiter skalieren, aber die formale Soundness für das ursprüngliche Modell verlieren.

Ergebnisse

• Massen-Nicht-Zunahme: Unter Verwendung der exakten Kodierung fand Z3 sounde Gegenbeispiele für Massenverletzungen für alle 10 Modelle. Bei 7 der 10 Modelle entdeckte Z3 schwerwiegendere Verletzungen als sowohl die gradientenbasierte Falsifikation als auch der MC-Test. Für lineare Modelle optimierte Z3 global, um tiefere Verletzungen zu finden; für ReLU-Modelle blieb die Gradientensuche konkurrenzfähig.
• Positivität:
  • Lineare Modelle (L=1): Z3 lieferte 2 sounde Positivitätsbeweise (für Gittergrößen $N=8$ und $N=16$) und fand 4 sounde Gegenbeispiele an anderen linearen Modellen.
  • ReLU-Modelle (L=2): Z3 fand 1 soundes Gegenbeispiel, lief jedoch bei den verbleibenden 3 Positivitätsabfragen aufgrund der kombinatorischen Explosion von Aktivierungsmustern ($2^{NH}$) aus. Die gradientenbasierte Falsifikation fand erfolgreich Verletzungen bei allen 4 ReLU-Modellen, oft mit größerer Schwere als Z3.
• Eingefrorene Kodierung: Dieser Ansatz verifizierte erfolgreich die Positivität bei 8 größeren Modellen ($N=32$ bis $64$) und fand bei 4 davon Massengegenbeispiele. Diese Ergebnisse sind jedoch approximativ; die Positivitätsbeweise gelten nur für den eingefrorenen Surrogat, und Massengegenbeispiele erforderten eine erneute Validierung am ursprünglichen Modell (3 bestätigt, 1 unbestätigt).

Bedeutung und Behauptungen
Der Artikel positioniert sich als Proof of Concept und nicht als Lösung für die Verifikation im Produktionsmaßstab. Die Autoren stellen explizit fest, dass ihre Ergebnisse die FNO-Verifikation im großen Maßstab nicht lösen; die getesteten Modelle sind „spielzeuggroß" mit eingefrorenen versteckten Schichten und begrenzten Parametern.

Die Bedeutung liegt in der Demonstration, dass:

1. FNOs exakt in stückweise lineare Formen kompiliert werden können, was die Verwendung von SMT-Lösern für physikalisch motivierte Eigenschaften ermöglicht.
2. Formale Verifikation für kleine, lineare neuronale Operatoren machbar ist und die ersten sounden Zertifikate für solche Systeme liefert.
3. Eine klare Grenze besteht: Exakte Beweise sind derzeit nur für kleine lineare Modelle praktikabel, während exakte Gegenbeispiele sich auf moderate ReLU-Modelle erstrecken. Größere Operatoren erfordern entweder approximative Kodierungen oder die Integration mit spezialisierten, skalierbaren neuronalen Verifikatoren (z. B. $\alpha$-$\beta$-CROWN) anstelle von allgemeinen SMT-Lösern.

Die Autoren schließen daraus, dass diese Arbeit die Gemeinschaft der formalen Verifikation ermutigt, sich mit neuronalen PDE-Surrogaten zu befassen, und schlägt vor, dass die Gemeinschaft des Operator-Lernens die Überprüfbarkeit als Designkriterium betrachten sollte.