Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation for Efficient Synthesis and Verification

要約

学習ベースのニューラル ネットワーク (NN) 制御ポリシーは、ロボット工学および制御の幅広いタスクにおいて優れた経験的パフォーマンスを示しています。
ただし、非線形動的システムを備えた NN コントローラーの引力領域 (ROA) にわたる形式的な (リアプノフ) 安定性の保証は取得が困難であり、既存のアプローチのほとんどは二乗和 (SOS) などの高価なソルバーに依存しています。
-整数計画法 (MIP)、または充足可能性モジュロ理論 (SMT)。
この論文では、高速な経験的改ざんと戦略的正則化を使用して、リアプノフ証明書とともに NN コントローラーを学習するための新しいフレームワークを実証します。
我々は、文献に示されているものよりも大きな検証可能な関心領域（ROA）を定義し、リアプノフ導関数に対する従来の制限的な制約を改良して、証明可能なROAのみに焦点を当てる新しい定式化を提案します。
リャプノフ条件は、分枝限定とスケーラブルな線形境界伝播ベースの NN 検証技術を使用して事後的に厳密に検証されます。
このアプローチは効率的で柔軟であり、SOS、MIP、SMT の高価なソルバーに依存することなく、トレーニングと検証の手順全体が GPU 上で高速化されます。
私たちのフレームワークの柔軟性と効率により、文献で初めて、合成された NN ベースのコントローラーと正式な安定性が保証された NN ベースのオブザーバーを使用したリアプノフ安定出力フィードバック制御を実証することができます。
ソースコードは https://github.com/Verified-Intelligence/Lyapunov_Stable_NN_Controllers にあります。

要約(オリジナル)

Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. However, formal (Lyapunov) stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain, and most existing approaches rely on expensive solvers such as sums-of-squares (SOS), mixed-integer programming (MIP), or satisfiability modulo theories (SMT). In this paper, we demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations. We propose a novel formulation that defines a larger verifiable region-of-attraction (ROA) than shown in the literature, and refines the conventional restrictive constraints on Lyapunov derivatives to focus only on certifiable ROAs. The Lyapunov condition is rigorously verified post-hoc using branch-and-bound with scalable linear bound propagation-based NN verification techniques. The approach is efficient and flexible, and the full training and verification procedure is accelerated on GPUs without relying on expensive solvers for SOS, MIP, nor SMT. The flexibility and efficiency of our framework allow us to demonstrate Lyapunov-stable output feedback control with synthesized NN-based controllers and NN-based observers with formal stability guarantees, for the first time in literature. Source code at https://github.com/Verified-Intelligence/Lyapunov_Stable_NN_Controllers.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google