論文の概要: Provably Safe Neural Network Controllers via Differential Dynamic Logic
- arxiv url: http://arxiv.org/abs/2402.10998v1
- Date: Fri, 16 Feb 2024 16:15:25 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-21 00:01:19.447572
- Title: Provably Safe Neural Network Controllers via Differential Dynamic Logic
- Title（参考訳）: 微分動的論理による安全なニューラルネットワーク制御
- Authors: Samuel Teuber, Stefan Mitsch and Andr\'e Platzer
- Abstract要約: 本稿では、微分動的論理(dL)とNN検証を組み合わせた最初のアプローチについて紹介する。
Mosaic: ピースワイド線形NNにおける実算術特性に対する最初の音響および完全検証手法を提案する。
適応型巡航制御や空中衝突回避を含むケーススタディの評価は、VerSAILLEとMosaicの汎用性を実証している。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: While neural networks (NNs) have a large potential as goal-oriented
controllers for Cyber-Physical Systems, verifying the safety of neural network
based control systems (NNCSs) poses significant challenges for the practical
use of NNs -- especially when safety is needed for unbounded time horizons. One
reason for this is the intractability of NN and hybrid system analysis. We
introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The
first approach for the combination of differential dynamic logic (dL) and NN
verification. By joining forces, we can exploit the efficiency of NN
verification tools while retaining the rigor of dL. We reflect a safety proof
for a controller envelope in an NN to prove the safety of concrete NNCS on an
infinite-time horizon. The NN verification properties resulting from VerSAILLE
typically require nonlinear arithmetic while efficient NN verification tools
merely support linear arithmetic. To overcome this divide, we present Mosaic:
The first sound and complete verification approach for polynomial real
arithmetic properties on piece-wise linear NNs. Mosaic lifts off-the-shelf
tools for linear properties to the nonlinear setting. An evaluation on case
studies, including adaptive cruise control and airborne collision avoidance,
demonstrates the versatility of VerSAILLE and Mosaic: It supports the
certification of infinite-time horizon safety and the exhaustive enumeration of
counterexample regions while significantly outperforming State-of-the-Art tools
in closed-loop NNV.
- Abstract（参考訳）: ニューラルネットワーク(NN)はサイバー物理システムのための目標指向コントローラとして大きな可能性を秘めているが、ニューラルネットワークベースの制御システム(NNCS)の安全性を検証することは、NNの実用化に重大な課題をもたらす。
この理由の1つは、nnとハイブリッドシステム分析の難解さである。
VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): 微分動的論理(dL)とNN検証を組み合わせた最初のアプローチ。
dL の厳密さを維持しながら NN 検証ツールの効率性を活用することができる。
NNにおけるコントローラエンベロープの安全性証明を反映して,コンクリートNNCSの安全性を無限時間水平線上で証明する。
VerSAILLE から得られる NN の検証特性は一般に非線形算術を必要とするが、効率的な NN 検証ツールは単に線形算術をサポートするだけである。
この分割を克服するために,区間線形nn上の多項式実算術特性に対する最初の健全かつ完全検証手法であるモザイクを提案する。
モザイクは、非線形設定への線形特性のための既製ツールを持ち上げる。
適応型巡航制御や空中衝突回避を含むケーススタディの評価は,VerSAILLEとMosaicの汎用性を実証している。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。