論文の概要: Verification of Autonomous Neural Car Control with KeYmaera X
- arxiv url: http://arxiv.org/abs/2504.03272v1
- Date: Fri, 04 Apr 2025 08:43:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-04-07 14:48:49.894271
- Title: Verification of Autonomous Neural Car Control with KeYmaera X
- Title（参考訳）: KeYmaera Xを用いた自律型ニューラルカー制御の検証
- Authors: Enguerrand Prebet, Samuel Teuber, André Platzer,
- Abstract要約: 本稿では、微分力学(dL)におけるABZ'25ケーススタディのための形式モデルと形式的安全性証明について述べる。
ケーススタディでは、近隣の車との衝突を避けるために高速道路を走行する自動運転車について検討している。
KeYmaera X の dL 実装を用いて、無限時間地平線上での衝突の欠如を証明し、安全が旅行距離とは無関係に維持されていることを確かめる。
- 参考スコア（独自算出の注目度）: 2.726684740197893
- License:
- Abstract: This article presents a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a highway avoiding collisions with neighbouring cars. Using KeYmaera X's dL implementation, we prove absence of collision on an infinite time horizon which ensures that safety is preserved independently of trip length. The safety guarantees hold for time-varying reaction time and brake force. Our dL model considers the single lane scenario with cars ahead or behind. We demonstrate that dL with its tools is a rigorous foundation for runtime monitoring, shielding, and neural network verification. Doing so sheds light on inconsistencies between the provided specification and simulation environment highway-env of the ABZ'25 study. We attempt to fix these inconsistencies and uncover numerous counterexamples which also indicate issues in the provided reinforcement learning environment.
- Abstract（参考訳）: 本稿では、微分力学(dL)におけるABZ'25ケーススタディのための形式モデルと形式的安全性証明について述べる。
ケーススタディでは、近隣の車との衝突を避けるために高速道路を走行する自動運転車について検討している。
KeYmaera X の dL 実装を用いて、無限時間地平線上での衝突の欠如を証明し、安全が旅行距離とは無関係に維持されていることを確かめる。
安全保証は、時間変化の反応時間とブレーキ力を保持する。
当社のdLモデルは、車両を前後に並べた単一レーンのシナリオを考慮に入れています。
私たちは、dLとそのツールがランタイム監視、シールド、ニューラルネットワーク検証のための厳格な基盤であることを実証しています。
ABZ'25研究の仕様とシミュレーション環境との整合性に光を当てる。
我々はこれらの不整合を修復し、提供された強化学習環境における問題を示す多数の反例を明らかにする。
関連論文リスト
- Foundation Models for Rapid Autonomy Validation [4.417336418010182]
重要な課題は、自動運転車が遭遇するあらゆる種類の運転シナリオでテストする必要があることだ。
本研究では,運転シナリオを再構築するための行動基礎モデル,特にマスク付きオートエンコーダ(MAE)の使用を提案する。
論文 参考訳（メタデータ） (2024-10-22T15:32:43Z) - A novel framework for adaptive stress testing of autonomous vehicles in
highways [3.2112502548606825]
高速道路交通のシナリオにおいて,安全上の懸念を生じさせるようなコーナーケースを探索する新しい枠組みを提案する。
衝突確率推定に基づいて衝突シナリオを識別する際のASTを導出するDRLの新しい報奨関数を開発した。
提案するフレームワークは,より現実的なトラフィックシナリオの作成を可能にする,新たな駆動モデルとさらに統合されている。
論文 参考訳（メタデータ） (2024-02-19T04:02:40Z) - DARTH: Holistic Test-time Adaptation for Multiple Object Tracking [87.72019733473562]
複数物体追跡(MOT)は、自律運転における知覚システムの基本的構成要素である。
運転システムの安全性の追求にもかかわらず、テスト時間条件における領域シフトに対するMOT適応問題に対する解決策は提案されていない。
我々はMOTの総合的なテスト時間適応フレームワークであるDARTHを紹介する。
論文 参考訳（メタデータ） (2023-10-03T10:10:42Z) - Slow Down, Move Over: A Case Study in Formal Verification, Refinement,
and Testing of the Responsibility-Sensitive Safety Model for Self-Driving
Cars [0.0]
我々は、自動運転車の責任感性安全モデル(RSS)を定式化する。
我々は、ハイブリッドシステム定理証明器KeYmaera Xを用いて、RSSを非決定論的制御選択と連続運動モデルを備えたハイブリッドシステムとして定式化する。
結果のPythonコードは、シミュレーションにおいてRSSのモーションモデルに従って車の振る舞いをテストすることができる。
論文 参考訳（メタデータ） (2023-05-15T17:18:36Z) - Unsupervised Driving Event Discovery Based on Vehicle CAN-data [62.997667081978825]
本研究は,車両CANデータのクラスタリングとセグメンテーションを同時に行うことで,一般的な運転イベントを教師なしで識別する手法である。
我々は、実際のTesla Model 3車載CANデータと、異なる運転イベントをアノテートした2時間の運転セッションのデータセットを用いて、アプローチを評価した。
論文 参考訳（メタデータ） (2023-01-12T13:10:47Z) - Differentiable Control Barrier Functions for Vision-based End-to-End
Autonomous Driving [100.57791628642624]
本稿では,視覚に基づくエンドツーエンド自動運転のための安全保証学習フレームワークを提案する。
我々は、勾配降下によりエンドツーエンドに訓練された微分制御バリア関数(dCBF)を備えた学習システムを設計する。
論文 参考訳（メタデータ） (2022-03-04T16:14:33Z) - Causal Imitative Model for Autonomous Driving [85.78593682732836]
慣性および衝突問題に対処するための因果Imitative Model (CIM)を提案する。
CIMは因果モデルを明確に発見し、ポリシーのトレーニングに利用します。
実験の結果,本手法は慣性および衝突速度において従来の手法よりも優れていたことがわかった。
論文 参考訳（メタデータ） (2021-12-07T18:59:15Z) - A Reinforcement Learning Benchmark for Autonomous Driving in
Intersection Scenarios [11.365750371241154]
本稿では,RL-CISと呼ばれる複雑な交差点シナリオにおける自律走行エージェントの訓練と試験のためのベンチマークを提案する。
テストベンチマークとベースラインは、交差点シナリオにおける自動運転のためのRLの研究のための公平で包括的なトレーニングおよびテストプラットフォームを提供する。
論文 参考訳（メタデータ） (2021-09-22T07:38:23Z) - Safety-aware Motion Prediction with Unseen Vehicles for Autonomous
Driving [104.32241082170044]
本研究では,無人運転用無人車を用いた新しい作業,安全を意識した動作予測手法について検討する。
既存の車両の軌道予測タスクとは異なり、占有率マップの予測が目的である。
私たちのアプローチは、ほとんどの場合、目に見えない車両の存在を予測できる最初の方法です。
論文 参考訳（メタデータ） (2021-09-03T13:33:33Z) - An NCAP-like Safety Indicator for Self-Driving Cars [2.741266294612776]
本稿では,自動運転車の安全性を評価するメカニズムを提案する。
車両が敵と衝突することを避けるシナリオにおいて、車両の安全性を評価する。
セーフカミカゼ距離(Safe-Kamikaze Distance)と呼ばれる安全対策は、安全な敵の軌道と安全な軌道に近いカミカゼ軌道との平均的な類似性を計算する。
論文 参考訳（メタデータ） (2021-04-02T02:39:53Z) - Detecting 32 Pedestrian Attributes for Autonomous Vehicles [103.87351701138554]
本稿では、歩行者を共同で検出し、32の歩行者属性を認識するという課題に対処する。
本稿では,複合フィールドフレームワークを用いたマルチタスク学習(MTL)モデルを提案する。
競合検出と属性認識の結果と,より安定したMTLトレーニングを示す。
論文 参考訳（メタデータ） (2020-12-04T15:10:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。