Scenario-based Compositional Verification of Autonomous Systems with Neural Perception

要約

深い学習の最近の進歩により、知覚に深いニューラルネットワークを使用する自律システムの開発が可能になりました。
これらのシステムの正式な検証は、認識DNNのサイズと複雑さ、および環境条件の変化が困難になることのために困難です。
これらの課題に対処するために、次の重要な概念に基づいて自律システムの確率的検証フレームワークを提案します。（1）シナリオベースのモデリング：それぞれが異なる環境条件を表すシナリオの構成にタスク（たとえば、カーナビゲーション）を分解します。
（2）確率的抽象化：各シナリオについて、シナリオの環境条件を表すオフラインデータセットでのDNNのパフォーマンスに基づいて、知覚のコンパクトな抽象化を構築します。
（3）象徴的な推論と加速：抽象化により、象徴的な推論と、環境条件の任意のバリエーションでシステムの誤差確率を制限する新しい加速度証明規則を介して自律システムの効率的な構成検証が可能になります。
2つのケーススタディでのアプローチを説明します。高次元の知覚DNNSを使用してタクシーで飛行機を導く実験的自律システムと、LIDAR観測を使用したF1tenth自律車のシミュレーションモデルです。

要約(オリジナル)

Recent advances in deep learning have enabled the development of autonomous systems that use deep neural networks for perception. Formal verification of these systems is challenging due to the size and complexity of the perception DNNs as well as hard-to-quantify, changing environment conditions. To address these challenges, we propose a probabilistic verification framework for autonomous systems based on the following key concepts: (1) Scenario-based Modeling: We decompose the task (e.g., car navigation) into a composition of scenarios, each representing a different environment condition. (2) Probabilistic Abstractions: For each scenario, we build a compact abstraction of perception based on the DNN’s performance on an offline dataset that represents the scenario’s environment condition. (3) Symbolic Reasoning and Acceleration: The abstractions enable efficient compositional verification of the autonomous system via symbolic reasoning and a novel acceleration proof rule that bounds the error probability of the system under arbitrary variations of environment conditions. We illustrate our approach on two case studies: an experimental autonomous system that guides airplanes on taxiways using high-dimensional perception DNNs and a simulation model of an F1Tenth autonomous car using LiDAR observations.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google