Learn and Verify: A Framework for Rigorous Verification of Physics-Informed Neural Networks
Kazuaki Tanaka, Kohei Yatabe
TL;DR
The paper tackles the lack of rigorous error guarantees for physics-informed neural network solvers of ODEs by introducing Learn and Verify, a two-phase framework that first learns an approximate solution and enclosures, then certifies them with interval arithmetic. The key novelty is constructing sub- and super-solutions $\underline{u}$ and $\overline{u}$ around a PINN estimate $u_{\hat{\theta}}$, with a differentiable DSM loss that drives the residuals to satisfy $\frac{d\underline{u}}{dt}\le f(t,\underline{u})$ and $\frac{d\overline{u}}{dt}\ge f(t,\overline{u})$, and verifying these via adaptive interval subdivision. The framework provides computable a posteriori error bounds and machine-verifiable proofs of enclosure, demonstrated on nonlinear ODEs including time-varying logistic models and a Riccati blow-up where the method yields rigorous lower/upper bounds for the solution and, in the Riccati case, a bound on the blow-up time. This approach advances trustworthy scientific machine learning by enabling certified, gap-free verification of neural solvers without requiring closed-form references. The results show that appropriately tuned regularization and DSM parameters yield reliable verifications and tight enclosures, offering a practical path to robust, verified PINN-based simulations.
Abstract
The numerical solution of differential equations using neural networks has become a central topic in scientific computing, with Physics-Informed Neural Networks (PINNs) emerging as a powerful paradigm for both forward and inverse problems. However, unlike classical numerical methods that offer established convergence guarantees, neural network-based approximations typically lack rigorous error bounds. Furthermore, the non-deterministic nature of their optimization makes it difficult to mathematically certify their accuracy. To address these challenges, we propose a "Learn and Verify" framework that provides computable, mathematically rigorous error bounds for the solutions of differential equations. By combining a novel Doubly Smoothed Maximum (DSM) loss for training with interval arithmetic for verification, we compute rigorous a posteriori error bounds as machine-verifiable proofs. Numerical experiments on nonlinear Ordinary Differential Equations (ODEs), including problems with time-varying coefficients and finite-time blow-up, demonstrate that the proposed framework successfully constructs rigorous enclosures of the true solutions, establishing a foundation for trustworthy scientific machine learning.
