論文の概要: 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の文脈における帰納的不変量の帰納性を検証することは、ニューラルネットワークのスケールと非線形性のために難しい。
本手法は,インダクティブネス証明義務をより小さく,より扱いやすいサブプロブレムに分解することにより,検証プロセスを管理可能にする。
提案手法と並行して,必要な分解述語を自動的に推測することにより,候補の帰納性を自動的に検証するアルゴリズムを提案する。
このアルゴリズムはベースライン法を著しく上回り、ケーススタディにおける実行時間を大幅に短縮し、検証時間を時間(またはタイムアウト)から秒に短縮する。
関連論文リスト
- Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks [23.01933325606068]
既存の完全検証技術は、すべての堅牢性クエリに対して証明可能な保証を提供するが、小さなニューラルネットワークを超えてスケールするのに苦労する。
本稿では,これらの線形近似の品質向上のためのパラメータ探索手法を提案する。
具体的には、最先端のアルゴリズム構成手法によって与えられた検証問題に慎重に適応する単純な探索手法を用いることで、最先端技術よりも平均で25%のグローバルローバウンドを向上することを示す。
論文 参考訳(メタデータ) (2024-06-14T16:16:26Z) - Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies [7.9898826915621965]
我々は、他のニューラルネットワークをトレーニングする検証手順を使用し、ポリシーがタスクを満足することを示す証明書として機能する。
リーチ回避タスクでは、この証明ネットワークがリーチ回避スーパーマーチンゲール(RASM)であることを示すのに十分である。
論文 参考訳(メタデータ) (2024-06-02T18:19:19Z) - Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。