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.

本文针对非线性系统中控制Lyapunov函数构建的挑战，提出了一种物理信息学习与神经网络控制Lyapunov函数的正式验证方法。研究表明，该方法通过解决转化后的Hamilton-Jacobi-Bellman方程，提供比传统方法更优越的性能，并实现了对二次控制Lyapunov函数的有效形式验证，展示了显著的全局可控性证书生成能力。

正式验证的物理信息神经控制Lyapunov函数