Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jun Liu, Yiming Meng, Maxwell Fitzsimmons, Ruikun Zhou

TL;DR

LyZNet tackles robust ROA computation for nonlinear systems by integrating Zubov's PDE with physics-informed neural networks (PINNs) and SMT-based verification. It combines local quadratic Lyapunov analysis, neural Lyapunov learning via Zubov's equation, and compositional verification to produce ROA estimates that approach the true domain of attraction, often outperforming SOS-based methods. The framework is lightweight, modular, and scalable to high-dimensional systems, enabling end-to-end learning and provable guarantees with the option to switch between Zubov-based and data-driven losses. This work advances practical stability analysis by delivering verified ROA near the domain boundary and outlining clear paths for future extensions to broader dynamics and verifiers.

Abstract

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.

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

TL;DR

LyZNet tackles robust ROA computation for nonlinear systems by integrating Zubov's PDE with physics-informed neural networks (PINNs) and SMT-based verification. It combines local quadratic Lyapunov analysis, neural Lyapunov learning via Zubov's equation, and compositional verification to produce ROA estimates that approach the true domain of attraction, often outperforming SOS-based methods. The framework is lightweight, modular, and scalable to high-dimensional systems, enabling end-to-end learning and provable guarantees with the option to switch between Zubov-based and data-driven losses. This work advances practical stability analysis by delivering verified ROA near the domain boundary and outlining clear paths for future extensions to broader dynamics and verifiers.

Abstract

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.
Paper Structure (20 sections, 26 equations, 3 figures, 4 tables)

This paper contains 20 sections, 26 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Problem formulation
  4. Tool overview and usage
  5. Tool overview
  6. Tool usage
  7. Methodology
  8. Local stability analysis using quadratic Lyapunov functions
  9. Learning neural Lyapunov functions via Zubuv's equation for ROA verification
  10. Zubov's theorem and maximal Lyapunov function
  11. Physics-informed neural solution to Zubov's PDE
  12. Verification of regions of attraction
  13. Examples
  14. Conclusions and future work
  15. Appendix
  16. ...and 5 more sections

Figures (3)

  • Figure 1: Verified neural Lyapunov function for Van der Pol equation with $\mu=1.0$ (Example \ref{['ex:vdp']}). Dashed red: quadratic Lyapunov function; dot-dashed green: SOS Lyapunov; solid blue: neural Lyapunov.
  • Figure 2: Verified neural Lyapunov function for Van der Pol equation with $\mu=3.0$ (Example \ref{['ex:vdp']}). Dashed red: quadratic Lyapunov function; dot-dashed green: SOS Lyapunov; solid blue: neural Lyapunov. The learned neural Lyapunov function outperforms a sixth degree SOS Lyapunov function.
  • Figure 3: Verified neural Lyapunov function for a two-machine power system (Example \ref{['ex:power']}). Dashed red: quadratic Lyapunov function; dot-dashed green: SOS Lyapunov; solid blue: neural Lyapunov. The learned neural Lyapunov function significantly outperforms a sixth degree SOS Lyapunov function.

Theorems & Definitions (3)

  • Remark 1
  • Remark 2
  • Remark 3