論文の概要: NNLander-VeriF: A Neural Network Formal Verification Framework for
Vision-Based Autonomous Aircraft Landing
- arxiv url: http://arxiv.org/abs/2203.15841v1
- Date: Tue, 29 Mar 2022 18:18:53 GMT
- ステータス: 処理完了
- システム内更新日: 2022-03-31 14:20:02.418550
- Title: NNLander-VeriF: A Neural Network Formal Verification Framework for
Vision-Based Autonomous Aircraft Landing
- Title(参考訳): NNLander-VeriF:視覚に基づく自律航空機着陸のためのニューラルネットワーク形式検証フレームワーク
- Authors: Ulices Santa Cruz and Yasser Shoukry
- Abstract要約: ビジョンベースのNNコントローラは、滑走路に近づきながら、カメラから画像を処理して航空機を誘導する。
NNLander-VeriFは、自律着陸に使用されるビジョンベースのNNコントローラを検証するフレームワークである。
- 参考スコア(独自算出の注目度): 1.4620086904601473
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper, we consider the problem of formally verifying a Neural Network
(NN) based autonomous landing system. In such a system, a NN controller
processes images from a camera to guide the aircraft while approaching the
runway. A central challenge for the safety and liveness verification of
vision-based closed-loop systems is the lack of mathematical models that
captures the relation between the system states (e.g., position of the
aircraft) and the images processed by the vision-based NN controller. Another
challenge is the limited abilities of state-of-the-art NN model checkers. Such
model checkers can reason only about simple input-output robustness properties
of neural networks. This limitation creates a gap between the NN model checker
abilities and the need to verify a closed-loop system while considering the
aircraft dynamics, the perception components, and the NN controller. To this
end, this paper presents NNLander-VeriF, a framework to verify vision-based NN
controllers used for autonomous landing. NNLander-VeriF addresses the
challenges above by exploiting geometric models of perspective cameras to
obtain a mathematical model that captures the relation between the aircraft
states and the inputs to the NN controller. By converting this model into a NN
(with manually assigned weights) and composing it with the NN controller, one
can capture the relation between aircraft states and control actions using one
augmented NN. Such an augmented NN model leads to a natural encoding of the
closed-loop verification into several NN robustness queries, which
state-of-the-art NN model checkers can handle. Finally, we evaluate our
framework to formally verify the properties of a trained NN and we show its
efficiency.
- Abstract(参考訳): 本稿では,ニューラルネットワーク(NN)に基づく自律着陸システムについて,正式に検証する問題を考察する。
このようなシステムでは、NNコントローラがカメラからの画像を処理し、滑走路に接近しながら航空機を誘導する。
視覚ベースのクローズドループシステムの安全性と生存性検証の課題は、システム状態(例えば航空機の位置)とビジョンベースのNNコントローラによって処理された画像の関係を捉える数学的モデルがないことである。
もうひとつの課題は、最先端のNNモデルチェッカーの能力の制限だ。
このようなモデルチェッカーは、ニューラルネットワークの単純な入出力ロバスト性のみを推論することができる。
この制限により、NNモデルチェッカー能力と、航空機のダイナミックス、知覚コンポーネント、NNコントローラを考慮してクローズドループシステムを検証する必要性の間にギャップが生じる。
そこで本稿では,自律着陸に使用される視覚ベースのNNコントローラを検証するフレームワークであるNNLander-VeriFを提案する。
NNLander-VeriFは、視点カメラの幾何学的モデルを利用して、航空機の状態とNNコントローラへの入力の関係を捉える数学的モデルを得る。
このモデルを(手動で割り当てられた重量で)NNに変換し、NNコントローラで構成することにより、航空機の状態と制御行動の関係を1つの強化NNを使って捉えることができる。
このような拡張NNモデルは、クローズドループ検証をいくつかのNNロバストネスクエリに自然なエンコーディングをもたらす。
最後に、トレーニングされたNNの特性を正式に検証するためのフレームワークを評価し、その効率性を示す。
関連論文リスト
- 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) - Securing Graph Neural Networks in MLaaS: A Comprehensive Realization of Query-based Integrity Verification [68.86863899919358]
我々は機械学習におけるGNNモデルをモデル中心の攻撃から保護するための画期的なアプローチを導入する。
提案手法は,GNNの完全性に対する包括的検証スキーマを含み,トランスダクティブとインダクティブGNNの両方を考慮している。
本稿では,革新的なノード指紋生成アルゴリズムを組み込んだクエリベースの検証手法を提案する。
論文 参考訳(メタデータ) (2023-12-13T03:17:05Z) - 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) - ConCerNet: A Contrastive Learning Based Framework for Automated
Conservation Law Discovery and Trustworthy Dynamical System Prediction [82.81767856234956]
本稿では,DNNに基づく動的モデリングの信頼性を向上させるために,ConCerNetという新しい学習フレームワークを提案する。
本手法は, 座標誤差と保存量の両方において, ベースラインニューラルネットワークよりも一貫して優れていることを示す。
論文 参考訳(メタデータ) (2023-02-11T21:07:30Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳(メタデータ) (2022-09-28T13:17:28Z) - Recurrent neural network-based Internal Model Control of unknown
nonlinear stable systems [0.30458514384586394]
Gated Recurrent Neural Networks (RNN)は、動的システムを学ぶための人気のあるツールとなっている。
本稿では、内部モデル制御(IMC)アーキテクチャの合成にこれらのネットワークをどのように適用できるかについて議論する。
論文 参考訳(メタデータ) (2021-08-10T11:02:25Z) - On the benefits of robust models in modulation recognition [53.391095789289736]
畳み込み層を用いたディープニューラルネットワーク(DNN)は、通信における多くのタスクにおいて最先端である。
画像分類のような他の領域では、DNNは敵の摂動に弱いことが示されている。
最新モデルの堅牢性をテストするための新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2021-03-27T19:58:06Z) - Provably Correct Training of Neural Network Controllers Using
Reachability Analysis [3.04585143845864]
我々は、安全と生活性を満たすことが保証されるサイバー物理システムのためのニューラルネットワーク(NN)コントローラのトレーニングの問題を考える。
我々のアプローチは、動的システムのためのモデルベース設計手法とデータ駆動アプローチを組み合わせることで、この目標を達成することである。
論文 参考訳(メタデータ) (2021-02-22T07:08:11Z) - Continuous Safety Verification of Neural Networks [1.7056768055368385]
本稿では,前回のDNN安全検証問題から修正問題設定への移行結果のアプローチについて考察する。
全体的な概念は、認識された画像から視覚的方向を決定するために、DNNコントローラを装備する1/10ドルのスケールで評価される。
論文 参考訳(メタデータ) (2020-10-12T13:28:04Z) - Progressive Tandem Learning for Pattern Recognition with Deep Spiking
Neural Networks [80.15411508088522]
スパイキングニューラルネットワーク(SNN)は、低レイテンシと高い計算効率のために、従来の人工知能ニューラルネットワーク(ANN)よりも優位性を示している。
高速かつ効率的なパターン認識のための新しいANN-to-SNN変換およびレイヤワイズ学習フレームワークを提案する。
論文 参考訳(メタデータ) (2020-07-02T15:38:44Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。