論文の概要: Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models

• arxiv url: http://arxiv.org/abs/2608.06287v1
• Date: Thu, 06 Aug 2026 17:13:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-07 15:25:20.971668
• Title: Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models
• Title（参考訳）: 大規模言語モデルによる線形時間論理への非構造的要求の自動翻訳
• Abstract要約: 本稿では,LTL(Linear Temporal Logic)式を非構造的要求から直接生成することにより,現代市販のLarge Language Models (LLMs) がこのギャップを埋めることができるかどうかを評価する。 本研究は, 構造的に異なる15の異種ベンチマークを用いて, 数発のプロンプト戦略を用いて, 近代LLMの6点について検討した。 その結果,現在の汎用LLMはタスク固有の微調整を伴わずに非構造化NLto-LTLタスクにおいて実質的に有意な性能を達成できることが示唆された。
• 参考スコア（独自算出の注目度）: 46.28810845443601
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automatically translating unstructured natural language requirements into formal specifications remains a challenge in requirements engineering and formal methods, particularly for safety- and mission-critical systems whose verification depends on mathematically precise specifications. This paper evaluates whether contemporary off-the-shelf Large Language Models (LLMs) can help bridge this gap by generating Linear Temporal Logic (LTL) formulas directly from unstructured requirements. The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements. Five independent generations were collected for each requirement-model pair, yielding 450 candidate LTL formulas in total. Performance was assessed through manual semantic evaluation, pass@k for k in {1, 3, 5}, and a self-consistency measure capturing syntactic reproducibility across stochastic trials. The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NL-to-LTL task without task-specific fine-tuning. The study also considers understandability for non-experts by pairing generated formulas with model-produced natural language explanations and discussing the complementary use of timeline-based LTL visualization. The findings suggest that modern LLMs are becoming viable front-end assistants for semi-automated formalization workflows.
• Abstract（参考訳）: 非構造化の自然言語要件を形式的な仕様に自動翻訳することは、特に数学的に正確な仕様に依存する安全性とミッションクリティカルなシステムにおいて、要求工学と形式的手法における課題である。 本稿では,LTL(Linear Temporal Logic)式を非構造的要求から直接生成することにより,現代市販のLarge Language Models (LLMs) がこのギャップを埋めることができるかどうかを評価する。 本研究は, 構造的に異なる15の異種ベンチマークを用いて, 数発のプロンプト戦略を用いて, 近代LLMの6点について検討した。 それぞれの要求モデルペアに対して5つの独立した世代が収集され、450の候補TL式が得られた。 手動による意味評価,1, 3, 5} における k のpass@k と,確率的試行を通して構文再現性を評価する自己整合性尺度を用いて評価した。 その結果,現在の汎用LLMは,タスク固有の微調整を伴わない非構造化NL-to-LTLタスクにおいて,実質的に有意な性能を達成できることが示唆された。 この研究は、生成した式とモデル生成した自然言語の説明をペアリングし、タイムラインベースのLTL視覚化の相補的利用について議論することで、非専門家の理解可能性についても考察した。 この結果は,半自動フォーマライゼーションワークフローのためのフロントエンドアシスタントとして,現代のLLMが実現しつつあることを示唆している。

関連論文リスト

• Class Model Generation from Requirements using Large Language Models [5.685497917524985]
  大規模言語モデル(LLM)は、自然言語要求から自動的にクラス図を生成することができる。 本稿では,GPT-5,Claude Sonnet 4.0,Gemini 2.5 Flash Thinking,Llama-3.1-8-B-Instructなどの最先端LLMの能力について検討する。
  論文  参考訳（メタデータ） (2026-03-10T02:20:35Z)
• FASTRIC: Prompt Specification Language for Verifiable LLM Interactions [3.8073142980732997]
  大規模言語モデル(LLM)は複雑なマルチターンインタラクションプロトコルを実行するが、デザイナの意図に対する実行を検証するための正式な仕様がない。 本稿では、自然言語のプロンプトで暗黙的な有限状態機械(FSM)を明示するプロンプト仕様言語であるFASTRICを紹介する。
  論文  参考訳（メタデータ） (2025-12-22T01:19:50Z)
• 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)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• Beyond In-Context Learning: Aligning Long-form Generation of Large Language Models via Task-Inherent Attribute Guidelines [71.14354526117958]
  In-context Learning (ICL) は、事前訓練された大規模言語モデル(LLM)の重要かつ完全には理解されていない能力である。 タスク言語とフォーマット特性をキャプチャする2つのガイドラインの並列ストリームを効率よく生成するLongGuideを提案する。 LongGuideはガイドラインの最良の組み合わせを自動的に選択し、ゼロショット設定と少数ショット設定の両方で、強力なオープンソースLLMとクローズドソースLLMの両方を5%以上改善する。
  論文  参考訳（メタデータ） (2025-06-02T02:35:24Z)
• Self-Steering Language Models [113.96916935955842]
  DisCIPL は "self-steering" 言語モデル (LM) の手法である。 DisCIPLは、Followerモデルの集団によって実行されるタスク固有の推論プログラムを生成する。 我々の研究は、高度に並列化されたモンテカルロ推論戦略の設計空間を開く。
  論文  参考訳（メタデータ） (2025-04-09T17:54:22Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• Can Large Language Models Understand Real-World Complex Instructions? [54.86632921036983]
  大型言語モデル(LLM)は人間の指示を理解することができるが、複雑な命令には耐えられない。 既存のベンチマークでは、LLMが複雑な命令を理解する能力を評価するには不十分である。 複雑な命令を体系的に追従するLSMの能力を評価するためのベンチマークであるCellOを提案する。
  論文  参考訳（メタデータ） (2023-09-17T04:18:39Z)

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

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