pith. sign in

arxiv: 2304.07215 · v1 · submitted 2023-04-14 · 🧮 math.OC · cs.SY· eess.SY

Towards Learning and Verifying Maximal Neural Lyapunov Functions

Jun Liu , Yiming Meng , Maxwell Fitzsimmons , Ruikun Zhou This is my paper

Pith reviewed 2026-05-24 09:32 UTC · model grok-4.3

classification 🧮 math.OC cs.SYeess.SY
keywords Lyapunov functionsZubov's equationphysics-informed neural networksdomain of attractionSMT solversstability verificationnonlinear systemsneural Lyapunov functions
0
0 comments X

The pith

A physics-informed neural network trained on Zubov's equation can produce a nearly maximal Lyapunov function whose level sets approach the domain of attraction boundary.

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

The paper shows how to train a neural network to approximate a maximal Lyapunov function for a given stable set by solving Zubov's equation. This yields a function whose sub-level sets can be made arbitrarily close to the boundary of the full region of attraction. The authors also supply stability conditions that satisfiability modulo theories solvers can check directly for both local and global cases. They prove that maximal Lyapunov functions exist under the stated assumptions. A sympathetic reader would care because this supplies a systematic, verifiable way to estimate stability regions for nonlinear systems without constructing Lyapunov functions by hand.

Core claim

The central claim is that a physics-informed neural network can be trained on Zubov's equation to learn a Lyapunov function that is nearly maximal for a given stable set, so that its sub-level sets approximate the domain of attraction arbitrarily closely, while additional conditions allow SMT solvers to certify local or global stability, all supported by existence guarantees for maximal Lyapunov functions.

What carries the argument

Zubov's equation, which defines the maximal Lyapunov function on the domain of attraction and serves as the training objective for the neural network.

If this is right

  • Stability regions can be certified more tightly than with non-maximal Lyapunov functions.
  • SMT solvers become applicable to both local and global stability without manual Lyapunov construction.
  • Numerical examples demonstrate the approach on concrete nonlinear systems.
  • Theoretical guarantees ensure existence of the maximal functions being approximated.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same training procedure could be tested on systems whose domains of attraction are known analytically to measure how closely the learned level sets match the true boundary.
  • Combining the SMT conditions with interval arithmetic might reduce solver timeouts on higher-dimensional examples.
  • The method might extend to estimating regions of attraction for switched or hybrid systems if Zubov's equation can be adapted accordingly.

Load-bearing premise

A maximal Lyapunov function exists for the given stable set and the neural-network approximation remains sufficiently accurate that its near-maximality and the SMT-verifiable conditions are preserved.

What would settle it

A concrete dynamical system for which the trained neural function either violates positive-definiteness, has sub-level sets that stop short of the domain-of-attraction boundary, or satisfies the SMT conditions while the system is actually unstable.

Figures

Figures reproduced from arXiv: 2304.07215 by Jun Liu, Maxwell Fitzsimmons, Ruikun Zhou, Yiming Meng.

Figure 1
Figure 1. Figure 1: A neural network, consisting of three hidden layers with 10 neurons [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A neural network, consisting of three hidden layers with 10 neurons [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
read the original abstract

The search for Lyapunov functions is a crucial task in the analysis of nonlinear systems. In this paper, we present a physics-informed neural network (PINN) approach to learning a Lyapunov function that is nearly maximal for a given stable set. A Lyapunov function is considered nearly maximal if its sub-level sets can be made arbitrarily close to the boundary of the domain of attraction. We use Zubov's equation to train a maximal Lyapunov function defined on the domain of attraction. Additionally, we propose conditions that can be readily verified by satisfiability modulo theories (SMT) solvers for both local and global stability. We provide theoretical guarantees on the existence of maximal Lyapunov functions and demonstrate the effectiveness of our computational approach through 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

3 major / 2 minor

Summary. The paper proposes a physics-informed neural network (PINN) method to learn a nearly maximal Lyapunov function for a given stable set by training on Zubov's equation, which is defined on the domain of attraction. It introduces SMT-solver-checkable conditions for verifying local and global stability and states theoretical guarantees on the existence of maximal Lyapunov functions, with effectiveness shown via numerical examples.

Significance. If the approximation error between the trained PINN and the true solution of Zubov's PDE can be rigorously controlled, the approach would provide a practical bridge between data-driven learning of Lyapunov functions and formal verification via SMT solvers, potentially enabling computation of maximal functions whose sub-level sets approach the domain-of-attraction boundary. The combination of Zubov's PDE with SMT predicates is a constructive idea that could scale stability analysis beyond hand-crafted Lyapunov functions.

major comments (3)
  1. [Theoretical guarantees paragraph and associated existence statement] The section stating theoretical guarantees invokes the classical existence result for maximal Lyapunov functions via Zubov's equation but supplies no derivation or bound showing that the PINN residual implies the learned function is arbitrarily close to maximality (i.e., that sub-level sets can be made arbitrarily close to the DOA boundary). The central claim of a 'nearly maximal' neural Lyapunov function therefore rests on an unproven propagation of approximation error.
  2. [PINN training procedure and SMT verification conditions] No a-priori or a-posteriori error estimate is provided for the residual of Zubov's PDE after PINN training, nor is there a quantitative relation between that residual and the distance of the learned sub-level sets to the true domain-of-attraction boundary. Consequently the claim that the SMT-verifiable stability conditions remain sound for the trained network lacks supporting analysis.
  3. [Numerical examples section] The numerical examples demonstrate that the trained networks produce plausible level sets, yet they report neither the achieved PDE residual norm nor any certified distance to the DOA boundary, leaving the 'nearly maximal' property unquantified even empirically.
minor comments (2)
  1. [Throughout the manuscript] Notation for the neural network approximant V_NN and the exact maximal function V* should be introduced once and used consistently; the current alternation between 'learned Lyapunov function' and 'maximal neural Lyapunov function' is occasionally ambiguous.
  2. [SMT conditions subsection] The abstract states that the SMT conditions 'can be readily verified,' but the manuscript would benefit from an explicit statement of the predicate encoding (e.g., which quantifiers are eliminated and which remain) before the numerical examples.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We appreciate the referee's detailed feedback on our manuscript. We address each of the major comments below, providing clarifications and indicating where revisions will be made to strengthen the paper.

read point-by-point responses

  1. Referee: [Theoretical guarantees paragraph and associated existence statement] The section stating theoretical guarantees invokes the classical existence result for maximal Lyapunov functions via Zubov's equation but supplies no derivation or bound showing that the PINN residual implies the learned function is arbitrarily close to maximality (i.e., that sub-level sets can be made arbitrarily close to the DOA boundary). The central claim of a 'nearly maximal' neural Lyapunov function therefore rests on an unproven propagation of approximation error.

    Authors: We thank the referee for this observation. The theoretical section cites the classical existence result for maximal Lyapunov functions via Zubov's equation. The 'nearly maximal' descriptor is intended to reflect the empirical behavior observed in the numerical examples rather than a proven convergence result for the PINN approximation. We agree that a rigorous propagation of the approximation error is not derived and will revise the text to explicitly state this limitation and clarify the scope of the theoretical guarantees. revision: partial

  2. Referee: [PINN training procedure and SMT verification conditions] No a-priori or a-posteriori error estimate is provided for the residual of Zubov's PDE after PINN training, nor is there a quantitative relation between that residual and the distance of the learned sub-level sets to the true domain-of-attraction boundary. Consequently the claim that the SMT-verifiable stability conditions remain sound for the trained network lacks supporting analysis.

    Authors: The SMT conditions are formulated to verify stability directly for the trained neural network, ensuring they are sound regardless of the residual. However, we concur that without error estimates linking the residual to proximity to the true maximal function, the 'nearly maximal' claim lacks quantitative support. This connection is indeed difficult to establish rigorously for PINNs applied to Zubov's equation. We will include additional discussion on this point and mark it as an important direction for future research. revision: partial

  3. Referee: [Numerical examples section] The numerical examples demonstrate that the trained networks produce plausible level sets, yet they report neither the achieved PDE residual norm nor any certified distance to the DOA boundary, leaving the 'nearly maximal' property unquantified even empirically.

    Authors: We accept this criticism. The revised version will report the PDE residual norms achieved during training for each example to better quantify the approximation quality. While a certified distance to the DOA boundary is not computed, the examples are chosen such that the domain of attraction is known or can be compared visually; we will enhance the presentation with more quantitative metrics where possible. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation relies on classical existence results and external PINN/SMT training without reduction to fitted inputs or self-citations.

full rationale

The paper's core steps consist of (1) invoking classical existence of maximal Lyapunov functions via Zubov's equation, (2) training a PINN to approximate its solution on the domain of attraction, and (3) proposing SMT-checkable conditions for local/global stability. None of these steps reduce by the paper's own equations to quantities defined in terms of the fitted network parameters; the approximation error is treated as a separate numerical issue rather than being absorbed into a self-referential prediction. No load-bearing self-citations, uniqueness theorems imported from the authors, or ansatzes smuggled via prior work appear in the abstract or described method. The derivation is therefore self-contained against external benchmarks (PDE theory, SMT solvers) and receives score 0.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on abstract only; the central claim rests on standard Lyapunov theory and neural approximation assumptions whose details are not visible.

axioms (1)
  • domain assumption Existence of maximal Lyapunov functions for given stable sets in nonlinear systems
    Invoked when stating theoretical guarantees and using Zubov's equation to train on the domain of attraction.

pith-pipeline@v0.9.0 · 5653 in / 1211 out tokens · 33858 ms · 2026-05-24T09:32:27.611233+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

  1. [1]

    Dynamical Systems: Stability Theory and Applications , volume 35

    Nam P Bhatia and George P Szeg ¨o. Dynamical Systems: Stability Theory and Applications , volume 35. Springer, 1967

    work page 1967

  2. [2]

    Neural Lyapunov control

    Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. In Proceedings of the 33rd International Conference on Neural Information Processing Systems , pages 3245–3254, 2019

    work page 2019

  3. [3]

    Safe control with learned certificates: A survey of neural Lyapunov, barrier, and con- traction methods

    Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural Lyapunov, barrier, and con- traction methods. arXiv preprint arXiv:2202.11762 , 2022

    work page arXiv 2022

  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. In Proceedings of the 24th International Conference on Automated Deduction , pages 208– 214, 2013

    work page 2013

  5. [5]

    Construction of Global Lyapunov Functions Using Radial Basis Functions

    Peter Giesl. Construction of Global Lyapunov Functions Using Radial Basis Functions. Springer, 2007

    work page 2007

  6. [6]

    Review on computational methods for Lyapunov functions

    Peter Giesl and Sigurdur Hafstein. Review on computational methods for Lyapunov functions. Discrete & Continuous Dynamical Systems-B, 20(8):2291, 2015

    work page 2015

  7. [7]

    Computing Lyapunov functions using deep neural networks

    Lars Gr ¨une. Computing Lyapunov functions using deep neural networks. Journal of Computational Dynamics , 8(2), 2021

    work page 2021

  8. [8]

    Overcoming the curse of dimensionality for approximat- ing Lyapunov functions with deep neural networks under a small-gain condition

    Lars Gr ¨une. Overcoming the curse of dimensionality for approximat- ing Lyapunov functions with deep neural networks under a small-gain condition. IFAC-PapersOnLine, 54(9):317–322, 2021

    work page 2021

  9. [9]

    Nonlinear Dynam- ical Systems and Control: A Lyapunov-based Approach

    Wassim M Haddad and VijaySekhar Chellaboina. Nonlinear Dynam- ical Systems and Control: A Lyapunov-based Approach . Princeton university press, 2008

    work page 2008

  10. [10]

    Converse Lyapunov functions and converging inner approximations to maximal regions of attraction of nonlinear systems

    Morgan Jones and Matthew M Peet. Converse Lyapunov functions and converging inner approximations to maximal regions of attraction of nonlinear systems. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 5312–5319. IEEE, 2021

    work page 2021

  11. [11]

    Data-driven computational methods for the domain of attraction and zubov’s equation

    Wei Kang, Kai Sun, and Liang Xu. Data-driven computational methods for the domain of attraction and zubov’s equation. arXiv preprint arXiv:2112.14415, 2021

    work page arXiv 2021

  12. [12]

    The general problem of the stability of motion

    Aleksandr Mikhailovich Lyapunov. The general problem of the stability of motion. International journal of control , 55(3):531–534, 1992

    work page 1992

  13. [13]

    Contributions to stability theory

    Jos ´e L Massera. Contributions to stability theory. Annals of Mathe- matics, pages 182–206, 1956

    work page 1956

  14. [14]

    Global stability analysis using the eigenfunctions of the koopman operator

    Alexandre Mauroy and Igor Mezi ´c. Global stability analysis using the eigenfunctions of the koopman operator. IEEE Transactions on Automatic Control, 61(11):3356–3369, 2016

    work page 2016

  15. [15]

    Why and when can deep-but not shallow- networks avoid the curse of dimensionality: a review

    Tomaso Poggio, Hrushikesh Mhaskar, Lorenzo Rosasco, Brando Mi- randa, and Qianli Liao. Why and when can deep-but not shallow- networks avoid the curse of dimensionality: a review. International Journal of Automation and Computing , 14(5):503–519, 2017

    work page 2017

  16. [16]

    Physics- informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations

    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

  17. [17]

    Con- structive Nonlinear Control

    Rodolphe Sepulchre, Mrdjan Jankovic, and Petar V Kokotovic. Con- structive Nonlinear Control . Springer Science & Business Media, 2012

    work page 2012

  18. [18]

    Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems

    Anthony Vannelli and Mathukumalli Vidyasagar. Maximal Lyapunov functions and domains of attraction for autonomous nonlinear systems. Automatica, 21(1):69–80, 1985

    work page 1985

  19. [19]

    Neural Lyapunov control of unknown nonlinear systems with stability guar- antees

    Ruikun Zhou, Thanin Quartz, Hans De Sterck, and Jun Liu. Neural Lyapunov control of unknown nonlinear systems with stability guar- antees. In Advances in Neural Information Processing Systems , 2022

    work page 2022

  20. [20]

    V . I. Zubov. Methods of A. M. Lyapunov and Their Application . Noordhoff, 1964

    work page 1964