論文の概要: Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems
- arxiv url: http://arxiv.org/abs/2010.08311v4
- Date: Fri, 29 Mar 2024 14:41:08 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-01 21:15:55.117646
- Title: Formal Verification of Robustness and Resilience of Learning-Enabled State Estimation Systems
- Title（参考訳）: 学習可能状態推定システムのロバスト性とレジリエンスの形式的検証
- Authors: Wei Huang, Yifan Zhou, Gaojie Jin, Youcheng Sun, Jie Meng, Fan Zhang, Xiaowei Huang,
- Abstract要約: 我々は,ロボット工学の分野で広く利用されている学習可能な状態推定システム(LE-SESs)に注目した。
LE-SESを形式的検証の観点から検討し,システムモデルの満足度を決定する。
- 参考スコア（独自算出の注目度）: 20.491263196235376
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,ロバストでレジリエントな学習システムの設計と実装のための形式的検証指導手法を提案する。
我々は,ロボット工学の分野で広く用いられている,学習可能な状態推定システム(LE-SES)に注目し,複雑なシステムの現在の状態(例えば,位置,速度,方向など)を決定する。
LE-SESはネットワーク化されたシステムであり、状態推定のためのベイズフィルタ、知覚入力を処理するニューラルネットワークを含む一連の接続コンポーネントで構成されている。
LE-SESを形式的検証の観点から検討し,その特性に対するシステムモデルの満足度を決定する。
LE-SES上では、ロバスト性とレジリエンスという2つの重要な特性を調査し、それらの公式な定義を提供する。
本論文では, LE-SESをラベル付き遷移系の新しいクラスである {PO}^2-LTS に還元し, その特性を制約された最適化目的として正式に表現する。
検証問題はNP完全であることを証明する。
LE-SESの特性の満足度を確認するために, {PO}^2-LTSと最適化目標に基づいて, 実用的検証アルゴリズムを開発した。
主要なケーススタディとして,1つのカルマンフィルタ(KF)(ベイズフィルタの特殊なケース)を使って地上車両のローカライズと追跡を行う,現実世界の動的トラッキングシステムを疑問視する。
畳み込みニューラルネットワークに基づく認識システムは、WAMI(Wide Area Motion Imagery)データストリームを高解像度で処理する。
実験の結果,我々のアルゴリズムはWAMトラッキングシステムの特性を検証できるだけでなく,代表的な例も提示できることがわかった。
実験により, 改良された設計のロバスト性の向上が確認された。
関連論文リスト
- Entropy-Regularized Token-Level Policy Optimization for Language Agent Reinforcement [67.1393112206885]
大規模言語モデル(LLM)は、対話的な意思決定タスクにおいてインテリジェントなエージェントとして期待されている。
本稿では,トークンレベルでのLLMの最適化に適したエントロピー拡張RL法である,エントロピー正規化トークンレベル最適化(ETPO)を導入する。
我々は,データサイエンスコード生成を多段階対話型タスクのシリーズとしてモデル化したシミュレーション環境におけるETPOの有効性を評価する。
論文 参考訳（メタデータ） (2024-02-09T07:45:26Z) - RLEEGNet: Integrating Brain-Computer Interfaces with Adaptive AI for
Intuitive Responsiveness and High-Accuracy Motor Imagery Classification [0.0]
本稿では,Deep Q-Networks (DQN) を用いた強化学習を分類タスクに活用するフレームワークを提案する。
本稿では,OVR(One-Versus-The-Rest)方式で,マルチクラス運動画像(MI)分類のための前処理手法を提案する。
DQNと1D-CNN-LSTMアーキテクチャの統合は意思決定プロセスをリアルタイムで最適化する。
論文 参考訳（メタデータ） (2024-02-09T02:03:13Z) - Investigating Robustness in Cyber-Physical Systems: Specification-Centric Analysis in the face of System Deviations [8.8690305802668]
サイバー物理システム(CPS)の重要属性は堅牢性であり、安全に運用する能力を示している。
本稿では,特定のシステム要件を満たす上でのコントローラの有効性を特徴付ける,仕様に基づく新しいロバスト性を提案する。
本稿では, 微妙な堅牢性違反を識別するための2層シミュレーションに基づく解析フレームワークを提案する。
論文 参考訳（メタデータ） (2023-11-13T16:44:43Z) - Physics Inspired Hybrid Attention for SAR Target Recognition [61.01086031364307]
本稿では,物理にヒントを得たハイブリットアテンション(PIHA)機構と,この問題に対処するためのOFA評価プロトコルを提案する。
PIHAは、物理的情報の高レベルなセマンティクスを活用して、ターゲットの局所的なセマンティクスを認識した特徴群を活性化し、誘導する。
提案手法は,ASCパラメータが同じ12のテストシナリオにおいて,他の最先端手法よりも優れている。
論文 参考訳（メタデータ） (2023-09-27T14:39:41Z) - SysNoise: Exploring and Benchmarking Training-Deployment System
Inconsistency [55.49469003537601]
我々はSysNoiseを紹介した。SysNoiseは、頻繁に発生するが、ディープラーニングのトレーニング-デプロイサイクルでしばしば見過ごされるノイズである。
我々は,SysNoiseが20以上のモデル,画像分類,オブジェクト検出,インスタンスセグメンテーション,自然言語処理タスクに与える影響を測定する。
実験の結果、SysNoiseはさまざまなタスクにわたるモデルロバスト性に一定の影響をもたらし、データ強化や逆行訓練のような一般的な緩和効果は、それに対する限られた影響を示します。
論文 参考訳（メタデータ） (2023-07-01T09:22:54Z) - Age of Semantics in Cooperative Communications: To Expedite Simulation
Towards Real via Offline Reinforcement Learning [53.18060442931179]
協調リレー通信システムにおける状態更新のセマンティックス更新度を測定するための意味学年代(AoS)を提案する。
オンライン・ディープ・アクター・クリティック(DAC)学習手法を,政治時間差学習の枠組みに基づいて提案する。
そこで我々は,以前に収集したデータセットから最適制御ポリシーを推定する,新しいオフラインDAC方式を提案する。
論文 参考訳（メタデータ） (2022-09-19T11:55:28Z) - Formalizing and Evaluating Requirements of Perception Systems for
Automated Vehicles using Spatio-Temporal Perception Logic [25.070876549371693]
本研究では,空間的および時間的演算子を用いた知覚データに対する推論を可能にするロジックを提案する。
STPLの大きな利点の1つは、知覚システムの機能性能の基本的な正当性チェックを容易にすることである。
論文 参考訳（メタデータ） (2022-06-29T02:36:53Z) - Fingerprint recognition with embedded presentation attacks detection:
are we ready? [6.0168714922994075]
セキュリティアプリケーションのための指紋認証システムの拡散は,ソフトウェアベースのプレゼンテーション攻撃アルゴリズム(PAD)をそのようなシステムに組み込むことを急ぐ。
現在の研究では、指紋認証システムに組み込む際の有効性についてはあまり言及されていない。
本稿では,PADと検証段階を逐次実施する場合の2つの個別システムの受信者動作特性(ROC)の関係を確率論的にモデル化した性能シミュレータを提案する。
論文 参考訳（メタデータ） (2021-10-20T13:53:16Z) - An Explainable Machine Learning-based Network Intrusion Detection System
for Enabling Generalisability in Securing IoT Networks [0.0]
機械学習(ML)ベースのネットワーク侵入検知システムは、組織のセキュリティ姿勢を高める多くの利点をもたらす。
多くのシステムは研究コミュニティで設計・開発されており、特定のデータセットを用いて評価すると、しばしば完璧な検出率を達成する。
本稿では,異なるネットワーク環境と攻撃タイプに設定した共通機能の汎用性を評価することにより,ギャップを狭める。
論文 参考訳（メタデータ） (2021-04-15T00:44:45Z) - A Novel Anomaly Detection Algorithm for Hybrid Production Systems based
on Deep Learning and Timed Automata [73.38551379469533]
DAD:DeepAnomalyDetectionは,ハイブリッド生産システムにおける自動モデル学習と異常検出のための新しいアプローチである。
深層学習とタイムドオートマトンを組み合わせて、観察から行動モデルを作成する。
このアルゴリズムは実システムからの2つのデータを含む少数のデータセットに適用され、有望な結果を示している。
論文 参考訳（メタデータ） (2020-10-29T08:27:43Z) - Deep Speaker Embeddings for Far-Field Speaker Recognition on Short
Utterances [53.063441357826484]
深層話者埋め込みに基づく話者認識システムは,制御条件下での大幅な性能向上を実現している。
制御されていない雑音環境下での短い発話に対する話者検証は、最も困難で要求の高いタスクの1つである。
本稿では,a)環境騒音の有無による遠距離話者検証システムの品質向上,b)短時間発話におけるシステム品質劣化の低減という2つの目標を達成するためのアプローチを提案する。
論文 参考訳（メタデータ） (2020-02-14T13:34:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。