# Formally Verified Physics-Informed Neural Control Lyapunov Functions

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 34 references that are in the map.
- First posted on arXiv 30 Sep 2024.

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

- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Adaptive Deep Learning for High-Dimensional Hamilton-Jacobi-Bellman Equations](https://mlsanity.com/paper/1907.05317/) (2019)
- [Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guarantees](https://mlsanity.com/paper/2206.01913/) (2022)
- [Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation](https://mlsanity.com/paper/2404.07956/) (2024)
- [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)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Computing Lyapunov functions using deep neural networks](https://mlsanity.com/paper/2005.08965/) (2020)
- [Physics-Informed Neural Network Policy Iteration: Algorithms, Convergence, and Verification](https://mlsanity.com/paper/2402.10119/) (2024)
- [LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction](https://mlsanity.com/paper/2403.10013/) (2024)
- [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)

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

- [Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://mlsanity.com/paper/2410.08304/) (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)
- [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)

Control Lyapunov functions are a central tool in the design and analysis of stabilizing controllers for nonlinear systems. Constructing such functions, however, remains a significant challenge. In this paper, we investigate physics-informed learning and formal verification of neural network control Lyapunov functions. These neural networks solve a transformed Hamilton-Jacobi-Bellman equation, augmented by data generated using Pontryagin's maximum principle. Similar to how Zubov's equation characterizes the domain of attraction for autonomous systems, this equation characterizes the null-controllability set of a controlled system. This principled learning of neural network control Lyapunov functions outperforms alternative approaches, such as sum-of-squares and rational control Lyapunov functions, as demonstrated by numerical examples. As an intermediate step, we also present results on the formal verification of quadratic control Lyapunov functions, which, aided by satisfiability modulo theories solvers, can perform surprisingly well compared to more sophisticated approaches and efficiently produce global certificates of null-controllability.