論文の概要: 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自動仕様作成
• 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%のリコールを実現しており、その出力は既存の検証ツールで直接消費することができる。

関連論文リスト

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  本稿では,LTL(Linear Temporal Logic)式を非構造的要求から直接生成することにより,現代市販のLarge Language Models (LLMs) がこのギャップを埋めることができるかどうかを評価する。 本研究は, 構造的に異なる15の異種ベンチマークを用いて, 数発のプロンプト戦略を用いて, 近代LLMの6点について検討した。 その結果,現在の汎用LLMはタスク固有の微調整を伴わずに非構造化NLto-LTLタスクにおいて実質的に有意な性能を達成できることが示唆された。
  論文  参考訳（メタデータ） (2026-08-06T17:13:07Z)
• NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic [0.0]
  本稿では,学習翻訳と形式的検証を一体化したニューロシンボリックアーキテクチャであるNeuroNL2LTLを提案する。 航空宇宙、ロボティクス、自動運転車、さらに10のドメインにまたがる20万以上の要件に対して、NeuroNL2LTLは基準仕様と28%のセマンティックな等価性を達成している。
  論文  参考訳（メタデータ） (2026-05-20T03:31:51Z)
• ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
  textscReasonSTLは、自然言語からSTL生成にローカルのオープンソース言語モデルを適用するツール拡張フレームワークである。 textscReasonSTLは、翻訳プロセスを明示的な推論、決定論的ツール呼び出し、構造化された公式構成に分解する。 実験により、textscReasonSTLでトレーニングされた4Bモデルは、自動測定と人的評価の両方で最先端のパフォーマンスを達成することが示された。
  論文  参考訳（メタデータ） (2026-05-07T16:07:30Z)
• 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)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  我々は,SimulMTタスクに大規模言語モデルを適用する可能性を検討する。 MUST-Cデータセットと異なる9言語でtextttLlama2-7b-chatモデルを用いて実験を行った。 その結果,LLM は BLEU と LAAL の指標で専用MT モデルよりも優れていた。
  論文  参考訳（メタデータ） (2023-09-13T04:06:47Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。