LyZNet: A Lightweight Python Tool for Learning and Verifying Neural
  Lyapunov Functions and Regions of Attraction
Jun Liu Yiming Meng Maxwell Fitzsimmons Ruikun Zhou
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.