論文の概要: OVERT: An Algorithm for Safety Verification of Neural Network Control
Policies for Nonlinear Systems
- arxiv url: http://arxiv.org/abs/2108.01220v1
- Date: Tue, 3 Aug 2021 00:41:27 GMT
- ステータス: 処理完了
- システム内更新日: 2021-08-04 20:06:16.530742
- Title: OVERT: An Algorithm for Safety Verification of Neural Network Control
Policies for Nonlinear Systems
- Title（参考訳）: OVERT:非線形システムのためのニューラルネットワーク制御ポリシーの安全性検証アルゴリズム
- Authors: Chelsea Sidrane, Amir Maleki, Ahmed Irfan, Mykel J. Kochenderfer
- Abstract要約: 本稿では,ニューラルネットワーク制御ポリシーの安全性検証のための音響アルゴリズムOVERTを提案する。
OVERT の中心的な概念は、最適にきつく片方向の線形境界を持つ非線形関数を抽象化することである。
オーバートは、到達可能な集合の時間的および厳密性の両方において、既存の方法と好意的に比較する。
- 参考スコア（独自算出の注目度）: 31.3812947670948
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Deep learning methods can be used to produce control policies, but certifying
their safety is challenging. The resulting networks are nonlinear and often
very large. In response to this challenge, we present OVERT: a sound algorithm
for safety verification of nonlinear discrete-time closed loop dynamical
systems with neural network control policies. The novelty of OVERT lies in
combining ideas from the classical formal methods literature with ideas from
the newer neural network verification literature. The central concept of OVERT
is to abstract nonlinear functions with a set of optimally tight piecewise
linear bounds. Such piecewise linear bounds are designed for seamless
integration into ReLU neural network verification tools. OVERT can be used to
prove bounded-time safety properties by either computing reachable sets or
solving feasibility queries directly. We demonstrate various examples of safety
verification for several classical benchmark examples. OVERT compares favorably
to existing methods both in computation time and in tightness of the reachable
set.
- Abstract（参考訳）: 深層学習法は制御ポリシーの作成に使用できるが、安全性の確認は困難である。
結果として生じるネットワークは非線形であり、しばしば非常に大きい。
そこで本研究では,非線形離散時間閉ループ力学系のニューラルネットワーク制御ポリシーによる安全性検証のための音響アルゴリズムであるovertを提案する。
overtの斬新さは、古典的形式的手法文学のアイデアと、新しいニューラルネットワーク検証文学のアイデアを組み合わせることにある。
OVERT の中心的な概念は、最適にきつく片方向の線形境界を持つ非線形関数を抽象化することである。
このような分割線形境界は、reluニューラルネットワーク検証ツールへのシームレスな統合のために設計されている。
OVERTは、到達可能なセットを計算したり、実行可能性クエリを直接解決することで、バウンダリタイムの安全性を証明できる。
いくつかの古典的ベンチマーク例に対する安全性検証の様々な例を示す。
overtは、計算時間と到達可能な集合のタイト性の両方において、既存の方法と好適に比較できる。
関連論文リスト
- Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳（メタデータ） (2024-04-11T17:49:15Z) - Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
NNCS検証のための制御理論の再利用を可能にする最初の一般手法を提案する。
dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。
本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
論文 参考訳（メタデータ） (2024-02-16T16:15:25Z) - Probabilistic Reach-Avoid for Bayesian Neural Networks [71.67052234622781]
最適合成アルゴリズムは、証明された状態の数を4倍以上に増やすことができることを示す。
このアルゴリズムは、平均的な到達回避確率を3倍以上に向上させることができる。
論文 参考訳（メタデータ） (2023-10-03T10:52:21Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2022-09-28T13:17:28Z) - Neural Network Verification in Control [3.3123634393237706]
このチュートリアルはまず、NNの堅牢性を検証する最新のテクニックを紹介し、統一する。
その後、これらの技術は、神経フィードバックループの正式な保証を提供するように拡張される。
提案したツールは, 閉ループ到達性解析と頑健な深層強化学習を可能にする。
論文 参考訳（メタデータ） (2021-09-30T22:28:44Z) - Constrained Feedforward Neural Network Training via Reachability
Analysis [0.0]
安全上の制約に従うためにニューラルネットワークをトレーニングすることは、依然としてオープンな課題である。
本研究は, 整列線形単位(ReLU)非線形性を持つフィードフォワードニューラルネットワークを同時に訓練し, 検証する制約付き手法を提案する。
論文 参考訳（メタデータ） (2021-07-16T04:03:01Z) - Certification of Iterative Predictions in Bayesian Neural Networks [79.15007746660211]
我々は、BNNモデルの軌道が与えられた状態に到達する確率に対して、安全でない状態の集合を避けながら低い境界を計算する。
我々は、制御と強化学習の文脈において、下限を用いて、与えられた制御ポリシーの安全性保証を提供する。
論文 参考訳（メタデータ） (2021-05-21T05:23:57Z) - Reinforcement Learning with External Knowledge by using Logical Neural
Networks [67.46162586940905]
論理ニューラルネットワーク(LNN)と呼ばれる最近のニューラルシンボリックフレームワークは、ニューラルネットワークとシンボリックロジックの両方のキープロパティを同時に提供することができる。
外部知識ソースからのモデルフリー強化学習を可能にする統合手法を提案する。
論文 参考訳（メタデータ） (2021-03-03T12:34:59Z) - Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural
Network Controllers via Semidefinite Programming [19.51345816555571]
本稿では,ニューラルネットワークを用いた線形時間変化システムの安全性検証のための新しいフォワードリーチビリティ解析手法を提案する。
半有限計画法を用いて、これらの近似到達可能な集合を計算できることが示される。
提案手法は,まずディープニューラルネットワークを用いて非線形モデル予測制御器を近似し,その解析ツールを用いて閉ループシステムの有限時間到達性と制約満足度を証明した。
論文 参考訳（メタデータ） (2020-04-16T18:48:25Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。