論文の概要: Provably Safe Neural Network Controllers via Differential Dynamic Logic
- arxiv url: http://arxiv.org/abs/2402.10998v3
- Date: Thu, 24 Oct 2024 15:13:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-10-25 12:50:31.230722
- Title: Provably Safe Neural Network Controllers via Differential Dynamic Logic
- Title（参考訳）: 微分動的論理による潜在的に安全なニューラルネットワーク制御
- Authors: Samuel Teuber, Stefan Mitsch, André Platzer,
- Abstract要約: NNCS検証のための制御理論の再利用を可能にする最初の一般手法を提案する。
dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。
本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
- 参考スコア（独自算出の注目度）: 2.416907802598482
- License:
- Abstract: 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.
- Abstract（参考訳）: ニューラルネットワーク(NN)はサイバー物理システムのための自律的なコントローラとしての可能性を持っているが、NNベースの制御システム(NNCS)の安全性を検証することは、NNの実用化に重大な課題をもたらす。
理由の1つは、NN、ODE、ハイブリッドシステムを分析することの難しさである。
この目的のために、我々は VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): NNCS検証のための制御理論結果の再利用を可能にする最初の一般的なアプローチを紹介する。
結合力により,差動動的論理(dL)の厳密さを維持しつつ,NN検証ツールの効率性を利用する。
dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。
本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
ハイブリッドシステムから得られるNN検証特性は、通常非線形算術と任意の論理構造を含むが、効率的なNN検証は線形制約のみをサポートする。
この分割を克服するために、モーザイクについて述べる: ピースワイド線形NN上での多項式実数性に対する効率的で健全で完全な検証手法。
モザイクは複雑な検証クエリを単純なクエリに分割し、逆例領域の正確な推論と近似を組み合わせることで、既成の線形制約ツールを完全性保存的な方法で非線形設定に引き上げる。
VerSAILLE と Mosaic の汎用性は以下の通りである: 古典的垂直空中衝突回避 NNCS 検証ベンチマークにおいて、安全でないシナリオで反例領域を列挙しながら、2つのシナリオに対して無限の安全性を証明します。
また,本手法はクローズドループNNVのState-of-the-Artツールよりも優れていることを示す。
関連論文リスト
- Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
ブランチ・アンド・バウンド(BaB)は、ニューラルネットワーク(NN)検証において最も効果的な手法の一つである。
我々は、一般的な非線形性にBaBを実行し、一般的なアーキテクチャでNNを検証する汎用フレームワークGenBaBを開発した。
我々は、Sigmoid、Tanh、Sine、GeLUなどの活性化機能を持つNNを含む幅広いNNの検証におけるGenBaBの有効性を実証する。
論文 参考訳（メタデータ） (2024-05-31T17:51:07Z) - Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳（メタデータ） (2024-04-11T17:49:15Z) - Safety Filter Design for Neural Network Systems via Convex Optimization [35.87465363928146]
ニューラルネットワーク(NN)システムの安全性を確保するために,凸最適化に依存する新しい安全フィルタを提案する。
非線形振り子システムにおいて,提案手法の有効性を数値的に示す。
論文 参考訳（メタデータ） (2023-08-16T01:30:13Z) - Scaling Model Checking for DNN Analysis via State-Space Reduction and
Input Segmentation (Extended Version) [12.272381003294026]
既存のフレームワークは、トレーニングされたNNに対して堅牢性と/または安全性を保証する。
我々は、広範囲のNNプロパティを分析するための最初のモデルチェックベースのフレームワークであるFANNetを提案した。
本研究は,形式的NN解析のスケーラビリティとタイミング効率を向上させるために,状態空間の削減と入力セグメント化手法を開発する。
論文 参考訳（メタデータ） (2023-06-29T22:18:07Z) - Benign Overfitting in Deep Neural Networks under Lazy Training [72.28294823115502]
データ分布が適切に分離された場合、DNNは分類のためのベイズ最適テスト誤差を達成できることを示す。
よりスムーズな関数との補間により、より一般化できることを示す。
論文 参考訳（メタデータ） (2023-05-30T19:37:44Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳（メタデータ） (2023-01-17T18:32:01Z) - Safety Verification for Neural Networks Based on Set-boundary Analysis [5.487915758677295]
ニューラルネットワーク(NN)は、自動運転車のような安全クリティカルなシステムにますます適用されている。
本稿では, NNの安全性検証問題に対するトポロジ的視点から検討するための, 集合境界到達可能性法を提案する。
論文 参考訳（メタデータ） (2022-10-09T05:55:37Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2022-09-28T13:17:28Z) - Automated Repair of Neural Networks [0.26651200086513094]
安全でないNNの安全仕様を修復するためのフレームワークを提案する。
提案手法では,重み値のいくつかを修正して,新しい安全なNN表現を探索することができる。
我々は,提案するフレームワークが安全なNNを実現する能力を示す広範な実験を行った。
論文 参考訳（メタデータ） (2022-07-17T12:42:24Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳（メタデータ） (2022-04-01T03:31:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。