Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note2 min read

Translating Natural Language to Strategic Temporal Specifications via LLMs

Source

arXiv

arxiv.org/abs/2606.30441v1

Read the source

Source

Plain-Language Brief

Researchers have developed a framework for translating Natural Language descriptions of strategic requirements into well-formed ATL/ATL* formulas using Large Language Models (LLMs). They created and validated a novel dataset for training and evaluating fine-tuned models. The best fine-tuned system reached 0.84 semantic accuracy, comparable to a proprietary baseline while keeping requirements on-premises. The generated specifications were integrated into an existing strategic logics model checker.

What the Document Says

  • A framework is presented for translating Natural Language descriptions of strategic requirements into ATL/ATL* formulas using Large Language Models (LLMs).
  • A novel dataset was created and validated for training and evaluating fine-tuned models.
  • In-domain fine-tuning of small open-weight models (3 - 7B parameters) matches strong few-shot proprietary API baselines.
  • The best fine-tuned system reached 0.84 semantic accuracy, statistically on par with the strongest few-shot proprietary baseline.
  • The strongest proprietary models are found to be less reliable judges compared to the open-weight Llama-3.3-70B model.
  • The generated specifications were integrated into an existing strategic logics model checker.

Key Concepts Mentioned

  • Multi-Agent Systems (MAS)
  • formal specifications
  • NL-to-ATL/ATL* translation
  • Large Language Models (LLMs)
  • semantic accuracy
  • strategic logics model checker

Claims Made by the Document

  • The framework translates Natural Language descriptions of strategic requirements into well-formed ATL/ATL* formulas using LLMs.
  • In-domain fine-tuning of small open-weight models matches strong few-shot proprietary API baselines.
  • The best fine-tuned system reaches 0.84 semantic accuracy, comparable to a proprietary baseline.
  • Judge reliability is inverse to generator strength.
  • The generated specifications can be integrated into an existing strategic logics model checker.

Evidence Used

  • The text describes the framework, dataset creation, model evaluation, semantic accuracy, and integration of the specifications.

Methods / Approach

UNKNOWN

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

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.