# Towards Learning and Verifying Maximal Neural Lyapunov Functions

arXiv: https://arxiv.org/abs/2304.07215 · HTML: https://mlsanity.com/paper/2304.07215/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Apr 2023.

## Built on by (most cited first, 7 of 7)

- [Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification](https://mlsanity.com/paper/2312.09131/) (2023)
- [LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction](https://mlsanity.com/paper/2403.10013/) (2024)
- [Formally Verified Physics-Informed Neural Control Lyapunov Functions](https://mlsanity.com/paper/2409.20528/) (2024)
- [Neural Control Barrier Functions from Physics Informed Neural Networks](https://mlsanity.com/paper/2504.11045/) (2025)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Rigorous Error Certification for Neural PDE Solvers: From Empirical Residuals to Solution Guarantees](https://mlsanity.com/paper/2603.19165/) (2026)
- [Verifiable Error Bounds for Physics-Informed Neural Network Solutions of Lyapunov and Hamilton-Jacobi-Bellman Equations](https://mlsanity.com/paper/2603.19545/) (2026)

## Abstract (arXiv)

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.