論文の概要: Automated LTL Specification Generation from Industrial Aerospace Requirements
- arxiv url: http://arxiv.org/abs/2604.21715v1
- Date: Tue, 21 Apr 2026 01:20:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-24 14:40:06.591577
- Title: Automated LTL Specification Generation from Industrial Aerospace Requirements
- Title（参考訳）: 産業用航空要件からのTLL自動仕様作成
- Authors: Zhi Ma, Xiao Liang, Cheng Wen, Rui Chen, Bin Gu, Shengchao Qin, Cong Tian, Mengfei Yang,
- Abstract要約: 大規模言語モデル(LLM)を用いたプロパティ生成を自動化するフレームワークであるAeroReq2LTLを提案する。
実際の航空宇宙データセットでは、AeroReq2LTLは85%のリコールを生成でき、その出力は既存の検証ツールによって直接消費される。
- 参考スコア（独自算出の注目度）: 21.94000502237098
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In the development and verification of safety-critical aero-space software, Linear Temporal Logic (LTL) has been widely used to specify complex system properties derived from requirements. However, a significant gap remains in industrial practice: translating natural language (NL) requirements into formal LTL properties is a labor-intensive and error-prone process that requires rare expertise in both aerospace control engineering and formal methods. While recent NL-to-LTL tools (e.g., NL2SPEC, NL2TL, NL2LTL) are capable of automating parts of this process, they often fail on real requirement documents in industrial settings, due to complex domain terminology or implicit temporal and logical structure. To address these challenges, we present AeroReq2LTL, a framework that automates LTL property generation for aerospace requirements using large language models (LLMs), with two key industrial innovations: (i) a data dictionary that normalizes technical jargon into precise atomic propositions; and (ii) a template-based requirement language that makes temporal cues and logical relations explicit before translation. On a real aerospace dataset, AeroReq2LTL achieves 85% precision and 88% recall in LTL generation, and its outputs can be directly consumed by existing verification tools.
- Abstract（参考訳）: 安全クリティカルな航空宇宙ソフトウェアの開発と検証において、LTL(Linear Temporal Logic)は要求から派生した複雑なシステム特性の特定に広く用いられている。
自然言語(NL)の要件を形式的LTL特性に変換することは、航空宇宙制御工学と形式的手法の両方において稀な専門知識を必要とする労働集約的かつエラーを起こしやすいプロセスである。
最近のNL-to-LTLツール(例えば、NL2SPEC、NL2TL、NL2LTL)は、このプロセスの一部を自動化することができるが、複雑なドメイン用語や暗黙の時間的・論理的構造のために、産業環境では実際の要求文書では失敗することが多い。
これらの課題に対処するため,大型言語モデル(LLM)を用いたLTLプロパティの自動生成を行うフレームワークであるAeroReq2LTLを紹介した。
一 専門用語を正確な原子命題に正規化するデータ辞書
(ii)テンプレートベースの要件言語で、翻訳の前に時間的手がかりと論理的関係を明確にする。
実際の航空宇宙データセットでは、AeroReq2LTLはLTL生成において85%の精度と88%のリコールを実現しており、その出力は既存の検証ツールで直接消費することができる。
関連論文リスト
- Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions [61.479946958462754]
エージェントが単一のユニバーサルポリシーを学習する環境であるマルチタスク強化学習(RL)について検討する。
本稿では,新世代の意味翻訳を利用したタスク埋め込み手法を提案する。
論文 参考訳（メタデータ） (2026-02-06T14:46:27Z) - Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs [10.958536923155101]
Req2LTLは、NLとLinear Temporal Logicをブリッジするモジュラーフレームワークである。
実世界の航空要求に対して88.4%のセマンティック精度と100%の構文的正確性を達成する。
論文 参考訳（メタデータ） (2025-12-19T08:25:54Z) - Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning [7.574481956683386]
この研究は、新しいエンドツーエンド合成フレームワークであるProof2Siliconを提示する。
以前提案されたPreFACEフローを組み込んで、自然言語仕様から直接、正確性バイコンストラクションハードウェアを生成する。
論文 参考訳（メタデータ） (2025-09-07T23:04:15Z) - Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
本稿では,API2Depという新しいステップバイステップコード生成フレームワークを提案する。
まず、サービス指向アーキテクチャに適した拡張Unified Modeling Language (UML) APIダイアグラムを紹介します。
次に、データフローの重要な役割を認識し、専用のデータ依存推論タスクを導入する。
論文 参考訳（メタデータ） (2025-08-05T12:28:23Z) - QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation [51.393569044134445]
大きな言語モデル(LLM)は、強化学習と検証可能な報酬(RLVR)によって訓練され、明示的で自動化可能な検証を伴うタスクにおいてブレークスルーを達成した。
しかし、自然言語(NL)仕様からVerilogのようなハードウェア記述言語(HDL)を自動的に生成するRLVRの拡張には、3つの大きな課題がある。
本稿では,Verilog 生成 LLM をトレーニングするための RLVR フレームワークである CodeV-R1 を紹介する。
論文 参考訳（メタデータ） (2025-05-30T03:51:06Z) - Vision to Specification: Automating the Transition from Conceptual Features to Functional Requirements [10.85799957734291]
EasyFRアプローチでは、与えられた抽象機能に対してセマンティックロールラベリングシーケンスを推奨し、結合機能要件(FR)の生成において、事前学習言語モデル(PLM)をガイドする。
我々の結果は、将来のソフトウェアプロジェクトにおける要求仕様のプロセスを改善する可能性を秘めている、自動要求合成の領域における顕著な進歩を示している。
論文 参考訳（メタデータ） (2025-05-18T07:01:50Z) - Exploring Code Language Models for Automated HLS-based Hardware Generation: Benchmark, Infrastructure and Analysis [14.458529723566379]
LLM(Large Language Model)は、PythonやC++などのプログラミング言語に使用される。
本稿では,LLMを利用してHLS(High-Level Synthesis)ベースのハードウェア設計を行う。
論文 参考訳（メタデータ） (2025-02-19T17:53:59Z) - The Synergy of LLMs & RL Unlocks Offline Learning of Generalizable Language-Conditioned Policies with Low-fidelity Data [50.544186914115045]
TEDUOは、シンボリック環境におけるオフライン言語条件のポリシー学習のための、新しいトレーニングパイプラインである。
まず、オフラインデータセットをよりリッチなアノテーションで拡張する自動化ツールとして、次に、一般化可能な命令フォローエージェントとして使用します。
論文 参考訳（メタデータ） (2024-12-09T18:43:56Z) - Interactive Learning from Natural Language and Demonstrations using
Signal Temporal Logic [5.88797764615148]
自然言語(NL)は曖昧で、現実世界のタスクであり、それらの安全性要件はあいまいにコミュニケーションする必要がある。
Signal Temporal Logic (STL) は、ロボットタスクを記述するための汎用的で表現力があり、曖昧な形式言語として機能する形式論理である。
DIALOGUESTLは,(しばしば)曖昧なNL記述から正確かつ簡潔なSTL公式を学習するための対話的手法である。
論文 参考訳（メタデータ） (2022-07-01T19:08:43Z) - From English to Signal Temporal Logic [7.6398837478968025]
本稿では,サイバー物理システムのための公式な仕様言語であるSignal Temporal Logic (STL) に,自由英語文として与えられる非公式な要件を翻訳するためのツールおよびテクニックであるDeepSTLを提案する。
このような翻訳を考案する上での大きな課題は、公式な非公式な要件と公式な仕様の欠如である。
2番目のステップでは、最先端のトランスフォーマーベースのニューラル翻訳技術を用いて、英語からSTLへの正確な注意翻訳を訓練する。
論文 参考訳（メタデータ） (2021-09-21T16:13:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。