論文の概要: 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への自動翻訳
- 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%の構文的正当性を達成し、既存の手法を著しく上回っていることを示している。
関連論文リスト
- 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) - ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。
ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。
1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
論文 参考訳（メタデータ） (2026-07-01T09:58:59Z) - 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) - ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification [41.040507019193775]
Signal Temporal Logic (STL) は、サイバー物理システムのリアルタイム動作を特定するための形式言語である。
大規模言語モデル(LLM)を活用した最近の取り組みは目覚ましい性能を示しているが、いくつかの自然言語要求にはあいまいな情報や曖昧な情報が含まれている。
要求の明確化を通じてSTL変換を強化する対話型LLMエージェントフレームワークであるClarifySTLを提案する。
論文 参考訳（メタデータ） (2026-05-02T02:55:06Z) - Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
Orchidは、曖昧な要求で特別に設計された最初のコード生成ベンチマークです。
これは、語彙、構文、意味、曖昧さの4つの異なる種類の曖昧さをカバーする1,304の関数レベルタスクからなる。
この結果から,高度モデルにおいて最も顕著な負の効果が観察され,不明瞭さは全ての評価LCMの性能を常に低下させることが示された。
論文 参考訳（メタデータ） (2026-04-23T10:07:33Z) - Automated LTL Specification Generation from Industrial Aerospace Requirements [21.94000502237098]
大規模言語モデル(LLM)を用いたプロパティ生成を自動化するフレームワークであるAeroReq2LTLを提案する。
実際の航空宇宙データセットでは、AeroReq2LTLは85%のリコールを生成でき、その出力は既存の検証ツールによって直接消費される。
論文 参考訳（メタデータ） (2026-04-21T01:20:33Z) - Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
SOTA LLMが形式言語の構造的・階層的複雑性を把握できるかどうかは不明である。
ChomskyBench はchomsky Hierarchy のレンズを通して LLM を体系的に評価するためのベンチマークである。
ChomskyBenchは、各レベルで機能をテストするように設計された、言語認識と生成タスクの包括的なスイートで構成されている。
論文 参考訳（メタデータ） (2026-04-03T04:06:39Z) - Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions [61.479946958462754]
エージェントが単一のユニバーサルポリシーを学習する環境であるマルチタスク強化学習(RL)について検討する。
本稿では,新世代の意味翻訳を利用したタスク埋め込み手法を提案する。
論文 参考訳（メタデータ） (2026-02-06T14:46:27Z) - 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) - ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees [10.687644259002674]
我々は,未知のNLコマンドに対してユーザ定義の翻訳成功率を達成するための,ConformalNL2LTLと呼ばれる新しいNL-to-LTL変換手法を提案する。
提案手法は, LLM を用いた開語彙質問応答問題 (QA) の系列に対処することで, 論理式を反復的に構築する。
論文 参考訳（メタデータ） (2025-04-22T20:32:34Z) - $\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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。