論文の概要: Compositional Inductive Invariant Based Verification of Neural Network
Controlled Systems
- arxiv url: http://arxiv.org/abs/2312.10842v1
- Date: Sun, 17 Dec 2023 23:20:51 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-19 14:24:14.961132
- Title: Compositional Inductive Invariant Based Verification of Neural Network
Controlled Systems
- Title(参考訳): 構成帰納的不変量に基づくニューラルネットワーク制御システムの検証
- Authors: Yuhao Zhou, Stavros Tripakis
- Abstract要約: 本稿では,インダクティブ不変法を利用したNNCSの安全性検証手法を提案する。
本稿では、必要な分解述語を自動的に推論することで、与えられた候補の帰納性を自動的に検証できるアルゴリズムを提案する。
- 参考スコア(独自算出の注目度): 13.953407261152877
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The integration of neural networks into safety-critical systems has shown
great potential in recent years. However, the challenge of effectively
verifying the safety of Neural Network Controlled Systems (NNCS) persists. This
paper introduces a novel approach to NNCS safety verification, leveraging the
inductive invariant method. Verifying the inductiveness of a candidate
inductive invariant in the context of NNCS is hard because of the scale and
nonlinearity of neural networks. Our compositional method makes this
verification process manageable by decomposing the inductiveness proof
obligation into smaller, more tractable subproblems. Alongside the high-level
method, we present an algorithm capable of automatically verifying the
inductiveness of given candidates by automatically inferring the necessary
decomposition predicates. The algorithm significantly outperforms the baseline
method and shows remarkable reductions in execution time in our case studies,
shortening the verification time from hours (or timeout) to seconds.
- Abstract(参考訳): 安全クリティカルシステムへのニューラルネットワークの統合は、近年大きな可能性を秘めている。
しかし、NNCS(Neural Network Controlled Systems)の安全性を効果的に検証するという課題が続いている。
本稿では,インダクティブ不変法を利用したNNCSの安全性検証手法を提案する。
NNCSの文脈における帰納的不変量の帰納性を検証することは、ニューラルネットワークのスケールと非線形性のために難しい。
本手法は,インダクティブネス証明義務をより小さく,より扱いやすいサブプロブレムに分解することにより,検証プロセスを管理可能にする。
提案手法と並行して,必要な分解述語を自動的に推測することにより,候補の帰納性を自動的に検証するアルゴリズムを提案する。
このアルゴリズムはベースライン法を著しく上回り、ケーススタディにおける実行時間を大幅に短縮し、検証時間を時間(またはタイムアウト)から秒に短縮する。
関連論文リスト
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation for Efficient Synthesis and Verification [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳(メタデータ) (2024-04-11T17:49:15Z) - Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems [18.049286149364075]
深部強化学習技術の急速な進歩は、ディープニューラルネットワーク(DNN)を利用した安全クリティカルシステムの監視を可能にする
既存の検証アプローチのほとんどは定性的アプローチに依存しており、主に到達可能性分析を利用している。
本稿では,定性的・定量的な安全性検証問題を統一するための新しい枠組みを提案する。
論文 参考訳(メタデータ) (2024-04-02T09:31:51Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - Safety Verification of Neural Network Control Systems Using Guaranteed
Neural Network Model Reduction [3.0839245814393728]
モデル縮小精度の概念は、ニューラルネットワークの出力と縮小サイズバージョンの間の保証された距離を記述するために提案される。
モデル削減精度を正確に計算するために,到達可能性に基づくアルゴリズムを提案する。
元のシステムの到達可能な集合を計算するアルゴリズムが開発され、より計算効率のよい安全性検証プロセスをサポートすることができる。
論文 参考訳(メタデータ) (2023-01-17T03:25:57Z) - Quantization-aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks [58.195261590442406]
我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。
近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。
本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
論文 参考訳(メタデータ) (2022-11-29T13:32:38Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳(メタデータ) (2022-09-28T13:17:28Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳(メタデータ) (2022-04-01T03:31:27Z) - Neural Network Verification in Control [3.3123634393237706]
このチュートリアルはまず、NNの堅牢性を検証する最新のテクニックを紹介し、統一する。
その後、これらの技術は、神経フィードバックループの正式な保証を提供するように拡張される。
提案したツールは, 閉ループ到達性解析と頑健な深層強化学習を可能にする。
論文 参考訳(メタデータ) (2021-09-30T22:28:44Z) - OVERT: An Algorithm for Safety Verification of Neural Network Control
Policies for Nonlinear Systems [31.3812947670948]
本稿では,ニューラルネットワーク制御ポリシーの安全性検証のための音響アルゴリズムOVERTを提案する。
OVERT の中心的な概念は、最適にきつく片方向の線形境界を持つ非線形関数を抽象化することである。
オーバートは、到達可能な集合の時間的および厳密性の両方において、既存の方法と好意的に比較する。
論文 参考訳(メタデータ) (2021-08-03T00:41:27Z) - Fast Falsification of Neural Networks using Property Directed Testing [0.1529342790344802]
本稿では,反例の探索を指示するニューラルネットワークの偽造アルゴリズムを提案する。
提案アルゴリズムは, 微分自由サンプリングに基づく最適化手法を用いる。
フェールシフィケーション手順は、他の検証ツールが安全でないと報告しているすべての安全でないインスタンスを検出する。
論文 参考訳(メタデータ) (2021-04-26T09:16:27Z) - GraN: An Efficient Gradient-Norm Based Detector for Adversarial and
Misclassified Examples [77.99182201815763]
ディープニューラルネットワーク(DNN)は、敵対的な例やその他のデータ摂動に対して脆弱である。
GraNは、どのDNNにも容易に適応できる時間およびパラメータ効率の手法である。
GraNは多くの問題セットで最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2020-04-20T10:09:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。