# LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 49 references that are in the map.
- First posted on arXiv 15 Mar 2024.

## Builds on (most cited first, 13 of 13)

- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification](https://mlsanity.com/paper/2312.09131/) (2023)
- [Lyapunov-Net: A Deep Neural Network Architecture for Lyapunov Function Approximation](https://mlsanity.com/paper/2109.13359/) (2021)
- [Computing Lyapunov functions using deep neural networks](https://mlsanity.com/paper/2005.08965/) (2020)
- [Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers](https://mlsanity.com/paper/2007.10865/) (2020)
- [Data-Driven Computational Methods for the Domain of Attraction and Zubov's Equation](https://mlsanity.com/paper/2112.14415/) (2021)
- [Towards Learning and Verifying Maximal Neural Lyapunov Functions](https://mlsanity.com/paper/2304.07215/) (2023)
- [Overcoming the curse of dimensionality for approximating Lyapunov functions with deep neural networks under a small-gain condition](https://mlsanity.com/paper/2001.08423/) (2020)
- [Converse Lyapunov Functions and Converging Inner Approximations to Maximal Regions of Attraction of Nonlinear Systems](https://mlsanity.com/paper/2103.12825/) (2021)

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

- [Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion](https://mlsanity.com/paper/2506.01356/) (2025)
- [Formally Verified Physics-Informed Neural Control Lyapunov Functions](https://mlsanity.com/paper/2409.20528/) (2024)
- [Transformer-Based Fault-Tolerant Control for Fixed-Wing UAVs Using Knowledge Distillation and In-Context Adaptation](https://mlsanity.com/paper/2411.02975/) (2024)
- [Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation](https://mlsanity.com/paper/2506.13961/) (2025)
- [Stochastic Reinforcement Learning with Stability Guarantees for Control of Unknown Nonlinear Systems](https://mlsanity.com/paper/2409.08382/) (2024)
- [Learning Koopman-based Stability Certificates for Unknown Nonlinear Systems](https://mlsanity.com/paper/2412.02807/) (2024)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Verifiable Error Bounds for Physics-Informed Neural Network Solutions of Lyapunov and Hamilton-Jacobi-Bellman Equations](https://mlsanity.com/paper/2603.19545/) (2026)
- [Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators](https://mlsanity.com/paper/2605.08938/) (2026)
- [Learning Lyapunov Operators for Nonlinear Systems](https://mlsanity.com/paper/2609.18894/) (2026)

## Abstract (arXiv)

In this paper, we describe a lightweight Python framework that provides integrated learning and verification of neural Lyapunov functions for stability analysis. The proposed tool, named LyZNet, learns neural Lyapunov functions using physics-informed neural networks (PINNs) to solve Zubov's equation and verifies them using satisfiability modulo theories (SMT) solvers. What distinguishes this tool from others in the literature is its ability to provide verified regions of attraction close to the domain of attraction. This is achieved by encoding Zubov's partial differential equation (PDE) into the PINN approach. By embracing the non-convex nature of the underlying optimization problems, we demonstrate that in cases where convex optimization, such as semidefinite programming, fails to capture the domain of attraction, our neural network framework proves more successful. The tool also offers automatic decomposition of coupled nonlinear systems into a network of low-dimensional subsystems for compositional verification. We illustrate the tool's usage and effectiveness with several numerical examples, including both non-trivial low-dimensional nonlinear systems and high-dimensional systems. The repository of the tool can be found at https://git.uwaterloo.ca/hybrid-systems-lab/lyznet.