用物理约束训练神经网络控制李雅普诺夫函数，确保系统稳定可验证。
Formally Verified Physics-Informed Neural Control Lyapunov Functions
- 通过哈密顿-雅可比-贝尔曼方程与庞特里亚金原理生成数据，训练神经网络控制李雅普诺夫函数。
- 在数值实验中优于平方和与有理型控制李雅普诺夫函数，实现更优的系统稳定性保证。
- 结合形式化验证工具，可高效生成全局零可控性证明，适合高安全性控制系统设计。
控制李雅普诺夫函数是设计和分析非线性系统稳定控制器的核心工具。然而，构造此类函数仍面临重大挑战。本文研究基于物理信息的神经网络控制李雅普诺夫函数的学习与形式化验证方法。这些神经网络求解经变换的哈密顿-雅可比-贝尔曼方程，并引入庞特里亚金最大值原理生成的数据进行增强。类似于佐博夫方程刻画自治系统的吸引域，该方程刻画受控系统的零可控集。这种原理驱动的神经网络学习方法在数值实验中表现优于平方和与有理型控制李雅普诺夫函数。作为中间步骤，本文还提出利用满足模理论求解器对二次控制李雅普诺夫函数进行形式化验证，其性能出人意料地接近复杂方法，且能高效生成全局零可控性证书。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。