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 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).

翻译：本文系统研究了利用物理信息神经网络计算李雅普诺夫函数的方法。我们将李雅普诺夫条件编码为偏微分方程，并用于训练神经网络李雅普诺夫函数。分析了李雅普诺夫和祖博夫偏微分方程解的分析性质，特别证明了在训练神经李雅普诺夫函数时采用祖博夫方程能够逼近真实吸引域的范围。随后给出了学习得到的神经李雅普诺夫函数可通过可满足性模理论求解器直接验证的充分条件，从而实现对局部稳定性分析和大范围吸引域估计的形式化验证。通过从低维到高维的多个非线性算例，我们证明了所提出框架能够超越传统采用半定规划得到的平方和（SOS）李雅普诺夫函数。