Translating Natural Language to Strategic Temporal Specifications via LLMs

• URL: http://arxiv.org/abs/2606.30441v2
• Date: Thu, 02 Jul 2026 13:55:48 GMT
• Title: Translating Natural Language to Strategic Temporal Specifications via LLMs
• Abstract summary: We present a framework for translating Natural Language descriptions of strategic requirements into well-formed ATL/ATL* formulas.<n>Our best fine-tuned system reaches 0.84 semantic accuracy, statistically on par with 0.86 for the strongest few-shot proprietary baseline.<n>To assess the practical applicability of the generated specifications, we embed our tool to an existing strategic logics model checker.
• Score: 4.863985119779627
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A rigorous formalization of system requirements is a fundamental prerequisite for the verification of Multi-Agent Systems (MAS). However, writing correct formal specifications is well known as an error-prone, time-consuming, and expertise-intensive task. This difficulty is further accentuated in MAS, where requirements must capture strategic abilities and temporal objectives. At present, there is no established methodology for deriving MAS specifications from natural language. We present a framework for translating Natural Language descriptions of strategic requirements into well-formed ATL/ATL* formulas using Large Language Models (LLMs). Since no available dataset supports supervised learning for the NL-to-ATL/ATL* translation task, we create and curate a novel expert-validated dataset, employed for training and evaluating fine-tuned models. On a held-out test set, evaluated under the LLM judge that best agrees with expert annotations, in-domain fine-tuning of small open-weight models (3 - 7B parameters) matches strong few-shot proprietary API baselines. Our best fine-tuned system reaches 0.84 semantic accuracy, statistically on par with 0.86 for the strongest few-shot proprietary baseline, while keeping requirements on-premises. We further find that judge reliability is inverse to generator strength. The open-weight Llama-3.3-70B tracks human verdicts most closely, whereas the strongest proprietary models are the least reliable judges, over-rejecting faithful paraphrases of the reference. To assess the practical applicability of the generated specifications, we embed our tool to an existing strategic logics model checker, enabling non-expert users to specify strategic properties in natural language.

Related papers

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  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.<n>The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements.<n>The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NLto-LTL task without task-specific fine-tuning.
  arXiv  Detail & Related papers  (2026-08-06T17:13:07Z)
• ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
  textscReasonSTL is a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation.<n>textscReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction.<n>Experiments show that a 4B model trained with textscReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations.
  arXiv  Detail & Related papers  (2026-05-07T16:07:30Z)
• LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning [2.365021420497964]
  Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL)<n>In this work, we focus on enabling resource-efficient open-weight models to generate correct temporal logic (LTL) specifications from informal requirements.<n>We presentGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free specifications from informal input.
  arXiv  Detail & Related papers  (2026-03-05T22:34:45Z)
• SIEVE: Sample-Efficient Parametric Learning from Natural Language [66.46967795931559]
  We propose SIEVE, a method for sample-efficient parametric learning from natural language context.<n>We use a novel synthetic data generation pipeline, SIEVE-GEN, that leverages the insight that context is decomposable.<n>Our results show that SIEVE outperforms prior context distillation methods using just three query examples.
  arXiv  Detail & Related papers  (2026-02-02T18:52:52Z)
• RL-Struct: A Lightweight Reinforcement Learning Framework for Reliable Structured Output in LLMs [0.08594140167290097]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in natural language generation and reasoning.<n>Their integration into automated software ecosystems is often hindered by the "Structure Gap"<n>We propose a lightweight, efficient Reinforcement Learning framework to bridge this gap.
  arXiv  Detail & Related papers  (2025-11-29T04:47:14Z)
• LETToT: Label-Free Evaluation of Large Language Models On Tourism Using Expert Tree-of-Thought [18.539462131974215]
  We propose Expert $textbfT$ree-$textbfo$f-$textbfT$hought (LETToT), a framework that leverages expert-derived reasoning structures.<n>Results demonstrate the effectiveness of our systematically optimized expert ToT with 4.99-14.15% relative quality gains over baselines.
  arXiv  Detail & Related papers  (2025-08-15T07:37:12Z)
• Transferable Modeling Strategies for Low-Resource LLM Tasks: A Prompt and Alignment-Based Approach [1.3286097954612326]
  This paper addresses the limited transfer and adaptation capabilities of large language models in low-resource language scenarios.<n>It proposes a unified framework that combines a knowledge transfer module with parameter-efficient fine-tuning strategies.<n>It enhances task-specific adaptability while preserving the general capabilities of large language models.
  arXiv  Detail & Related papers  (2025-07-01T09:34:49Z)
• MoRE-LLM: Mixture of Rule Experts Guided by a Large Language Model [54.14155564592936]
  We propose a Mixture of Rule Experts guided by a Large Language Model (MoRE-LLM)<n>MoRE-LLM steers the discovery of local rule-based surrogates during training and their utilization for the classification task.<n>LLM is responsible for enhancing the domain knowledge alignment of the rules by correcting and contextualizing them.
  arXiv  Detail & Related papers  (2025-03-26T11:09:21Z)
• Context is Key: A Benchmark for Forecasting with Essential Textual Information [87.3175915185287]
  "Context is Key" (CiK) is a forecasting benchmark that pairs numerical data with diverse types of carefully crafted textual context.<n>We evaluate a range of approaches, including statistical models, time series foundation models, and LLM-based forecasters.<n>We propose a simple yet effective LLM prompting method that outperforms all other tested methods on our benchmark.
  arXiv  Detail & Related papers  (2024-10-24T17:56:08Z)
• TriSum: Learning Summarization Ability from Large Language Models with Structured Rationale [66.01943465390548]
  We introduce TriSum, a framework for distilling large language models' text summarization abilities into a compact, local model. Our method enhances local model performance on various benchmarks. It also improves interpretability by providing insights into the summarization rationale.
  arXiv  Detail & Related papers  (2024-03-15T14:36:38Z)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  We investigate the possibility of applying Large Language Models to SimulMT tasks. We conducted experiments using the textttLlama2-7b-chat model on nine different languages from the MUST-C dataset. The results show that LLM outperforms dedicated MT models in terms of BLEU and LAAL metrics.
  arXiv  Detail & Related papers  (2023-09-13T04:06:47Z)
• Offline RL for Natural Language Generation with Implicit Language Q Learning [87.76695816348027]
  Large language models can be inconsistent when it comes to completing user specified tasks. We propose a novel RL method, that combines both the flexible utility framework of RL with the ability of supervised learning. In addition to empirically validating ILQL, we present a detailed empirical analysis situations where offline RL can be useful in natural language generation settings.
  arXiv  Detail & Related papers  (2022-06-05T18:38:42Z)
• Explaining the Deep Natural Language Processing by Mining Textual Interpretable Features [3.819533618886143]
  T-EBAnO is a prediction-local and class-based model-global explanation strategies tailored to deep natural-language models. It provides an objective, human-readable, domain-specific assessment of the reasons behind the automatic decision-making process.
  arXiv  Detail & Related papers  (2021-06-12T06:25:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.