Provably Safe Neural Network Controllers via Differential Dynamic Logic

要約

ニューラル ネットワーク (NN) はサイバーフィジカル システムの自律コントローラーとしての可能性を秘めていますが、NN ベースの制御システム (NNCS) の安全性を検証することは、特に制限のない時間軸で安全性が必要な場合、NN の実用化に重大な課題をもたらします。
理由の 1 つは、NN、ODE、ハイブリッド システムの解析が難しいことです。
この目的を達成するために、VerSAILLE (論理的にリンクされたエンベロープによる検証可能に安全な AI) を導入します。これは、NNCS 検証に制御理論の結果を再利用できる最初の一般的なアプローチです。
力を合わせることで、微分ダイナミック ロジック (dL) の厳密さを維持しながら、NN 検証ツールの効率を活用します。
dL の証明された安全な制御エンベロープに基づいて、NN 検証によって証明された NN の仕様を導き出します。
NN が仕様に準拠していることの証明は、NNCS の無限時間安全性に関する dL 証明に反映されることを示します。
ハイブリッド システムから得られる NN 検証プロパティには通常、非線形演算と任意の論理構造が含まれますが、効率的な NN 検証は線形制約をサポートするだけです。
この隔たりを克服するために、我々は Mosaic: 区分線形 NN 上の多項式実数演算プロパティに対する効率的で健全な完全な検証アプローチを提案します。
Mosaic は、複雑な検証クエリを単純なクエリに分割し、近似と反例領域の正確な推論を組み合わせることで、完全性を維持しながら既製の線形制約ツールを非線形設定に引き上げます。
私たちの評価は、VerSAILLE と Mosaic の多用途性を示しています。私たちは、安全でないシナリオにおける反例領域を (徹底的に) 列挙しながら、2 つのシナリオに対する古典的な垂直空中衝突回避 NNCS 検証ベンチマークで無限時間の安全性を証明しました。
また、私たちのアプローチが閉ループ NNV における最先端のツールよりも大幅に優れていることも示します。

要約(オリジナル)

While neural networks (NNs) have potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of NN based control systems (NNCSs) poses significant challenges for the practical use of NNs, especially when safety is needed for unbounded time horizons. One reason is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory results for NNCS verification. By joining forces, we exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS. The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic and arbitrary logical structures while efficient NN verification merely supports linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. Our evaluation demonstrates the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for two scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms State-of-the-Art tools in closed-loop NNV.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google