論文の概要: 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の汎用性を実証している。
関連論文リスト
- Scaling #DNN-Verification Tools with Efficient Bound Propagation and
Parallel Computing [57.49021927832259]
ディープニューラルネットワーク(DNN)は多くのシナリオで異常な結果を示した強力なツールです。
しかし、それらの複雑な設計と透明性の欠如は、現実世界のアプリケーションに適用する際の安全性上の懸念を提起する。
DNNの形式的検証(FV)は、安全面の証明可能な保証を提供する貴重なソリューションとして登場した。
論文 参考訳(メタデータ) (2023-12-10T13:51:25Z) - 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) - Reachability Analysis of Neural Network Control Systems [10.023618778236697]
ニューラルネットワーク制御システム(NNCS)の既存の検証アプローチは、限られたタイプのアクティベーション機能でのみ機能する。
本稿では,DeepNNCと呼ばれるリプシッツ最適化に基づくNNCSの検証フレームワークを提案する。
DeepNNCは、幅広いNNCよりも効率と精度の点で優れた性能を示している。
論文 参考訳(メタデータ) (2023-01-28T05:57:37Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳(メタデータ) (2022-09-28T13:17:28Z) - Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness [172.61581010141978]
証明可能な堅牢性は、安全クリティカルなシナリオでディープニューラルネットワーク(DNN)を採用する上で望ましい特性である。
線形性の適切なレベルを「グラフト」することで、神経細胞を戦略的に操作する新しいソリューションを提案する。
論文 参考訳(メタデータ) (2022-06-15T22:42:29Z) - On Feature Learning in Neural Networks with Global Convergence
Guarantees [49.870593940818715]
勾配流(GF)を用いた広帯域ニューラルネットワーク(NN)の最適化について検討する。
入力次元がトレーニングセットのサイズ以下である場合、トレーニング損失はGFの下での線形速度で0に収束することを示す。
また、ニューラル・タンジェント・カーネル(NTK)システムとは異なり、我々の多層モデルは特徴学習を示し、NTKモデルよりも優れた一般化性能が得られることを実証的に示す。
論文 参考訳(メタデータ) (2022-04-22T15:56:43Z) - Backward Reachability Analysis for Neural Feedback Loops [40.989393438716476]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
本稿では,BP設定した推定値を所定の時間軸上で反復的に求めるアルゴリズムを提案し,計算コストを低くすることで,保守性を最大88%削減できることを示す。
論文 参考訳(メタデータ) (2022-04-14T01:13:14Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳(メタデータ) (2022-04-01T03:31:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。