Translating Natural Language to Strategic Temporal Specifications via LLMs
Marco Aruta, Francesco Improta, Vadim Malvone, Aniello Murano, Vladana Perli\'c
Why It Matters
What makes this one worth your time
This work is relevant for AI researchers and engineers interested in simplifying the specification process for multi-agent systems, potentially reducing the expertise barrier in formalizing system requirements.
The paper develops a framework to translate natural language into strategic temporal specifications using LLMs.
Summary
The paper presents a framework for translating natural language descriptions of strategic requirements into ATL/ATL* formulas using Large Language Models (LLMs). It introduces a novel dataset for training and evaluating these models, achieving competitive semantic accuracy with fine-tuned models compared to few-shot proprietary baselines. The framework is integrated into a strategic logics model checker to allow non-experts to specify strategic properties in natural language.
Key contributions
- A framework for translating natural language to ATL/ATL* formulas using LLMs.
- Creation of a novel expert-validated dataset for training and evaluating NL-to-ATL/ATL* translation models.
- Integration of the translation tool into a strategic logics model checker.
Notable insights
- The reliability of LLM judges is inversely related to the generator's strength, with open-weight models aligning more closely with human judgments.
- Embedding the translation tool into a model checker allows non-experts to specify strategic properties in natural language.
Possible limitations
- Not stated in the abstract
Abstract
arXiv:2606.30441v2 Announce Type: replace-cross 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.