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

Ali Baheri; David Millard; Ignacio Laguna Peralta

arxiv: 2605.08938 · v1 · submitted 2026-05-09 · 💻 cs.AI · cs.LG

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

Ali Baheri , David Millard , Ignacio Laguna Peralta This is my paper

Pith reviewed 2026-05-12 01:46 UTC · model grok-4.3

classification 💻 cs.AI cs.LG

keywords Fourier Neural Operatorsformal verificationSMT solversZ3PDE surrogatespositivitymass conservationpiecewise-linear models

0 comments

The pith

Once trained with fixed weights and grid, small Fourier Neural Operators become piecewise-linear functions that SMT solvers can verify exactly for physical properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the spectral convolution inside an FNO reduces to a linear map when weights and discretization are held fixed. This turns the entire forward pass into a piecewise-linear computation that can be encoded directly into Z3's linear real arithmetic. Two concrete encodings are presented: an exact version that compiles the convolution into matrix multiplication and preserves soundness for both proofs and counterexamples, and a lighter frozen version that substitutes constants for faster but approximate checks. Experiments on ten tiny FNO surrogates for 1D advection-diffusion-reaction produce sound positivity proofs on linear models, multiple counterexamples to positivity and mass non-increase, and reveal timeouts on some ReLU queries. A reader cares because the work supplies the first explicit soundness-scalability tradeoff for formally checking whether neural PDE surrogates obey basic invariants instead of relying only on empirical testing.

Core claim

With trained weights and grid 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. The exact encoding compiles the spectral path into dense matrix multiplication, which is sound for both proving and disproving queries such as positivity and mass non-increase.

What carries the argument

The exact SMT encoding that converts the FNO spectral convolution into a dense matrix multiplication inside linear real arithmetic, enabling sound verification of the full piecewise-linear forward pass.

If this is right

Sound positivity proofs are obtained for all ReLU-free models.
Sound counterexamples to positivity are produced on five of the ten models.
Sound counterexamples to mass non-increase are produced on all ten models.
The frozen encoding scales to grid size 64 with sub-second checks but loses soundness for the original network.
ReLU activations cause three positivity queries to time out under the exact encoding.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Restricting neural operators to piecewise-linear activations from the design stage could make larger instances directly amenable to the same SMT compilation.
A hybrid workflow that first uses SMT on the linear core and then gradient or Monte Carlo search on the remaining nonlinear pieces could cover models that currently time out.
The same linear-map reduction might apply to other spectral neural operators beyond FNOs if their Fourier layers are likewise frozen after training.

Load-bearing premise

The studied FNO models stay very small, with 85-117 parameters and grids of size 8-32, so that the SMT solver finishes the queries without timing out.

What would settle it

An FNO instance on which the exact encoding returns unsat for a mass-violation query, yet direct evaluation of the original network on the same input point shows mass increase.

Figures

Figures reproduced from arXiv: 2605.08938 by Ali Baheri, David Millard, Ignacio Laguna Peralta.

**Figure 1.** Figure 1: The FNO-to-SMT bridge. We compile the spectral convolution into an explicit dense matrix and then query physics-motivated properties with an SMT solver. The exact encoding is sound but dense; the frozen encoding is faster but approximate. 3.3. Properties Our experiments use the one-dimensional advectiondiffusion-reaction equation with periodic boundary conditions, ∂tu + v∂xu = D∂xxu − λu. (5) Each traini… view at source ↗

**Figure 2.** Figure 2: Model quality. Left: Test MSE. Right: Severity of Z3’s sound counterexample for mass non-increase, with every counterexample re-evaluated on the original model. the 1-layer models, Z3 has a clearer advantage because the linear structure lets the solver optimize globally. Z3 solve times for mass range from <0.1 s at N=8 to 1.8 s for the N=16, L=2 case. Gradient falsification takes 1 to 4 s. 4.3. Positivity:… view at source ↗

**Figure 4.** Figure 4: Positivity. Left: Z3 exact results: green = sound proof, red = sound CE, gray = timeout. Right: Minimum output found by Z3, gradient falsification, and MC. Z3 proofs certify positivity for all constrained inputs. 10 2 10 1 10 0 Time (s) L1-N8-s42 L1-N8-s123 L1-N16-s42 L1-N16-s123 L1-N32-s42 L1-N32-s123 L2-N8-s42 L2-N8-s123 L2-N16-s42 L2-N16-s123 Mass (Exact Enc.) 10 2 10 1 10 0 10 1 Time (s) timeout Positi… view at source ↗

**Figure 5.** Figure 5: Z3 solve time with the exact encoding. Left: Mass. Right: Positivity. Linear models solve faster, while ReLU models time out for positivity proofs. 5. Discussion What this demonstrates. The main technical point is that FNOs can be compiled exactly into piecewise-linear form through spectral matrix construction. On small models, this lets Z3 produce both sound proofs and sound counterexamples. In particula… view at source ↗

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper shows how to compile the spectral layers of tiny fixed FNOs into exact Z3 queries for sound checks on positivity and mass, but the models stay very small and some ReLU cases time out.

read the letter

The core contribution is turning the spectral convolution into a dense matrix multiply once weights and grid are frozen, so the whole forward pass becomes piecewise linear and fits directly into linear real arithmetic. That part is clean and follows from the FFT structure without any extra assumptions. They then build an exact encoding that Z3 can use for both proofs and counterexamples, plus a faster frozen version that drops the spectral path to a constant. On the 10 small 1D models they tested, the exact version delivers sound positivity proofs on the two linear cases, sound counterexamples on five others, and sound mass-violation counterexamples on all ten, while also beating gradient and Monte Carlo falsification on seven models for mass non-increase. That is concrete and useful to see laid out side by side with the timeouts and the approximation cost of the frozen encoding. The paper is honest about the scalability limits and does not overclaim what the results mean for larger networks. The main limitations are the model sizes (85-117 parameters, grids 8-32) and the three positivity queries that time out on ReLU models. The frozen encoding is explicitly approximate and does not certify the original FNO, and there is no statistical summary or error analysis across the ten runs. Everything stays in 1D advection-diffusion-reaction, so generalization to higher dimensions or bigger grids is left open. This work is for people already thinking about SMT or formal methods for neural operators who want a working example of the exact-versus-approximate tradeoff. A reader focused on production-scale PDE surrogates will find the scale too small to apply directly. It deserves a serious referee because the encoding is new, the soundness claims are backed by explicit Z3 runs, and the limitations are stated plainly rather than hidden.

Referee Report

2 major / 2 minor

Summary. The manuscript claims that Fourier Neural Operators (FNOs), once trained weights and discretization grid are fixed, have a linear spectral convolution step, making the full model piecewise linear and exactly encodable in Z3's linear real arithmetic for SMT-based formal verification. Two encodings are studied: an exact one compiling to matrix multiplications (sound for proofs and counterexamples) and a frozen approximate one for speed. Experiments on 10 small 1D FNO surrogates (85-117 params, grids 8-32) for advection-diffusion-reaction PDEs show sound positivity proofs for 2 linear models, counterexamples for 5, timeouts for 3 ReLU models, and mass-violation counterexamples for all 10; the frozen version scales to larger grids but is approximate.

Significance. If the central encoding holds, this provides a novel approach to formally verifying properties like positivity and conservation in neural PDE surrogates using off-the-shelf SMT solvers. The work is significant for its explicit demonstration of soundness on the exact encoding and for highlighting practical limitations such as timeouts. It credits the use of standard linear real arithmetic without additional assumptions or fitted parameters, and the production of machine-checked proofs and counterexamples.

major comments (2)

[Experimental results] Experimental results section: the 3 timeouts on positivity queries for ReLU models (out of 10 total) limit the exact encoding's coverage to linear cases only, which is load-bearing for the claim that FNOs can be formally verified in general.
[Frozen encoding description] Frozen encoding description: replacing the spectral path with a constant makes the encoding approximate and unable to certify the original FNO; without quantified error bounds on this approximation, the scalability results to grid size 64 cannot be directly compared to the exact method.

minor comments (2)

The results across the 10 models are reported only as aggregate counts without statistical analysis, variance, or per-model breakdowns, which would strengthen the reproducibility of the findings.
Notation for the compilation of spectral convolution to dense matrix multiplication could be clarified with an explicit equation or pseudocode in the methods section.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. We address the two major comments below, agreeing with the identified limitations while clarifying the manuscript's scope and proposing targeted revisions for improved precision.

read point-by-point responses

Referee: [Experimental results] Experimental results section: the 3 timeouts on positivity queries for ReLU models (out of 10 total) limit the exact encoding's coverage to linear cases only, which is load-bearing for the claim that FNOs can be formally verified in general.

Authors: We agree that the three timeouts for ReLU models demonstrate that the exact encoding, as implemented, is currently practical only for linear FNOs. However, the manuscript does not advance a claim that FNOs can be formally verified in general. The title poses an open question, the abstract and conclusion explicitly report the timeouts, and the final paragraph frames the contribution around the observed soundness-scalability tradeoff. The sound proofs and counterexamples obtained for the linear models, together with the mass-violation results for all ten models, still establish feasibility for small fixed instances. We will revise the experimental results section to state more explicitly that the exact encoding is presently limited to linear activations and to flag efficient handling of ReLU (or other nonlinearities) as future work. revision: partial
Referee: [Frozen encoding description] Frozen encoding description: replacing the spectral path with a constant makes the encoding approximate and unable to certify the original FNO; without quantified error bounds on this approximation, the scalability results to grid size 64 cannot be directly compared to the exact method.

Authors: We agree that the frozen encoding is approximate and does not certify the original FNO, a point already noted in the manuscript. The grid-size-64 results are presented to illustrate the computational benefit of the lighter encoding rather than to claim equivalence with the exact method. We acknowledge that the absence of quantified error bounds prevents a rigorous comparison. Deriving such bounds is non-trivial and outside the current scope; we will therefore add a clarifying sentence in the frozen-encoding subsection stating that the reported timings are for an approximation and that error analysis remains future work. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's derivation rests on the direct mathematical observation that fixing the trained weights and discretization grid turns each FNO spectral convolution into an ordinary matrix multiplication (FFT → mode-wise multiply → IFFT), rendering the full forward pass piecewise-linear and therefore exactly representable in Z3's linear real arithmetic. This reduction follows from the standard definition of the FNO architecture and linear algebra; it is not obtained by fitting parameters to data, by renaming an empirical pattern, or by any self-citation chain. The authors explicitly document the encoding's limitations (timeouts on ReLU models, approximation in the frozen variant) and evaluate soundness only on the small instances they can solve, leaving the central claim self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The verification rests on the domain assumption that fixed-weight spectral convolution is exactly linear and that Z3's linear real arithmetic can represent the piecewise-linear forward pass without floating-point issues.

axioms (1)

domain assumption Spectral convolution with fixed trained weights and grid is a linear map
Stated directly in the abstract as the basis for exact encoding into Z3.

pith-pipeline@v0.9.0 · 5565 in / 1220 out tokens · 30420 ms · 2026-05-12T01:46:14.822627+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

once the trained weights and grid are fixed, the spectral convolution in an FNO is a linear map... the full forward pass is piecewise-linear and can be represented exactly in Z3's linear real arithmetic
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We build W_spec_ℓ by applying the spectral convolution to each standard basis vector

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

[1]

International Conference on Learning Representations , year=

Fourier Neural Operator for Parametric Partial Differential Equations , author=. International Conference on Learning Representations , year=

work page
[2]

Learning nonlinear operators via

Lu, Lu and Jin, Pengzhan and Pang, Guofei and Zhang, Zhongqiang and Karniadakis, George Em , journal=. Learning nonlinear operators via

work page
[3]

Kochenderfer and Ali Baheri , title =

Zahra Shahrooei and Mykel J. Kochenderfer and Ali Baheri , title =. European Control Conference (. 2023 , doi =

work page 2023
[4]

2024 , doi =

Joshua Yancosek and Ali Baheri , title =. 2024 , doi =

work page 2024
[5]

2022 , eprint =

Ali Baheri and Hao Ren and Benjamin Johnson and Pouria Razzaghi and Peng Wei , title =. 2022 , eprint =. doi:10.48550/arXiv.2205.04590 , url =

work page doi:10.48550/arxiv.2205.04590 2022
[6]

Journal of Computational Physics , volume=

Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations , author=. Journal of Computational Physics , volume=

work page
[7]

Reluplex: An efficient

Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J , booktitle=. Reluplex: An efficient

work page
[8]

Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico , booktitle=. Beta-

work page
[9]

International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

de Moura, Leonardo and Bj. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

work page
[10]

Liu, Jun and Meng, Yiming and Fitzsimmons, Maxwell and Zhou, Ruikun , booktitle=

work page
[11]

Gorard, Jonathan and Hakim, Ammar and Juno, James , journal=

work page
[12]

Journal of Computational Physics , pages=

Enforcing exact physics in scientific machine learning: a data-driven exterior calculus on graphs , author=. Journal of Computational Physics , pages=

work page
[13]

On the effectiveness of interval bound propagation for training verifiably robust models

On the effectiveness of interval bound propagation for training verifiably robust models , author=. arXiv preprint arXiv:1810.12715 , year=

work page arXiv
[14]

Neural operator: Learning maps between function spaces with applications to

Kovachki, Nikola and Li, Zongyi and Liu, Burigede and Azizzadenesheli, Kamyar and Bhattacharya, Kaushik and Stuart, Andrew and Anandkumar, Anima , journal=. Neural operator: Learning maps between function spaces with applications to

work page

[1] [1]

International Conference on Learning Representations , year=

Fourier Neural Operator for Parametric Partial Differential Equations , author=. International Conference on Learning Representations , year=

work page

[2] [2]

Learning nonlinear operators via

Lu, Lu and Jin, Pengzhan and Pang, Guofei and Zhang, Zhongqiang and Karniadakis, George Em , journal=. Learning nonlinear operators via

work page

[3] [3]

Kochenderfer and Ali Baheri , title =

Zahra Shahrooei and Mykel J. Kochenderfer and Ali Baheri , title =. European Control Conference (. 2023 , doi =

work page 2023

[4] [4]

2024 , doi =

Joshua Yancosek and Ali Baheri , title =. 2024 , doi =

work page 2024

[5] [5]

2022 , eprint =

Ali Baheri and Hao Ren and Benjamin Johnson and Pouria Razzaghi and Peng Wei , title =. 2022 , eprint =. doi:10.48550/arXiv.2205.04590 , url =

work page doi:10.48550/arxiv.2205.04590 2022

[6] [6]

Journal of Computational Physics , volume=

Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations , author=. Journal of Computational Physics , volume=

work page

[7] [7]

Reluplex: An efficient

Katz, Guy and Barrett, Clark and Dill, David L and Julian, Kyle and Kochenderfer, Mykel J , booktitle=. Reluplex: An efficient

work page

[8] [8]

Wang, Shiqi and Zhang, Huan and Xu, Kaidi and Lin, Xue and Jana, Suman and Hsieh, Cho-Jui and Kolter, J Zico , booktitle=. Beta-

work page

[9] [9]

International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

de Moura, Leonardo and Bj. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

work page

[10] [10]

Liu, Jun and Meng, Yiming and Fitzsimmons, Maxwell and Zhou, Ruikun , booktitle=

work page

[11] [11]

Gorard, Jonathan and Hakim, Ammar and Juno, James , journal=

work page

[12] [12]

Journal of Computational Physics , pages=

Enforcing exact physics in scientific machine learning: a data-driven exterior calculus on graphs , author=. Journal of Computational Physics , pages=

work page

[13] [13]

On the effectiveness of interval bound propagation for training verifiably robust models

On the effectiveness of interval bound propagation for training verifiably robust models , author=. arXiv preprint arXiv:1810.12715 , year=

work page arXiv

[14] [14]

Neural operator: Learning maps between function spaces with applications to

Kovachki, Nikola and Li, Zongyi and Liu, Burigede and Azizzadenesheli, Kamyar and Bhattacharya, Kaushik and Stuart, Andrew and Anandkumar, Anima , journal=. Neural operator: Learning maps between function spaces with applications to

work page