Formally Verified Physics-Informed Neural Control Lyapunov Functions

要約

制御リアプノフ関数は、非線形システムの安定化コントローラーの設計と解析における中心的なツールです。
ただし、そのような機能を構築することは依然として大きな課題です。
この論文では、ニューラル ネットワーク制御リアプノフ関数の物理情報に基づく学習と形式的検証を調査します。
これらのニューラル ネットワークは、ポントリャギンの最大原理を使用して生成されたデータによって強化された、変換されたハミルトン-ヤコビ-ベルマン方程式を解きます。
ズボフの方程式が自律システムの引力領域を特徴付けるのと同様に、この方程式は制御されたシステムのヌル制御可能性セットを特徴付けます。
ニューラル ネットワーク制御リアプノフ関数のこの原則に基づいた学習は、数値例で実証されているように、二乗和や合理的制御リアプノフ関数などの代替アプローチよりも優れています。
中間ステップとして、二次制御リアプノフ関数の形式的検証に関する結果も示します。この関数は、充足性モジュロ理論ソルバーの助けを借りて、より洗練されたアプローチと比較して驚くほど優れたパフォーマンスを発揮し、ヌル制御可能性のグローバル証明書を効率的に生成できます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google