Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems

要約

この論文では、堅牢で回復力のある学習対応システムの原則に基づいた設計と実装のための、形式的な検証に基づくアプローチを紹介します。
私たちは、複雑なシステムの現在の状態 (位置、速度、方向など) を決定するためにロボット工学アプリケーションで広く使用されている学習可能状態推定システム (LE-SES) に焦点を当てています。
LE-SES はネットワーク化されたシステムであり、状態推定用のベイズ フィルターや感覚入力を処理するニューラル ネットワークなどの一連の接続されたコンポーネントで構成されています。
私たちは、指定された特性に対するシステムモデルの充足性を決定する形式的検証の観点から LE-SES を研究します。
LE-SES について、堅牢性と回復力という 2 つの重要な特性を調査し、それらの正式な定義を提供します。
形式的な検証を可能にするために、LE-SES を、論文では {PO}^2-LTS と名付けられた新しいクラスのラベル付き遷移システムに還元し、そのプロパティを制約付き最適化目標として形式的に表現します。
検証問題が NP 完全であることを証明します。
{PO}^2-LTS と最適化目標に基づいて、LE-SES の特性の充足性をチェックするための実用的な検証アルゴリズムが開発されています。
主要なケーススタディとして、単一のカルマン フィルター (KF) (ベイズ フィルターの特殊なケース) を使用して地上車両の位置を特定し、追跡する現実世界の動的追跡システムについて調べます。
畳み込みニューラル ネットワークに基づくその認識システムは、高解像度の Wide Area Motion Imagery (WAMI) データ ストリームを処理します。
実験結果は、私たちのアルゴリズムが WAMI 追跡システムの特性を検証できるだけでなく、代表的な例も提供できることを示しています。後者は、ランタイム モニターまたはジョイント KF が必要な場合に強化された LE-SES 設計を採用するきっかけとなりました。
実験結果により、強化された設計の堅牢性の向上が確認されました。

要約(オリジナル)

This paper presents a formal verification guided approach for a principled design and implementation of robust and resilient learning-enabled systems. We focus on learning-enabled state estimation systems (LE-SESs), which have been widely used in robotics applications to determine the current state (e.g., location, speed, direction, etc.) of a complex system. The LE-SESs are networked systems, composed of a set of connected components including: Bayes filters for state estimation, and neural networks for processing sensory input. We study LE-SESs from the perspective of formal verification, which determines the satisfiabilty of a system model against the specified properties. Over LE-SESs, we investigate two key properties — robustness and resilience — and provide their formal definitions. To enable formal verification, we reduce the LE-SESs to a novel class of labelled transition systems, named {PO}^2-LTS in the paper, and formally express the properties as constrained optimisation objectives. We prove that the verification problems are NP-complete. Based on {PO}^2-LTS and the optimisation objectives, practical verification algorithms are developed to check the satisfiability of the properties on the LE-SESs. As a major case study, we interrogate a real-world dynamic tracking system which uses a single Kalman Filter (KF) — a special case of Bayes filter — to localise and track a ground vehicle. Its perception system, based on convolutional neural networks, processes a high-resolution Wide Area Motion Imagery (WAMI) data stream. Experimental results show that our algorithms can not only verify the properties of the WAMI tracking system but also provide representative examples, the latter of which inspired us to take an enhanced LE-SESs design where runtime monitors or joint-KFs are required. Experimental results confirm the improvement in the robustness of the enhanced design.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google