論文の概要: Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
- arxiv url: http://arxiv.org/abs/2404.01769v1
- Date: Tue, 2 Apr 2024 09:31:51 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-03 17:09:01.467220
- Title: Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
- Title（参考訳）: DNN制御システムの質的・定量的安全性検証の統一化
- Authors: Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong, Min Zhang,
- Abstract要約: 深部強化学習技術の急速な進歩は、ディープニューラルネットワーク(DNN)を利用した安全クリティカルシステムの監視を可能にする
既存の検証アプローチのほとんどは定性的アプローチに依存しており、主に到達可能性分析を利用している。
本稿では,定性的・定量的な安全性検証問題を統一するための新しい枠組みを提案する。
- 参考スコア（独自算出の注目度）: 18.049286149364075
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs). This underscores the pressing need to promptly establish certified safety guarantees for such DNN-controlled systems. Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. However, qualitative verification proves inadequate for DNN-controlled systems as their behaviors exhibit stochastic tendencies when operating in open and adversarial environments. In this paper, we propose a novel framework for unifying both qualitative and quantitative safety verification problems of DNN-controlled systems. This is achieved by formulating the verification tasks as the synthesis of valid neural barrier certificates (NBCs). Initially, the framework seeks to establish almost-sure safety guarantees through qualitative verification. In cases where qualitative verification fails, our quantitative verification method is invoked, yielding precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons. To facilitate the synthesis of NBCs, we introduce their $k$-inductive variants. We also devise a simulation-guided approach for training NBCs, aiming to achieve tightness in computing precise certified lower and upper bounds. We prototype our approach into a tool called $\textsf{UniQQ}$ and showcase its efficacy on four classic DNN-controlled systems.
- Abstract（参考訳）: 深層強化学習技術の急速な進歩は、ディープニューラルネットワーク(DNN)を利用した安全クリティカルシステムの監視を可能にする。
このことは、DNNが制御するシステムに対する認証された安全保証を迅速に確立する必要性を浮き彫りにしている。
既存の検証アプローチのほとんどは定性的アプローチに依存しており、主に到達可能性分析を利用している。
しかしながら、定性的検証は、DNNが制御するシステムでは、その動作がオープンな環境や対向的な環境での動作において確率的傾向を示すため、不十分であることを示す。
本稿では,DNN制御システムの定性的・定量的安全性検証問題を統一する新しい枠組みを提案する。
これは、有効なニューラルバリア証明書(NBC)の合成として検証タスクを定式化することで達成される。
当初、このフレームワークは質的検証を通じてほぼ確実に安全性を保証することを目指している。
定性検証が失敗した場合、定量検証法が実行され、無限時間地平線と有限時間地平線の両方において、確率的安全性の正確な下限と上限が得られる。
NBC の合成を容易にするため,$k$-inductive variant を導入する。
また, シミュレーション誘導によるNBCの訓練手法を考案し, 精度の高い下限と上限の計算における厳密性の実現を目指す。
この手法を$\textsf{UniQQ}$というツールにプロトタイプし、4つの古典的DNN制御システムで有効性を示す。
関連論文リスト
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳（メタデータ） (2024-04-11T17:49:15Z) - Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。
問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。
本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
論文 参考訳（メタデータ） (2024-03-15T17:32:02Z) - Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems [11.811233105411976]
本稿では,インダクティブ不変法を利用したNNCSの安全性検証手法を提案する。
本稿では、必要な分解述語を自動的に推論することで、与えられた候補の帰納性を自動的に検証できるアルゴリズムを提案する。
論文 参考訳（メタデータ） (2023-12-17T23:20:51Z) - VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees [3.208888890455612]
VNN(Verification-Friendly Neural Networks)を生成するための新しいフレームワークを提案する。
本稿では,予測性能と検証親和性とのバランスをとるための学習後最適化フレームワークを提案する。
論文 参考訳（メタデータ） (2023-12-15T12:39:27Z) - Enumerating Safe Regions in Deep Neural Networks with Provable
Probabilistic Guarantees [86.1362094580439]
安全プロパティとDNNが与えられた場合、安全であるプロパティ入力領域のすべての領域の集合を列挙する。
この問題の #P-hardness のため,epsilon-ProVe と呼ばれる効率的な近似法を提案する。
提案手法は, 許容限界の統計的予測により得られた出力可到達集合の制御可能な過小評価を利用する。
論文 参考訳（メタデータ） (2023-08-18T22:30:35Z) - 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) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z) - Scalable Synthesis of Verified Controllers in Deep Reinforcement
Learning [0.0]
高品質の安全シールドを合成できる自動検証パイプラインを提案します。
私たちの重要な洞察は、事前に計算された安全シールドを使用して神経コントローラのトレーニングを制限し、神経コントローラから安全検証を分離することを含みます。
実測的な高次元深部RLベンチマークによる実験結果から,本手法の有効性が示された。
論文 参考訳（メタデータ） (2021-04-20T19:30:29Z) - Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。
本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。
われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
論文 参考訳（メタデータ） (2020-02-17T09:53:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。