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.

翻译：控制李雅普诺夫函数是非线性系统稳定控制器设计与分析的核心工具。然而，构造此类函数仍是一项重大挑战。本文研究了神经网络控制李雅普诺夫函数的物理信息学习与形式化验证方法。这些神经网络通过求解经庞特里亚金极大值原理生成数据增强的变换后 Hamilton-Jacobi-Bellman 方程进行构建。类似于 Zubov 方程对自治系统吸引域的刻画，该方程描述了受控系统的零可控集。数值算例表明，这种基于原理的神经网络控制李雅普诺夫函数学习方法优于平方和有理控制李雅普诺夫函数等替代方案。作为中间步骤，我们还提出了二次控制李雅普诺夫函数的形式化验证结果——借助可满足性模理论求解器，该方法相比更复杂的验证策略表现出色，并能高效生成全局零可控性证明。