論文の概要: Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
- arxiv url: http://arxiv.org/abs/2411.14374v1
- Date: Thu, 21 Nov 2024 18:09:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-11-22 15:19:54.215008
- Title: Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
- Title（参考訳）: 形式モデル, 安全シールド, 認証制御を用いたAIベーストレインシステムの検証
- Authors: Jan Gruteser, Jan Roßbach, Fabian Vu, Michael Leuschel,
- Abstract要約: KI-LOKプロジェクトは、AIコンポーネントを自律列車に安全に統合するための新しい方法を模索している。
我々は,(1)B法を用いた形式解析によるステアリングシステムの安全性確保,(2)ランタイム証明書チェッカーによる認識システムの信頼性向上という2層的なアプローチを追求する。
この作業は、実際のAI出力と実際の証明書チェッカーによって制御されるフォーマルモデル上でシミュレーションを実行するデモレータ内の両方の戦略をリンクする。
- 参考スコア（独自算出の注目度）: 0.5249805590164903
- License:
- Abstract: The certification of autonomous systems is an important concern in science and industry. The KI-LOK project explores new methods for certifying and safely integrating AI components into autonomous trains. We pursued a two-layered approach: (1) ensuring the safety of the steering system by formal analysis using the B method, and (2) improving the reliability of the perception system with a runtime certificate checker. This work links both strategies within a demonstrator that runs simulations on the formal model, controlled by the real AI output and the real certificate checker. The demonstrator is integrated into the validation tool ProB. This enables runtime monitoring, runtime verification, and statistical validation of formal safety properties using a formal B model. Consequently, one can detect and analyse potential vulnerabilities and weaknesses of the AI and the certificate checker. We apply these techniques to a signal detection case study and present our findings.
- Abstract（参考訳）: 自律システムの認証は、科学と産業において重要な関心事である。
KI-LOKプロジェクトは、AIコンポーネントを自律列車に安全に統合するための新しい方法を模索している。
筆者らは,(1)B法を用いた形式解析によるステアリングシステムの安全性確保,(2)ランタイム証明書チェッカーによる認識システムの信頼性向上という2段階のアプローチを追求した。
この作業は、実際のAI出力と実際の証明書チェッカーによって制御されるフォーマルモデル上でシミュレーションを実行するデモレータ内の両方の戦略をリンクする。
デモンストレータはバリデーションツールProBに統合される。
これにより、フォーマルなBモデルを使用して、ランタイム監視、ランタイム検証、フォーマルな安全特性の統計的検証が可能になる。
その結果、AIと証明書チェッカーの潜在的な脆弱性と弱点を検出し、分析することができる。
これらの手法を信号検出ケーススタディに適用し,本研究の成果を報告する。
関連論文リスト
- Computational Safety for Generative AI: A Signal Processing Perspective [65.268245109828]
計算安全性は、GenAIにおける安全性の定量的評価、定式化、研究を可能にする数学的枠組みである。
ジェイルブレイクによる悪意のあるプロンプトを検出するために, 感度解析と損失景観解析がいかに有効かを示す。
我々は、AIの安全性における信号処理の鍵となる研究課題、機会、そして重要な役割について論じる。
論文 参考訳（メタデータ） (2025-02-18T02:26:50Z) - Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates [2.0611129932396164]
離散時間システムのためのNLBベースの証明書をトレーニングし、検証するための新しい手法を提案する。
具体的には,高度に複雑なシステムの検証を簡略化する証明書合成手法を提案する。
DRL制御宇宙船の安全性と生存性を保証するためのケーススタディにより,本手法の利点を実証する。
論文 参考訳（メタデータ） (2024-05-22T23:06:34Z) - Certified Control for Train Sign Classification [0.0]
KI-LOK研究プロジェクトは、このようなAIベースのシステムを証明する新しい方法の開発に関与している。
本稿では,交通標識の偽陽性検出を防止するランタイムモニタの認証制御アーキテクチャの有用性について検討する。
論文 参考訳（メタデータ） (2023-11-16T11:02:10Z) - Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
機械学習(ML)をサイバー物理システム(CPS)に統合することは大きな利益をもたらす。
既存の検証と検証技術は、しばしばこれらの新しいパラダイムには不十分である。
本稿では, 基礎確率テストからより厳密なアプローチへ移行し, 正式な保証を実現するためのロードマップを提案する。
論文 参考訳（メタデータ） (2023-11-13T14:56:14Z) - Simulation-based Safety Assurance for an AVP System incorporating
Learning-Enabled Components [0.6526824510982802]
テスト、検証、検証 AD/ADASセーフティクリティカルなアプリケーションが大きな課題のひとつとして残っています。
安全クリティカルな学習可能システムの検証と検証を目的としたシミュレーションベースの開発プラットフォームについて説明する。
論文 参考訳（メタデータ） (2023-09-28T09:00:31Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
我々はランダムフォレストとリカレントニューラルネットワークアーキテクチャに基づく2つの軽量ドライバ認証システムを開発した。
我々は,SMARTCANとGANCANという2つの新しいエスケープアタックを開発することで,これらのシステムに対する攻撃を最初に提案する。
コントリビューションを通じて、これらのシステムを安全に採用する実践者を支援し、車の盗難を軽減し、ドライバーのセキュリティを高める。
論文 参考訳（メタデータ） (2023-06-09T14:33:26Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z) - Evaluating the Safety of Deep Reinforcement Learning Models using
Semi-Formal Verification [81.32981236437395]
本稿では,区間分析に基づく半形式的意思決定手法を提案する。
本手法は, 標準ベンチマークに比較して, 形式検証に対して比較結果を得る。
提案手法は, 意思決定モデルにおける安全性特性を効果的に評価することを可能にする。
論文 参考訳（メタデータ） (2020-10-19T11:18:06Z) - Formal Verification of End-to-End Learning in Cyber-Physical Systems:
Progress and Challenges [7.955313479061443]
コンピュータチェックによる正式な正当性を構築することで、自律システムの安全性を確保することができるかもしれない。
本稿では,既存の形式的検証手法に基づく3つの仮定について述べる。
形式的検証による証拠の強度向上に向けた予備的な研究を要約する。
論文 参考訳（メタデータ） (2020-06-15T16:50:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。