Physics-Informed Neural Network Lyapunov Functions: PDE Characterization, Learning, and Verification

要約

私たちは、物理学に基づいたニューラル ネットワークを使用してリアプノフ関数を計算する体系的な調査を提供します。
リアプノフ条件を偏微分方程式 (PDE) としてエンコードし、これをニューラル ネットワークのリアプノフ関数のトレーニングに使用します。
リアプノフ偏微分方程式とズボフ偏微分方程式の解の解析特性を分析します。
特に、神経リアプノフ関数のトレーニングにズボフ方程式を使用すると、真の引力領域に近い近似引力領域が得られることを示します。
また、近似誤差と、ズボフ方程式の一意の解へのニューラル近似の収束も調べます。
次に、満足度モジュロ理論 (SMT) ソルバーによって容易に検証できる、学習された神経リアプノフ関数に十分な条件を提供し、局所的な安定性解析と大規模な引力領域推定の両方の正式な検証を可能にします。
低次元から高次元までの多数の非線形例を通じて、提案されたフレームワークが半定値計画法 (SDP) を使用して得られる従来の二乗和 (SOS) リアプノフ関数を上回る性能を発揮できることを実証します。

要約(オリジナル)

We provide a systematic investigation of using physics-informed neural networks to compute Lyapunov functions. We encode Lyapunov conditions as a partial differential equation (PDE) and use this for training neural network Lyapunov functions. We analyze the analytical properties of the solutions to the Lyapunov and Zubov PDEs. In particular, we show that employing the Zubov equation in training neural Lyapunov functions can lead to approximate regions of attraction close to the true domain of attraction. We also examine approximation errors and the convergence of neural approximations to the unique solution of Zubov’s equation. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and region-of-attraction estimates in the large. Through a number of nonlinear examples, ranging from low to high dimensions, we demonstrate that the proposed framework can outperform traditional sums-of-squares (SOS) Lyapunov functions obtained using semidefinite programming (SDP).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google