Formal Verification and Control with Conformal Prediction

要約

この調査では、不確実性の定量化のための統計ツールであるコンフォーマル予測（CP）を使用した実践的安全保証を使用して、自律システムの正式な検証および制御アルゴリズムを設計します。
学習対応コンポーネント（LEC）の複雑さが既存のモデルベースの検証と設計手法の使用を妨げる主要なボトルネックである学習対応自律システム（LEAS）に焦点を当てています。
代わりに、CPの使用を提唱し、正式な検証、システムと制御理論、およびロボット工学での使用を実証します。
CPは、その単純さ（理解しやすく、使用し、変更しやすい）、一般性（学習モデルやデータ分布に関する仮定は必要ありません。つまり、分布なし）、効率（リアルタイムの能力があり、正確です）のために特別に有用であると主張します。
この調査では、次の目標を追求します。
まず、CPを使用して自律性の問題を解決することに興味がある非専門家向けのCPへのアクセス可能な紹介を提供します。
次に、ニューラルネットワークの入出力特性を検証するために、LECの検証にCPを使用する方法を示します。
3番目と4番目に、安全な制御設計にCPを使用し、リースのオフラインおよびオンライン検証に使用する最近の記事をレビューします。
計算上効率的な方法でリースの複雑さを扱うことができる統一フレームワークで彼らのアイデアを要約します。
博覧会では、単純なシステム仕様、例えばロボットナビゲーションタスク、および時間的論理形式で定式化された複雑な仕様を検討します。
調査全体を通して、他の統計的手法（シナリオの最適化、PACベイズ理論など）およびこれらの手法が検証と制御にどのように使用されているかと比較します。
最後に、読者は問題と将来の研究の方向性を開くように指摘します。

要約(オリジナル)

In this survey, we design formal verification and control algorithms for autonomous systems with practical safety guarantees using conformal prediction (CP), a statistical tool for uncertainty quantification. We focus on learning-enabled autonomous systems (LEASs) in which the complexity of learning-enabled components (LECs) is a major bottleneck that hampers the use of existing model-based verification and design techniques. Instead, we advocate for the use of CP, and we will demonstrate its use in formal verification, systems and control theory, and robotics. We argue that CP is specifically useful due to its simplicity (easy to understand, use, and modify), generality (requires no assumptions on learned models and data distributions, i.e., is distribution-free), and efficiency (real-time capable and accurate). We pursue the following goals with this survey. First, we provide an accessible introduction to CP for non-experts who are interested in using CP to solve problems in autonomy. Second, we show how to use CP for the verification of LECs, e.g., for verifying input-output properties of neural networks. Third and fourth, we review recent articles that use CP for safe control design as well as offline and online verification of LEASs. We summarize their ideas in a unifying framework that can deal with the complexity of LEASs in a computationally efficient manner. In our exposition, we consider simple system specifications, e.g., robot navigation tasks, as well as complex specifications formulated in temporal logic formalisms. Throughout our survey, we compare to other statistical techniques (e.g., scenario optimization, PAC-Bayes theory, etc.) and how these techniques have been used in verification and control. Lastly, we point the reader to open problems and future research directions.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google