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

要約

画像を入力として使用するニューラル ネットワーク制御システムの安全性を検証することは、難しい問題です。なぜなら、与えられたシステム状態から、現実世界でどのような画像が可能かを数学的にモデル化する方法が知られていないからです。
私たちは、現実世界の代わりに条件付き敵対的生成ネットワーク (cGAN) を画像ジェネレーターとしてトレーニングする、代理検証アプローチを考慮した最近の研究に基づいて構築しています。
これにより、閉ループ システムのセットベースの形式的な解析が可能になり、シミュレーションやテストを超えた解析が可能になります。
既存の研究は小規模な例では効果的ですが、単一の制御期間内および複数の制御期間にわたる過度の過近似により、そのスケーラビリティが制限されます。
これら 2 つのエラーの原因を克服するためのアプローチを提案します。
まず、システムダイナミクスの単調解析のように入力状態と制御出力の間の依存関係を失うことなく、cGAN およびニューラル ネットワーク コントローラーとともにシステムのダイナミクスを合成することで、ワンステップ エラーを克服しました。
2 番目に、単一ステップの合成を繰り返し、基本的に制御ループの複数のステップを大規模なニューラル ネットワークに展開することで、複数ステップのエラーを削減します。
次に、既存のネットワーク検証ツールを活用して、複数のステップの正確な到達可能なセットを計算し、各ステップでの抽象化エラーの蓄積を回避します。
私たちは、自律航空機地上走行システムと高度な緊急ブレーキ システムという 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