Table of Contents
Fetching ...

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.

Learn and Verify: A Framework for Rigorous Verification of Physics-Informed Neural Networks

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 and around a PINN estimate , with a differentiable DSM loss that drives the residuals to satisfy and , 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.
Paper Structure (24 sections, 3 theorems, 36 equations, 10 figures, 3 tables)

This paper contains 24 sections, 3 theorems, 36 equations, 10 figures, 3 tables.

Key Result

Theorem 3

Given partition points $0 = t_0 < t_1 < \cdots < t_n < t_{n+1} = T$. Let $\ul{u}, \overline{u} \in \bigcap_{i=0}^{n} C^1([t_i,t_{i+1}])$ such that Here, within each interval, the right-hand derivative is taken at the left endpoint, and the left-hand derivative is taken at the right endpoint. Assuming that $\ul{u}(t) \leq \overline{u}(t)$ for all $t \in [0,T]$ and that $f$ is continuous over the s

Figures (10)

  • Figure 1: Overview of the proposed framework, "Learn and Verify."
  • Figure 2: Numerical solutions for the logistic equation approximated by PINNs under varying regularization strengths. Subplots correspond to values of $\log_2(\lambda_{\text{Phys}})$ ranging from $-8.0$ (top left) to $-5.5$ (bottom right), where $\lambda_{\text{Phys}}$ weights the regularization term $L_{\text{Phys}}$ defined in \ref{['eq:penalty']}. Red curves represent the analytical solution (ground truth), blue curves show successful numerical solutions verified by our framework, and gray curves indicate failed solutions.
  • Figure 3: Relative approximation errors for the logistic equation as a function of the regularization parameter $\lambda_{\text{Phys}}$. The horizontal axis represents $\log_2(\lambda_{\text{Phys}})$, while the vertical axis displays the relative error on a logarithmic scale. "Mean" denotes the average across 100 trials, whereas "Overall" corresponds to the worst-case scenario. The red dashed line indicates the error tolerance threshold of 0.1.
  • Figure 4: Success rate of approximate solutions for the logistic equation as a function of the regularization parameter $\lambda_{\text{Phys}}$. The success rate demonstrates a sharp, sigmoidal increase within the interval $\log_2(\lambda_{\text{Phys}}) \in [-8, -6]$, eventually plateauing at nearly $100\%$ for $\log_2(\lambda_{\text{Phys}}) \geq -5.5$.
  • Figure 5: Solution enclosures (left) and ODE residuals (right) for three error tolerances: $\varepsilon = 2^{-5}, 2^{-6}, 2^{-7}$ (from top to bottom). The sign of the residuals is chosen such that non-negativity correspond to a successful verification.
  • ...and 5 more figures

Theorems & Definitions (9)

  • Definition 1
  • Remark 2
  • Theorem 3
  • proof
  • Remark 4
  • Theorem 5
  • proof
  • Proposition 6
  • proof