論文の概要: Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
- arxiv url: http://arxiv.org/abs/2512.17334v1
- Date: Fri, 19 Dec 2025 08:25:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-22 19:25:54.305772
- Title: Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
- Title（参考訳）: 自然言語と形式仕様のブリッジ-LLMを用いた階層的意味論分解によるソフトウェア要求のLTLへの自動翻訳
- Authors: Zhi Ma, Cheng Wen, Zhexin Su, Xiao Liang, Cong Tian, Shengchao Qin, Mengfei Yang,
- Abstract要約: Req2LTLは、NLとLinear Temporal Logicをブリッジするモジュラーフレームワークである。
実世界の航空要求に対して88.4%のセマンティック精度と100%の構文的正確性を達成する。
- 参考スコア（独自算出の注目度）: 10.958536923155101
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automating the translation of natural language (NL) software requirements into formal specifications remains a critical challenge in scaling formal verification practices to industrial settings, particularly in safety-critical domains. Existing approaches, both rule-based and learning-based, face significant limitations. While large language models (LLMs) like GPT-4o demonstrate proficiency in semantic extraction, they still encounter difficulties in addressing the complexity, ambiguity, and logical depth of real-world industrial requirements. In this paper, we propose Req2LTL, a modular framework that bridges NL and Linear Temporal Logic (LTL) through a hierarchical intermediate representation called OnionL. Req2LTL leverages LLMs for semantic decomposition and combines them with deterministic rule-based synthesis to ensure both syntactic validity and semantic fidelity. Our comprehensive evaluation demonstrates that Req2LTL achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements, significantly outperforming existing methods.
- Abstract（参考訳）: 自然言語(NL)ソフトウェア要件を形式仕様に自動変換することは、特に安全クリティカルな領域において、産業環境での形式的検証プラクティスをスケールする上で、依然として重要な課題である。
既存のアプローチでは、ルールベースと学習ベースの両方が、大きな制限に直面している。
GPT-4oのような大きな言語モデル(LLM)は意味抽出の習熟度を示すが、実世界の産業要件の複雑さ、曖昧さ、論理的な深さに対処する上ではまだ困難である。
本論文では,NL と線形時間論理(LTL)を階層的な中間表現である OnionL を通じて橋渡しするモジュール型フレームワーク Req2LTL を提案する。
Req2LTLはLLMを意味分解に利用し、決定論的規則に基づく合成と組み合わせて、構文的妥当性と意味的忠実性の両方を保証する。
我々の総合評価は、Req2LTLが実世界の航空要求に対して88.4%のセマンティックな精度と100%の構文的正当性を達成し、既存の手法を著しく上回っていることを示している。
関連論文リスト
- Connecting the Dots: Training-Free Visual Grounding via Agentic Reasoning [63.109585527799005]
GroundingAgentは、タスク固有の微調整なしで動作するビジュアルグラウンドティングフレームワークである。
広く使用されているベンチマークでは、平均ゼロショットグラウンドの精度は65.1%である。
また、強い解釈可能性を提供し、各推論ステップを透過的に照らす。
論文 参考訳（メタデータ） (2025-11-24T03:11:08Z) - Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
非公式な文を形式論理に翻訳するプロセスであるオートフォーマル化は、強力な大規模言語モデルの出現により、新たな関心を集めている。
本稿では,LLMをベースとした簡易なオートフォーマライザを用いて,LLM生成した出力を少数の自然言語要求に対して検証する。
この結果から, LLM出力の完全性と論理的整合性を確保する上で, 自己形式化が有意な可能性を示唆した。
論文 参考訳（メタデータ） (2025-11-14T19:45:17Z) - Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
本稿では,API2Depという新しいステップバイステップコード生成フレームワークを提案する。
まず、サービス指向アーキテクチャに適した拡張Unified Modeling Language (UML) APIダイアグラムを紹介します。
次に、データフローの重要な役割を認識し、専用のデータ依存推論タスクを導入する。
論文 参考訳（メタデータ） (2025-08-05T12:28:23Z) - From Legal Texts to Defeasible Deontic Logic via LLMs: A Study in Automated Semantic Analysis [1.5749416770494706]
本稿では,大言語モデル(LLM)を用いた法文の自動意味解析への新しいアプローチを提案する。
本稿では、複雑な規範言語を原子スニペットに分割し、デオン規則を抽出し、それらを構文的・意味的コヒーレンスとして評価する構造化パイプラインを提案する。
論文 参考訳（メタデータ） (2025-06-10T15:25:19Z) - $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
$texttSEM-CTRL$は、LLMデコーダに直接、リッチなコンテキスト依存制約とタスクおよびインスタンス固有のセマンティクスを強制する統一的なアプローチである。
texttSEM-CTRL$は、小さな訓練済みのLLMがより大きな変種や最先端の推論モデルよりも効率的に性能を向上することを可能にする。
論文 参考訳（メタデータ） (2025-03-03T18:33:46Z) - Elevating Legal LLM Responses: Harnessing Trainable Logical Structures and Semantic Knowledge with Legal Reasoning [19.477062052536887]
意味と論理的コヒーレンスを橋渡しする教師ありフレームワークである論理・意味統合モデル(LSIM)を提案する。
LSIMは3つの要素から構成される: 強化学習は各質問に対して構造化されたファクトルールチェーンを予測し、訓練可能なDeep Structured Semantic Model(DSSM)は最も関連性の高い質問を検索し、回答内学習は最終回答を生成する。
LSIMが従来の手法に比べて精度と信頼性を著しく向上させるような,自動測定と人的評価デーモンレートによる実世界の法的データセットのQA検証実験を行った。
論文 参考訳（メタデータ） (2025-02-11T19:33:07Z) - Large Language Models are Interpretable Learners [53.56735770834617]
本稿では,Large Language Models(LLM)とシンボルプログラムの組み合わせによって,表現性と解釈可能性のギャップを埋めることができることを示す。
自然言語プロンプトを持つ事前訓練されたLLMは、生の入力を自然言語の概念に変換することができる解釈可能な膨大なモジュールセットを提供する。
LSPが学んだ知識は自然言語の記述と記号規則の組み合わせであり、人間(解釈可能)や他のLLMに容易に転送できる。
論文 参考訳（メタデータ） (2024-06-25T02:18:15Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。