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

Technical Summary: SMT Compilation of Small Fourier Neural Operators

Problem Statement
Fourier Neural Operators (FNOs) offer significant acceleration for Partial Differential Equation (PDE) simulations but often lack formal guarantees regarding physical constraints, such as mass conservation or positivity of concentrations. While standard validation relies on Monte Carlo (MC) testing or gradient-based falsification, these methods only sample specific inputs and cannot provide exhaustive guarantees over continuous input regions. Existing neural network verification tools are primarily designed for classifiers or control policies and do not natively handle spectral convolutions, function-space inputs, or PDE-specific properties like conservation laws.

Methodology
The authors propose compiling trained FNOs into Satisfiability Modulo Theories (SMT) solvers, specifically Z3, to enable formal verification. The core insight is that on a fixed grid with fixed trained weights, the spectral convolution in an FNO is a linear map. Consequently, an FNO with ReLU nonlinearities is a piecewise-linear map that can be represented exactly in Z3's linear real arithmetic without approximating the forward pass.

The methodology involves two primary encoding strategies:

1. Exact Encoding: The spectral convolution is compiled into an explicit dense matrix ($W^{spec}$) by applying the operation to standard basis vectors. The full forward pass is represented as a composition of affine maps and coordinate-wise ReLU functions. This encoding is sound, meaning a "UNSAT" result proves the property holds for all admissible inputs, and a "SAT" result provides a valid counterexample. However, the complexity scales as $O(N^2H^2L)$, limiting it to small grid sizes ($N \le 32$).
2. Frozen Encoding: To scale to larger grids ($N \le 64$), the spectral path is replaced with a constant derived from a reference input. This reduces complexity to $O(NH^2L)$ and enables sub-second checks. However, this is an approximation; "UNSAT" results certify only the frozen surrogate, not the original FNO, and "SAT" results require validation on the original model.

The experiments focus on 1D advection-diffusion-reaction (ADR) equations with periodic boundary conditions. The study verifies two properties:

• Mass Non-Increase: Checking if the discrete mass of the output exceeds the input mass by a tolerance $\epsilon = 0.05$.
• Positivity: Checking if non-negative inputs produce non-negative outputs at all grid points.

Key Contributions

• Exact Compilation: The paper presents the first exact compilation of fixed-grid FNOs into Z3's linear real arithmetic by constructing explicit spectral matrices.
• First Formal Proofs: It provides the first sound formal proofs for a neural PDE operator, specifically generating positivity certificates for linear (ReLU-free) FNOs at grid sizes up to 16.
• Comparative Analysis: The work compares Z3 against gradient-based falsification and Monte Carlo testing across 10 small models (85–117 parameters).
• Soundness–Scalability Boundary: The authors characterize the trade-off between exact verification and scalability, demonstrating that exact encodings support proofs for small linear models and counterexamples for moderate ReLU models, while approximate encodings scale further but lose formal soundness for the original model.

Results

• Mass Non-Increase: Using the exact encoding, Z3 found sound mass-violation counterexamples for all 10 models. On 7 of the 10 models, Z3 discovered more severe violations than both gradient-based falsification and MC testing. For linear models, Z3 optimized globally to find deeper violations; for ReLU models, gradient search remained competitive.
• Positivity:
  • Linear Models (L=1): Z3 produced 2 sound positivity proofs (for grid sizes $N=8$ and $N=16$) and found 4 sound counterexamples on other linear models.
  • ReLU Models (L=2): Z3 found 1 sound counterexample but timed out on the remaining 3 positivity queries due to the combinatorial explosion of activation patterns ($2^{NH}$). Gradient falsification successfully found violations on all 4 ReLU models, often with greater severity than Z3.
• Frozen Encoding: This approach successfully verified positivity on 8 larger models ($N=32$ to $64$) and found mass counterexamples on 4 of them. However, these results are approximate; the positivity proofs apply only to the frozen surrogate, and mass counterexamples required re-validation on the original model (3 confirmed, 1 unconfirmed).

Significance and Claims
The paper positions itself as a proof of concept rather than a solution for production-scale verification. The authors explicitly state that their results do not solve FNO verification at scale; the models tested are "toy-sized" with frozen hidden layers and limited parameters.

The significance lies in demonstrating that:

1. FNOs can be compiled exactly into piecewise-linear forms, enabling the use of SMT solvers for physics-motivated properties.
2. Formal verification is feasible for small, linear neural operators, yielding the first sound certificates for such systems.
3. There is a clear boundary: exact proofs are currently practical only for small linear models, while exact counterexamples extend to moderate ReLU models. Larger operators will require either approximate encodings or integration with specialized, scalable neural-network verifiers (e.g., $\alpha$-$\beta$-CROWN) rather than general-purpose SMT solvers.

The authors conclude that this work encourages the formal verification community to engage with neural PDE surrogates and suggests that the operator-learning community should treat verifiability as a design criterion.