論文の概要: Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation

• arxiv url: http://arxiv.org/abs/2604.07321v1
• Date: Wed, 08 Apr 2026 17:36:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-09 17:30:51.659744
• Title: Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
• Title（参考訳）: 構文解析は簡単、意味論は難しい:LTL翻訳のためのLLMの評価
• Authors: Priscilla Kyei Danso, Mohammad Saqib Hasan, Niranjan Balasubramanian, Omar Chowdhury,
• Abstract要約: 線形時間論理は、ソフトウェア、ネットワーク、システムに対する望ましい要件とセキュリティおよびプライバシポリシーを指定するための一般的な形式である。 多くのセキュリティおよびプライバシ分析ツールは、入力として公式を必要とするため、この難しさにより、多くの開発者やアナリストにリーチできない。 本稿では,複数の代表的なLLMが英語の文を提案式に効果的に翻訳する方法を評価することによって,その前提を評価する。
• 参考スコア（独自算出の注目度）: 14.34799644541222
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Propositional Linear Temporal Logic (LTL) is a popular formalism for specifying desirable requirements and security and privacy policies for software, networks, and systems. Yet expressing such requirements and policies in LTL remains challenging because of its intricate semantics. Since many security and privacy analysis tools require LTL formulas as input, this difficulty places them out of reach for many developers and analysts. Large Language Models (LLMs) could broaden access to such tools by translating natural language fragments into LTL formulas. This paper evaluates that premise by assessing how effectively several representative LLMs translate assertive English sentences into LTL formulas. Using both human-generated and synthetic ground-truth data, we evaluate effectiveness along syntactic and semantic dimensions. The results reveal three findings: (1) in line with prior findings, LLMs perform better on syntactic aspects of LTL than on semantic ones; (2) they generally benefit from more detailed prompts; and (3) reformulating the task as a Python code-completion problem substantially improves overall performance. We also discuss challenges in conducting a fair evaluation on this task and conclude with recommendations for future work.
• Abstract（参考訳）: 命題線形時間論理(英: Propositional Linear Temporal Logic、LTL)は、ソフトウェア、ネットワーク、システムに対して望ましい要件とセキュリティおよびプライバシポリシーを指定するための一般的な形式である。 しかし、そのような要件とポリシーをLTLで表現することは、その複雑な意味論のため、依然として困難である。 多くのセキュリティおよびプライバシ分析ツールは、入力としてTLL式を必要とするため、多くの開発者やアナリストにリーチできない。 LLM(Large Language Models)は、自然言語の断片をLTL式に変換することによって、そのようなツールへのアクセスを拡大する。 本稿では,複数の代表的なLLMがアサーティブな英語文をLTL式に効果的に翻訳する方法を評価することによって,その前提を評価する。 人為的および合成的地下構造データを用いて, 構文的および意味的次元による有効性を評価する。 その結果,(1) LLMは, セマンティックな部分よりもLTLの構文的側面が優れていること, (2) より詳細なプロンプトの恩恵を受けること,(3) Pythonのコード補完問題としてタスクを書き換えることにより, 全体的なパフォーマンスが大幅に向上すること,の3つの知見が得られた。 また,この課題について公平な評価を行う上での課題についても論じ,今後の課題について提言する。

関連論文リスト

• RAVEL: Reasoning Agents for Validating and Evaluating LLM Text Synthesis [78.32151470154422]
  テスト担当者が自律的に設計し、典型的な合成操作を実行できるようにするためのエージェントフレームワークであるRAVELを紹介する。 C3EBenchは、プロの人間の文章から1,258個のサンプルを抽出したベンチマークである。 SOTA LLMを演算子としてRAVELを増強することにより、そのようなエージェントテキスト合成はLLMの推論能力に支配されていることがわかった。
  論文  参考訳（メタデータ） (2026-02-28T14:47:34Z)
• 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)
• 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)
• Linguistic Blind Spots of Large Language Models [14.755831733659699]
  言語アノテーションタスクにおける最近の大規模言語モデル(LLM)の性能について検討する。 近年の LLM は言語クエリに対処する上で有効性が限られており,言語学的に複雑な入力に苦しむことが多い。 この結果から,LLMの設計・開発における今後の進歩を示唆する知見が得られた。
  論文  参考訳（メタデータ） (2025-03-25T01:47:13Z)
• CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [1.433758865948252]
  我々は、自然言語仕様を表現に変換するためのデータ効率のよいインコンテキスト学習フレームワークであるCoT-TLを紹介した。 CoT-TLは、ローデータシナリオで3つの多様なデータセット間で最先端の精度を達成する。 我々はCoT-TLの実用性を自然言語命令に基づく多段階ドローン計画のためのQuadCopterに組み込む。
  論文  参考訳（メタデータ） (2024-10-21T17:10:43Z)
• SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。 学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。 ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
  論文  参考訳（メタデータ） (2024-07-16T04:41:58Z)
• Prefix Text as a Yarn: Eliciting Non-English Alignment in Foundation Language Model [50.339632513018934]
  教師付き微調整(SFT)は、基礎大言語モデル(LLM)の出力を特定の嗜好に合わせるための単純なアプローチである。 我々はこの仮説を言語間タスクの範囲内で批判的に検証する。 タスク関連トークンを最小化するPreTTYという新しいトレーニングフリーアライメント手法を提案する。
  論文  参考訳（メタデータ） (2024-04-25T17:19:36Z)
• Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis [103.89753784762445]
  大規模言語モデル(LLM)は多言語機械翻訳(MMT)の処理において顕著な可能性を示した。 本稿では, MMT における LLM の利点と課題を体系的に検討する。 また,ChatGPTとGPT-4を含む8つのLLMを徹底的に評価した。
  論文  参考訳（メタデータ） (2023-04-10T15:51:30Z)

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

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