論文の概要: VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains
- arxiv url: http://arxiv.org/abs/2511.01417v1
- Date: Mon, 03 Nov 2025 10:11:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-05 16:37:27.217164
- Title: VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains
- Title（参考訳）: VeriODD: YAMLからSMT-LIBへ -- 運用設計ドメインの検証を自動化する
- Authors: Bassel Rafie, Christian Schindler, Andreas Rausch,
- Abstract要約: YAMLベースのODD/COD仕様を人間可読な命題論理に変換するツールであるVeriODDを提案する。
グラフィカルユーザインタフェースは、仕様の編集、生成された公式の検査、シングルクリックによる検証をサポートする。
- 参考スコア（独自算出の注目度）: 2.6126272668390373
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Operational Design Domains (ODDs) define the conditions under which an Automated Driving System (ADS) is allowed to operate, while Current Operational Domains (CODs) capture the actual runtime situation. Ensuring that a COD instance lies within the ODD is a crucial step in safety assurance. Today, ODD and COD specifications are frequently expressed in YAML to remain accessible for stakeholders, but such descriptions are not directly suitable for solver-based verification. Manual translation into formal languages such as SMT-LIB is slow and error-prone. We present VeriODD, a tool that automates this translation. VeriODD uses ANTLR-based compiler technology to transform YAML-based ODD/COD specifications into both human-readable propositional logic, for lightweight review on a simple basis, and solver-ready SMT-LIB. The tool integrates with SMT solvers such as Z3 to provide automated consistency checks of ODD specifications and verification of COD conformance. A graphical user interface supports editing specifications, inspecting generated formulas, and performing verification with a single click. VeriODD thereby closes the gap between stakeholder-friendly ODD/COD notations and formal verification, enabling scalable and automated assurance of operational boundaries in autonomous driving. Video demonstration: https://youtu.be/odRacNoL_Pk Tool available at: https://github.com/BasselRafie/VeriODD
- Abstract（参考訳）: Operational Design Domains (ODD) は、ADS(Automated Driving System)が動作することを許可する条件を定義し、Current Operational Domains (COD) は実際の実行状況をキャプチャする。
CODインスタンスがODD内にあることを保証することは、安全保証の重要なステップである。
今日では、ODDとCODの仕様はYAMLでしばしば表現され、利害関係者にもアクセス可能であるが、そのような記述は解決者による検証には適していない。
SMT-LIBのような形式言語への手動翻訳は遅く、エラーを起こしやすい。
この翻訳を自動化するツールであるVeriODDを提案する。
VeriODDはANTLRベースのコンパイラ技術を用いてYAMLベースのODD/COD仕様を人間可読な命題論理に変換する。
このツールは、Z3などのSMTソルバと統合し、ODD仕様の自動一貫性チェックとCOD適合性検証を提供する。
グラフィカルユーザインタフェースは、仕様の編集、生成された公式の検査、シングルクリックによる検証をサポートする。
VeriODDは、利害関係者に優しいODD/COD表記と正式な検証のギャップを埋め、自動運転における運用境界のスケーラブルで自動化された保証を可能にする。
ビデオデモ: https://youtu.be/odRacNoL_Pk Tool available at: https://github.com/BasselRafie/VeriODD
関連論文リスト
- LLM-Assisted Tool for Joint Generation of Formulas and Functions in Rule-Based Verification of Map Transformations [7.263865226644131]
本稿では、論理式とそれに対応する実行可能な述語を計算FOLフレームワーク内で共同で生成するLLM支援パイプラインを提案する。
その結果,手作業による作業の正確さを保ちながら,手作業による作業の削減が示され,地図変換検証に対するスケーラブルで半自動的なヒューマン・イン・ザ・ループ・アプローチの実現可能性が確認された。
論文 参考訳（メタデータ） (2025-11-03T10:19:52Z) - AutoMT: A Multi-Agent LLM Framework for Automated Metamorphic Testing of Autonomous Driving Systems [14.084623367678084]
AutoMTは、ローカルトラフィックルールからメタモルフィックリレーショナル(MR)を抽出するフレームワークである。
視覚言語エージェントがシナリオを分析し、検索エージェントがRAGベースのデータベースから適切なMRを取得し、フォローアップケースを生成する。
実験の結果, AutoMT は, 最良ベースラインと比較して, フォローアップケース生成において最大5倍の多様性を達成できることがわかった。
論文 参考訳（メタデータ） (2025-10-22T10:11:05Z) - FABRIC: Framework for Agent-Based Realistic Intelligence Creation [3.940391073007047]
大規模言語モデル(LLM)はエージェントとしてますます多くデプロイされ、目標を分解し、ツールを実行し、動的環境で結果を検証することが期待されている。
本稿では,LLMのみを用いたエージェントデータの統一化フレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-20T18:20:22Z) - AutoEDA: Enabling EDA Flow Automation through Microservice-Based LLM Agents [15.41283323575065]
AutoEDAは、標準化されたスケーラブルな自然言語エクスペリエンスに特化したモデルコンテキストプロトコル(MCP)を通じて並列学習を活用する、EDA自動化のためのフレームワークである。
実験の結果、既存の手法と比較して、自動化の精度と効率が向上し、スクリプトの品質も向上した。
論文 参考訳（メタデータ） (2025-08-01T18:23:57Z) - SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
SOPBenchは、各サービス固有のSOPコードプログラムを実行可能な関数の有向グラフに変換する評価パイプラインである。
提案手法では,各サービス固有のSOPコードプログラムを実行可能関数の有向グラフに変換し,自然言語SOP記述に基づいてこれらの関数を呼び出しなければならない。
我々は18の先行モデルを評価し、上位モデルでさえタスクが困難であることを示す。
論文 参考訳（メタデータ） (2025-03-11T17:53:02Z) - Design and implementation of tools to build an ontology of Security Requirements for Internet of Medical Things [2.446672595462589]
インターネット・オブ・メディカル・モノ(IoMT)の世界では、メーカーやサードパーティは、法律と仕様の両方で示されるセキュリティ要件を認識しなければならない。
関連する法則と仕様(欧州の文脈)を表わすオントロジーは非常に有用である。
検討された仕様文書の量とサイズが非常に多いため,自然文からオントロジーへの移行を簡単にするための方法論とツールが導入された。
論文 参考訳（メタデータ） (2025-01-06T15:04:45Z) - Get my drift? Catching LLM Task Drift with Activation Deltas [55.75645403965326]
タスクドリフトは攻撃者がデータを流出させたり、LLMの出力に影響を与えたりすることを可能にする。
そこで, 簡易線形分類器は, 分布外テストセット上で, ほぼ完全なLOC AUCでドリフトを検出することができることを示す。
このアプローチは、プロンプトインジェクション、ジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化する。
論文 参考訳（メタデータ） (2024-06-02T16:53:21Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。