Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification
This work addresses stability verification for nonlinear dynamical systems, which is crucial for control and safety-critical applications, though it is incremental as it builds on existing neural network and PDE approaches.
The authors tackled the problem of computing Lyapunov functions for stability analysis by encoding Lyapunov conditions as a PDE and training physics-informed neural networks, demonstrating that their framework can outperform traditional sums-of-squares methods in nonlinear examples from low to high dimensions.
We provide a systematic investigation of using physics-informed neural networks to compute Lyapunov functions. We encode Lyapunov conditions as a partial differential equation (PDE) and use this for training neural network Lyapunov functions. We analyze the analytical properties of the solutions to the Lyapunov and Zubov PDEs. In particular, we show that employing the Zubov equation in training neural Lyapunov functions can lead to approximate regions of attraction close to the true domain of attraction. We also examine approximation errors and the convergence of neural approximations to the unique solution of Zubov's equation. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and region-of-attraction estimates in the large. Through a number of nonlinear examples, ranging from low to high dimensions, we demonstrate that the proposed framework can outperform traditional sums-of-squares (SOS) Lyapunov functions obtained using semidefinite programming (SDP).