Search papers, labs, and topics across Lattice.
The paper introduces BEACONS, a framework for constructing formally-verified neural network solvers for PDEs with guaranteed convergence, stability, and conservation properties, enabling reliable extrapolation beyond training data. BEACONS leverages the method of characteristics to predict analytical properties of PDE solutions a priori, allowing for rigorous bounds on L^inf errors of shallow neural network approximations. By composing these shallow networks into deep architectures, BEACONS suppresses large approximation errors and provides machine-checkable certificates of correctness, demonstrating improved extrapolation compared to PINNs on linear and non-linear PDEs.
Neural networks can now reliably solve PDEs outside their training data's convex hull, thanks to a formally-verified framework that guarantees convergence and stability.
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.
