Translating Natural Language to Strategic Temporal Specifications via LLMs
作者: Marco Aruta, Francesco Improta, Vadim Malvone, Aniello Murano, Vladana Perlić
分类: cs.MA, cs.AI
发布日期: 2026-07-05
💡 一句话要点
提出基于大语言模型的自然语言到战略时序规范的翻译框架
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 多智能体系统 自然语言处理 形式化规范 大语言模型 需求分析 模型微调 时序逻辑
📋 核心要点
- 现有方法在多智能体系统中，需求的形式化编写既耗时又容易出错，缺乏有效的自然语言到形式规范的转换方法。
- 本文提出了一种利用大语言模型将自然语言描述转换为ATL/ATL*公式的框架，解决了现有方法的不足。
- 实验结果表明，经过微调的开放权重模型在语义准确性上与强大的少量示例基线相当，且能够有效支持非专家用户的需求表达。
📝 摘要（中文）
系统需求的严格形式化是多智能体系统（MAS）验证的基本前提。然而，编写正确的形式规范是一项容易出错、耗时且需要专业知识的任务，尤其在MAS中，需求必须捕捉战略能力和时序目标。目前尚无将自然语言推导为MAS规范的成熟方法。本文提出了一个框架，通过大语言模型（LLMs）将战略需求的自然语言描述翻译为有效的ATL/ATL*公式。我们创建并整理了一个新的专家验证数据集，用于训练和评估微调模型。在保留测试集上，经过微调的小型开放权重模型（3-7B参数）在语义准确性上达到了0.84，与最强的少量示例专有基线0.86相当，同时保持需求在本地。我们还发现，评估者的可靠性与生成器的强度成反比。
🔬 方法详解
问题定义：本文旨在解决多智能体系统中自然语言需求向形式化规范（ATL/ATL*）转换的困难，现有方法缺乏有效的转换机制，导致需求编写过程复杂且容易出错。
核心思路：通过构建一个基于大语言模型的翻译框架，将自然语言描述转化为形式化的ATL/ATL*公式，从而简化需求编写过程并提高准确性。
技术框架：该框架包括数据集创建、模型训练和评估三个主要模块。首先，构建专家验证的数据集；其次，利用该数据集对大语言模型进行微调；最后，评估模型在自然语言到形式化规范转换任务中的表现。
关键创新：最重要的创新在于创建了一个专门用于自然语言到ATL/ATL*翻译的新数据集，并通过微调开放权重模型实现了高语义准确性，突破了现有方法的局限。
关键设计：在模型训练中，采用了小型开放权重模型（3-7B参数），并通过专家验证的数据集进行微调，确保模型能够准确理解和生成形式化规范。
🖼️ 关键图片
📊 实验亮点
实验结果显示，经过微调的开放权重模型在语义准确性上达到了0.84，接近最强的少量示例专有基线0.86，表明该方法在自然语言到形式化规范转换任务中的有效性。同时，评估者的可靠性与生成器的强度呈反比，提供了新的研究方向。
🎯 应用场景
该研究的潜在应用领域包括多智能体系统的需求分析与验证，尤其适用于需要非专家用户参与的场景。通过简化需求表达过程，能够提高系统开发的效率和准确性，推动智能系统的广泛应用。
📄 摘要（原文）
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.