BEACONS: Bounded-Error, Algebraically-Composable Neural Solvers for Partial Differential Equations

TL;DR

BEACONS addresses the extrapolation failure of neural PDE solvers by embedding formal guarantees into neural architectures solving hyperbolic PDEs. It combines method-of-characteristics-based smoothness with bounded $L^{\infty}$ error bounds for shallow networks and introduces algebraic composability to build deep solvers whose overall error remains controlled. The framework includes a domain-specific language, an automated theorem-prover for machine-checkable certificates, and a code-generator that enables end-to-end formally-verified training and inference. Empirical results on 1D/2D linear advection, Burgers', and Euler equations demonstrate substantial improvements in accuracy and conservation over standard neural nets, with error bounds aligning with formal proofs. The work proposes a neurosymbolic path to reliable, extrapolatable PDE solvers and outlines future extensions to broader equation classes and multi-physics systems.

Abstract

The traditional limitations of neural networks in reliably generalizing beyond the convex hulls of their training data present a significant problem for computational physics, in which one often wishes to solve PDEs in regimes far beyond anything which can be experimentally or analytically validated. In this paper, we show how it is possible to circumvent these limitations by constructing formally-verified neural network solvers for PDEs, with rigorous convergence, stability, and conservation properties, whose correctness can therefore be guaranteed even in extrapolatory regimes. By using the method of characteristics to predict the analytical properties of PDE solutions a priori (even in regions arbitrarily far from the training domain), we show how it is possible to construct rigorous extrapolatory bounds on the worst-case L^inf errors of shallow neural network approximations. Then, by decomposing PDE solutions into compositions of simpler functions, we show how it is possible to compose these shallow neural networks together to form deep architectures, based on ideas from compositional deep learning, in which the large L^inf errors in the approximations have been suppressed. The resulting framework, called BEACONS (Bounded-Error, Algebraically-COmposable Neural Solvers), comprises both an automatic code-generator for the neural solvers themselves, as well as a bespoke automated theorem-proving system for producing machine-checkable certificates of correctness. We apply the framework to a variety of linear and non-linear PDEs, including the linear advection and inviscid Burgers' equations, as well as the full compressible Euler equations, in both 1D and 2D, and illustrate how BEACONS architectures are able to extrapolate solutions far beyond the training data in a reliable and bounded way. Various advantages of the approach over the classical PINN approach are discussed.

Figures (8)

• Figure 1: On the left, an example of the extended Racket data structure for representing a system of hyperbolic PDEs (in this case, the 1D compressible Euler equations), a collection of simulation parameters (in this case, representing a 1D Sod-type shock tube problem), and a collection of hyperparameters for a shallow BEACONS architecture (6 layers, 64 neurons per layer, 10,000 maximum training steps). On the right, the resulting optimized C code output by the automatic code-generator for running the specified simulation (using a Lax-Friedrichs solver with second-order flux extrapolation), generating the necessary training data, and training the BEACONS architecture accordingly.
• Figure 2: On the left, the final few steps of an executable Racket proof of flux continuity for a Roe solver for the 1D inviscid Burgers' equation. On the right, the final few steps of an executable Racket proof of a bound on the worst-case ${L^{\infty}}$ error (for the non-smooth parts of the solution) for a shallow BEACONS architecture for solving the 1D inviscid Burgers' equation.
• Figure 3: Results for the 1D linear advection Riemann problem at times ${t = 0.5}$ (left) and ${t = 0.8}$ (right), obtained using a formally-verified numerical solver (blue), a 6-layer neural network (red), an 8-layer neural network (yellow), a 6-layer BEACONS architecture (purple), and an 8-layer BEACONS architecture (green). The 6-layer neural network slightly overestimates the advection speed, and the 8-layer neural network significantly underestimates it; both neural network solutions exhibit substantial conservation errors. Both BEACONS solutions track the numerical solution more-or-less perfectly.
• Figure 4: Results for the 2D linear advection disk problem at times ${t = 0.33}$ (left), ${t = 0.66}$ (middle), and ${t = 0.99}$ (right), obtained using a formally-verified numerical solver (top), an 8-layer neural network (middle), and an 8-layer BEACONS architecture (bottom). The 8-layer neural network progressively distorts the shape of the disk as it approaches the top right of the domain, causing it to become increasingly "egg-shaped", while also underestimating the advection speed overall. The BEACONS architecture successfully preserves the shape of the disk, and shows near-perfect agreement with the numerical solution.
• Figure 5: Results for the 1D inviscid Burgers' "top-hat" initial value problem at times ${t = 0.5}$ (left) and ${t = 0.8}$ (right), obtained using a formally-verified numerical solver (blue), a 6-layer neural network (red), an 8-layer neural network (yellow), a 6-layer BEACONS architecture (purple), and an 8-layer BEACONS architecture (green). Both the 6-layer and 8-layer neural networks significantly overestimate the speed of the right-moving shock and underestimate the speed of the left-moving rarefaction; both neural network solutions fail to conserve the advected quantity, and exhibit significant diffusion of the overall qualitative structure of the solution. Both BEACONS solutions track the numerical solution more-or-less perfectly, without significant instability, wave-speed mis-prediction, or conservation errors.

Theorems & Definitions (4)

• Theorem 1
• Lemma 1
• Theorem 2
• Proposition 1