Verified AI Solvers Extend Physics Beyond Experiments

Scientists are addressing a fundamental challenge in computational physics: the limited ability of neural networks to reliably generalise beyond their training data when solving partial differential equations. Jonathan Gorard from Princeton University, Ammar Hakim and James Juno from Princeton Plasma Physics Laboratory, working in collaboration, present a novel framework, BEACONS (Bounded-Error, Algebraically-Composable Neural Solvers), which constructs formally-verified neural network solvers with guaranteed convergence, stability, and conservation properties. This research is significant because it circumvents the typical limitations of neural networks by predicting analytical properties of PDE solutions and composing shallow networks, enabling reliable and bounded extrapolations even in regimes inaccessible to experimental or analytical validation. The team demonstrate BEACONS’ capabilities across linear and non-linear PDEs, including the linear advection, inviscid Burgers’ and compressible Euler equations in both one and two dimensions, alongside an automatic code-generator and theorem-proving system to verify correctness.

Unlike current methods, this approach guarantees accurate results even when predicting behaviour outside of known data, a crucial step for modelling everything from weather patterns to aerospace engineering. This breakthrough addresses a critical challenge in computational physics, where solving partial differential equations (PDEs) often requires predictions in regimes that cannot be experimentally or analytically verified.

The research demonstrates the construction of formally-verified neural network architectures capable of rigorously guaranteeing convergence, stability, and conservation properties, even when extrapolating beyond known data. BEACONS achieves this by predicting analytical properties of PDE solutions a priori, using the method of characteristics to establish reliable bounds on approximation errors.

By decomposing complex PDE solutions into simpler, composable functions, the framework builds deep neural networks that suppress errors typically associated with discontinuous functions, mirroring techniques used in traditional numerical solvers like flux limiters. The resulting system includes an automatic code-generator for creating these neural solvers, alongside a bespoke automated theorem-proving system that generates machine-checkable certificates of correctness.

This work successfully applies BEACONS to a range of linear and non-linear PDEs, including the linear advection and inviscid Burgers’ equations, and the full compressible Euler equations in both one and two dimensions. The innovation lies in treating neural networks not merely as interpolators, but as a generalisation of classical numerical methods, allowing for rigorous mathematical analysis and verification.

By leveraging algebraic composition and automated theorem proving, the researchers have created a system capable of producing machine-checkable guarantees of solution accuracy, even in previously inaccessible extrapolatory regimes. This development promises to enhance the reliability and trustworthiness of simulations across a broad spectrum of scientific and engineering applications.

Predicting solution behaviour and quantifying error bounds using method of characteristics

The method of characteristics underpinned the development of rigorously-validated neural network solvers, enabling prediction of analytical properties of partial differential equation (PDE) solutions even outside the training domain. This technique, traditionally used to solve PDEs, was adapted to forecast solution behaviour and establish bounds on potential errors when approximated by neural networks.

By anticipating how solutions evolve, we constructed extrapolatory error bounds for shallow network approximations, quantifying the worst-case L^inf error, a measure of the maximum deviation between the true solution and the neural network’s prediction. To further enhance accuracy and reliability, complex PDE solutions were decomposed into compositions of simpler functions.

This modular approach allowed us to build deeper neural network architectures, inspired by compositional deep learning, where approximating discontinuous functions is improved by combining them with smoother ones. A bespoke automated theorem-proving system was also created as an integral part of BEACONS, generating machine-checkable certificates of correctness, providing formal verification of the solver’s behaviour and guaranteeing its accuracy even when extrapolating beyond the training data.

The framework was applied to linear and non-linear PDEs, including the linear advection, inviscid Burgers’ equations, and the compressible Euler equations in both one and two dimensions. By leveraging the method of characteristics, the study predicted analytical properties of PDE solutions a priori, enabling rigorous extrapolatory bounds on the worst-case L^inf errors of shallow neural network approximations.

Shallow neural networks were decomposed into compositions of simpler functions, forming architectures, based on ideas from compositional learning, that suppressed large L^inf errors in approximations. The study highlights a crucial distinction from PINNs, where latent space constraints can become problematic for complex, non-linear systems. BEACONS avoids these issues by focusing on algebraic composability, allowing for the construction of deeper, more expressive architectures while maintaining tightly controlled error bounds. This approach circumvents the limitations of traditional PINNs, which can struggle with non-convex latent space structures and convergence issues in complex scenarios.

Analytical safeguards enhance neural network reliability for physics extrapolations

The persistent challenge of reliably extrapolating beyond known data has long plagued computational physics. For decades, simulations have been constrained by the boundaries of training data, limiting our ability to model truly novel scenarios or extreme conditions. This work represents a significant step towards overcoming that limitation by achieving greater accuracy within established parameters, but by offering a framework for guaranteed reliability even when venturing into the unknown.

The development of BEACONS, Bounded-Error, Algebraically-COmposable Neural Solvers, signals a shift from simply approximating solutions to formally verifying them. What distinguishes this approach is the integration of analytical prediction, via the method of characteristics, with neural network architecture. By pre-determining the expected behaviour of solutions, researchers can construct networks with built-in safeguards against unphysical extrapolations.

This isn’t merely about improving performance metrics; it’s about establishing a level of trust in simulations that has been historically elusive. The automatic code generation and theorem-proving system are particularly noteworthy, automating the often laborious process of verification and opening the door to wider adoption. However, the complexity of the verification process itself remains a potential bottleneck.

While the framework demonstrably works for a range of equations, scaling it to even more complex, multi-dimensional problems will undoubtedly present challenges. Furthermore, the reliance on a priori analytical knowledge introduces a dependency on our existing understanding of the underlying physics. The true power of this approach will be realised when it can be applied to systems where analytical solutions are scarce or non-existent.

Future work might focus on loosening this dependency, perhaps by integrating data-driven discovery of analytical properties alongside the neural network training. Ultimately, BEACONS offers a compelling vision of a future where computational simulations are not just powerful, but provably correct.