Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators
For researchers needing formal guarantees on neural PDE surrogates, this work makes the soundness-scalability tradeoff explicit and identifies bottlenecks for verification of production-scale models.
The authors show that Fourier Neural Operators (FNOs) with fixed weights and grid are piecewise-linear and can be exactly encoded in Z3's linear real arithmetic. On 10 small FNO surrogates for 1D advection-diffusion-reaction, the exact encoding yields sound proofs or counterexamples for most queries, while the frozen encoding scales to larger grids but loses soundness.
Fourier Neural Operators (FNOs) can greatly accelerate PDE simulation, but they are often used without formal guarantees that they preserve basic physical structure. We show that, once the trained weights and grid are fixed, the spectral convolution in an FNO is a linear map. As a result, the full forward pass is piecewise-linear and can be represented exactly in Z3's linear real arithmetic. We study two encodings. The exact encoding compiles the spectral convolution into a dense matrix multiplication, which is sound for both proofs and counterexamples. The lighter frozen encoding replaces the spectral path with a constant, making it faster but approximate. On 10 small FNO surrogates for 1D advection-diffusion-reaction (85 to 117 parameters, grids 8 to 32), the exact encoding gives 2 sound positivity proofs on linear (ReLU-free) models, 5 sound positivity counterexamples, and 10 sound mass-violation counterexamples; the remaining 3 positivity queries on ReLU models time out. For mass non-increase, Z3 finds worse counterexamples than both gradient-based falsification and Monte Carlo on 7 of 10 models. The frozen encoding scales to grid size 64 with sub-second positivity checks, but it no longer provides certificates for the original FNO. Overall, the results make the soundness--scalability tradeoff explicit and point to what is needed for formal verification of production-scale neural operators.