pith. sign in

arxiv: 2603.19545 · v2 · pith:RQPWNUBOnew · submitted 2026-03-20 · 📡 eess.SY · cs.LG· cs.SY· math.OC

Verifiable Error Bounds for Physics-Informed Neural Network Solutions of Lyapunov and Hamilton-Jacobi-Bellman Equations

Jun Liu This is my paper

Pith reviewed 2026-05-21 10:13 UTC · model grok-4.3

classification 📡 eess.SY cs.LGcs.SYmath.OC
keywords physics-informed neural networksLyapunov equationsHamilton-Jacobi-Bellman equationserror boundsa posteriori estimatesoptimal controlverification
0
0 comments X

The pith

Verifiable residual bounds for neural approximations to Lyapunov and HJB equations imply relative error bounds on the exact solutions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that when a physics-informed neural network approximates the solution of a Lyapunov or Hamilton-Jacobi-Bellman equation, a rigorously verifiable upper bound on the PDE residual produces relative error bounds between the approximation and the true solution. These bounds are a posteriori and can be computed from the approximate solution alone. In the Hamilton-Jacobi-Bellman setting the same residual bound supplies certified upper and lower bounds on the optimal value function over compact sets and measures the suboptimality of the feedback policy obtained from the approximation. The results further establish that a one-sided residual bound is sufficient to guarantee that the approximation is itself a valid Lyapunov function or control Lyapunov function. This matters for control applications because it supplies the missing guarantee that a small residual corresponds to a useful approximate solution.

Core claim

For both the Lyapunov and HJB PDEs, a verifiable residual bound yields relative error bounds with respect to the true solutions as well as computable a posteriori estimates in terms of the approximate solutions. For the HJB equation this also yields certified upper and lower bounds on the optimal value function on compact sublevel sets and quantifies the optimality gap of the induced feedback policy. We further show that one-sided residual bounds already imply that the approximation itself defines a valid Lyapunov or control Lyapunov function.

What carries the argument

Comparison principles and Gronwall-type arguments that convert a bound on the PDE residual into a bound on the solution error.

Load-bearing premise

The PDE residual of the approximate solution must admit a rigorous and verifiable upper bound, and the equations must satisfy the regularity conditions required for the comparison principles and Gronwall arguments to relate the residual to the solution error.

What would settle it

Finding a concrete approximate solution to a Lyapunov or HJB equation with a small certified residual for which the actual error to the true solution exceeds the derived relative error bound would falsify the central claim.

Figures

Figures reproduced from arXiv: 2603.19545 by Jun Liu.

Figure 1
Figure 1. Figure 1: Left: neural approximation of the Lyapunov function. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
read the original abstract

Many core problems in nonlinear systems analysis and control can be recast as solving partial differential equations (PDEs) such as Lyapunov and Hamilton-Jacobi-Bellman (HJB) equations. Physics-informed neural networks (PINNs) have emerged as a promising mesh-free approach for approximating their solutions, but in most existing works there is no rigorous guarantee that a small PDE residual implies a small solution error. This paper develops verifiable error bounds for approximate solutions of Lyapunov and HJB equations, with particular emphasis on PINN-based approximations. For both the Lyapunov and HJB PDEs, we show that a verifiable residual bound yields relative error bounds with respect to the true solutions as well as computable a posteriori estimates in terms of the approximate solutions. For the HJB equation, this also yields certified upper and lower bounds on the optimal value function on compact sublevel sets and quantifies the optimality gap of the induced feedback policy. We further show that one-sided residual bounds already imply that the approximation itself defines a valid Lyapunov or control Lyapunov function. We illustrate the results with numerical examples.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript develops verifiable error bounds for physics-informed neural network (PINN) solutions to Lyapunov and Hamilton-Jacobi-Bellman (HJB) equations. It demonstrates that a verifiable bound on the PDE residual implies relative error bounds with respect to the true solutions, as well as computable a posteriori estimates. For the HJB equation, this provides certified upper and lower bounds on the optimal value function on compact sublevel sets and quantifies the optimality gap of the induced feedback policy. One-sided residual bounds are shown to certify the approximation as a valid Lyapunov or control-Lyapunov function. The results are illustrated with numerical examples.

Significance. If the derivations hold, this paper makes a significant contribution to the field of nonlinear control and systems analysis by providing rigorous, verifiable guarantees for neural network approximations of key PDEs. This addresses a critical limitation in existing PINN literature for control applications, where small residuals do not necessarily imply small solution errors. The approach leverages standard PDE theory (comparison principles, Gronwall estimates) to yield practical a posteriori bounds, which could enable certified control design and analysis in safety-critical systems. The explicit handling of one-sided bounds for Lyapunov certification is particularly useful.

minor comments (3)
  1. [§4.1] §4.1: The statement of the comparison principle used to convert residual bounds to solution error bounds should include a precise citation to the version of the theorem invoked (e.g., the specific viscosity-solution comparison result from Crandall et al.).
  2. [Table 1] Table 1: The reported a posteriori error estimates would benefit from an additional column showing the ratio of the computed bound to the observed numerical error to illustrate tightness.
  3. [Figure 3] Figure 3 caption: The domain of the compact sublevel set on which the HJB bounds are certified is not stated explicitly; add the numerical value of the level set parameter used.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and significance assessment of our work on verifiable error bounds for PINN solutions of Lyapunov and HJB equations. We appreciate the recommendation for minor revision and will incorporate improvements to enhance clarity and presentation in the revised version.

Circularity Check

0 steps flagged

No significant circularity; derivation uses standard PDE comparison principles

full rationale

The paper's central derivation converts a verifiable residual bound on the PDE into solution error bounds via comparison principles and Gronwall-type estimates, with regularity conditions (Lipschitz continuity, viscosity solutions) stated explicitly before each theorem and constants derived directly from those assumptions. No steps reduce by construction to fitted inputs, self-definitions, or load-bearing self-citations; the abstract and skeptic analysis confirm the logical chain from residual to a-posteriori error and optimality gap is independent and self-contained against external PDE theory benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper rests on standard well-posedness assumptions for the Lyapunov and HJB PDEs and on the ability to compute verifiable residual bounds; no free parameters or new invented entities are described in the abstract.

axioms (1)
  • domain assumption The Lyapunov and HJB PDEs satisfy sufficient regularity and comparison-principle conditions so that residual bounds imply solution error bounds.
    Invoked when the abstract claims that a verifiable residual bound yields relative error bounds.

pith-pipeline@v0.9.0 · 5727 in / 1309 out tokens · 45237 ms · 2026-05-21T10:13:17.865276+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages

  1. [1]

    Springer, 1997

    Martino Bardi, Italo Capuzzo Dolcetta, et al.Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, volume 12. Springer, 1997

    work page 1997

  2. [2]

    Galerkin approximations of the generalized hamilton-jacobi-bellman equation

    Randal W Beard, George N Saridis, and John T Wen. Galerkin approximations of the generalized hamilton-jacobi-bellman equation. Automatica, 33(12):2159–2177, 1997

    work page 1997

  3. [3]

    A generalization of Zubov’s method to perturbed systems.SIAM Journal on Control and Optimization, 40(2):496–515, 2001

    Fabio Camilli, Lars Gr ¨une, and Fabian Wirth. A generalization of Zubov’s method to perturbed systems.SIAM Journal on Control and Optimization, 40(2):496–515, 2001

    work page 2001

  4. [4]

    dReal: An SMT solver for nonlinear theories over the reals

    Sicun Gao, Soonho Kong, and Edmund M Clarke. dReal: An SMT solver for nonlinear theories over the reals. InProc. of CADE, 2013

    work page 2013

  5. [5]

    Springer, 2007

    Peter Giesl.Construction of global Lyapunov functions using radial basis functions. Springer, 2007

    work page 2007

  6. [6]

    Extreme learning machine: theory and applications.Neurocomputing, 70(1- 3):489–501, 2006

    Guang-Bin Huang, Qin-Yu Zhu, and Chee-Kheong Siew. Extreme learning machine: theory and applications.Neurocomputing, 70(1- 3):489–501, 2006

    work page 2006

  7. [7]

    Artificial neural networks for solving ordinary and partial differential equations

    Isaac E Lagaris, Aristidis Likas, and Dimitrios I Fotiadis. Artificial neural networks for solving ordinary and partial differential equations. IEEE Transactions on Neural Networks, 9(5):987–1000, 1998

    work page 1998

  8. [8]

    On strict verification of neural Lyapunov functions.IFAC-PapersOnLine, 59(19):304–309, 2025

    Jun Liu and Maxwell Fitzsimmons. On strict verification of neural Lyapunov functions.IFAC-PapersOnLine, 59(19):304–309, 2025

    work page 2025

  9. [9]

    Formally verified physics-informed neural control lyapunov functions

    Jun Liu, Maxwell Fitzsimmons, Ruikun Zhou, and Yiming Meng. Formally verified physics-informed neural control lyapunov functions. InProc. of ACC, pages 1347–1354. IEEE, 2025

    work page 2025

  10. [10]

    Towards learning and verifying maximal neural Lyapunov functions

    Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Towards learning and verifying maximal neural Lyapunov functions. InProc. of CDC, 2023

    work page 2023

  11. [11]

    LyZNet: A lightweight python tool for learning and verifying neural Lyapunov functions and regions of attraction

    Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. LyZNet: A lightweight python tool for learning and verifying neural Lyapunov functions and regions of attraction. InProc. of HSCC, pages 1–8, 2024

    work page 2024

  12. [12]

    Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification.Automatica, 175:112193, 2025

    Jun Liu, Yiming Meng, Maxwell Fitzsimmons, and Ruikun Zhou. Physics-informed neural network Lyapunov functions: PDE charac- terization, learning, and verification.Automatica, 175:112193, 2025

    work page 2025

  13. [13]

    Physics-informed neural network policy iteration: Algorithms, convergence, and verification

    Yiming Meng, Ruikun Zhou, Amartya Mukherjee, Maxwell Fitzsim- mons, Christopher Song, and Jun Liu. Physics-informed neural network policy iteration: Algorithms, convergence, and verification. InProc. of ICML, 2024

    work page 2024

  14. [14]

    Mitchell, Alexandre M

    Ian M. Mitchell, Alexandre M. Bayen, and Claire J. Tomlin. A time-dependent Hamilton–Jacobi formulation of reachable sets for continuous dynamic games.IEEE Transactions on Automatic Control, 50(7):947–957, 2005

    work page 2005

  15. [15]

    Maziar Raissi, Paris Perdikaris, and George E Karniadakis. Physics- informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations.Journal of Computational physics, 378:686–707, 2019

    work page 2019

  16. [16]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification.Proc

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification.Proc. of NeurIPS, 34, 2021

    work page 2021

  17. [17]

    Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. InProc. of ICLR, 2021

    work page 2021

  18. [18]

    Physics-informed extreme learning machine Lyapunov functions

    Ruikun Zhou, Maxwell Fitzsimmons, Yiming Meng, and Jun Liu. Physics-informed extreme learning machine Lyapunov functions. IEEE Control Systems Letters, 8:1763–1768, 2024

    work page 2024