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

翻译：我们系统研究了使用物理信息神经网络计算Lyapunov函数的方法。将Lyapunov条件编码为偏微分方程（PDE），并利用该方程训练神经网络Lyapunov函数。我们分析了Lyapunov和Zubov偏微分方程解的解析性质。特别地，我们证明在训练神经Lyapunov函数时采用Zubov方程可得到接近真实吸引域的近似吸引域。同时考察了逼近误差以及神经逼近收敛至Zubov方程唯一解的特性。随后提出可被可满足性模理论（SMT）求解器直接验证的神经Lyapunov函数充分条件，实现对大范围局部稳定性分析与吸引域估计的形式化验证。通过从低维到高维的多个非线性算例，我们证明该框架能超越传统基于半定规划（SDP）的平方和（SOS）Lyapunov函数方法。