Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling

要約

画像を入力として使用するニューラルネットワーク制御システムの安全性を検証することは、特定のシステム状態から、現実世界で可能な画像を数学的にモデル化する既知の方法がないため、困難な問題です。
サロゲート検証アプローチを考慮し、条件付き生成敵対的ネットワーク（CGAN）を現実世界の代わりに画像ジェネレーターとしてトレーニングする最近の作業に基づいて構築します。
これにより、閉ループシステムのセットベースの正式な分析が可能になり、シミュレーションとテストを超えた分析を提供します。
既存の作業は小さな例で効果的ですが、単一の制御期間内および複数の制御期間の両方で過度の過度に近接することは、そのスケーラビリティを制限します。
これら2つのエラーソースを克服するためのアプローチを提案します。
まず、システムダイナミクスの単調解析のように入力状態と制御出力間の依存関係を失うことなく、システムのダイナミクスをCGANおよびニューラルネットワークコントローラーとともに構成することにより、1段階のエラーを克服します。
第二に、シングルステップ組成を繰り返すことでマルチステップエラーを減らし、基本的にコントロールループの複数のステップを大きなニューラルネットワークに展開します。
次に、既存のネットワーク検証ツールを活用して、複数のステップで正確な到達可能なセットを計算し、各ステップで抽象化エラーの蓄積を回避します。
2つのケーススタディを使用した精度とスケーラビリティの両方の観点から、アプローチの有効性を実証します：自律航空機のタクシーシステムと高度な緊急ブレーキシステム。
航空機のタキシングシステムでは、提案されたアプローチと比較して、以前のベースライン法を使用して、収束した到達可能なセットは175％大きくなっています。
緊急ブレーキシステムでは、CGANからの画像出力変数の24倍を備えた緊急ブレーキシステムでは、ベースラインメソッドが安全であることを証明できませんが、当社の改善によりセットベースの安全分析が可能になります。

要約(オリジナル)

Verifying safety of neural network control systems that use images as input is a difficult problem because, from a given system state, there is no known way to mathematically model what images are possible in the real-world. We build on recent work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. This enables set-based formal analysis of the closed-loop system, providing analysis beyond simulation and testing. While existing work is effective on small examples, excessive overapproximation both within a single control period and across multiple control periods limits its scalability. We propose approaches to overcome these two sources of error. First, we overcome one-step error by composing the system’s dynamics along with the cGAN and neural network controller, without losing the dependencies between input states and the control outputs as in the monotonic analysis of the system dynamics. Second, we reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network. We then leverage existing network verification tools to compute accurate reachable sets for multiple steps, avoiding the accumulation of abstraction error at each step. We demonstrate the effectiveness of our approach in terms of both accuracy and scalability using two case studies: an autonomous aircraft taxiing system and an advanced emergency braking system. On the aircraft taxiing system, the converged reachable set is 175% larger using the prior baseline method compared with our proposed approach. On the emergency braking system, with 24x the number of image output variables from the cGAN, the baseline method fails to prove any states are safe, whereas our improvements enable set-based safety analysis.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google