Translating Natural Language to Strategic Temporal Specifications via LLMs
作者: Marco Aruta, Francesco Improta, Vadim Malvone, Aniello Murano, Vladana Perlic
分类: cs.MA, cs.AI
发布日期: 2026-06-29
💡 一句话要点
提出基于大语言模型的自然语言到战略时序规范的翻译方法
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 多智能体系统 自然语言处理 形式化规范 大语言模型 需求分析
📋 核心要点
- 现有方法在多智能体系统中，需求的形式化编写既耗时又容易出错，缺乏有效的自然语言到形式规范的转换方法。
- 本文提出了一种利用大语言模型将自然语言描述转换为ATL/ATL*公式的框架，解决了需求表达的复杂性问题。
- 实验结果表明，微调的小型开放权重模型在语义准确率上与强大的专有基线相当，且在实际应用中表现出良好的可用性。
📝 摘要（中文）
系统需求的严格形式化是多智能体系统（MAS）验证的基本前提。然而，编写正确的形式规范是一项容易出错、耗时且需要专业知识的任务，尤其在MAS中，需求必须捕捉战略能力和时序目标。目前尚无从自然语言推导MAS规范的成熟方法。本文提出了一种框架，通过大语言模型（LLMs）将战略需求的自然语言描述翻译为规范的ATL/ATL公式。由于缺乏支持NL到ATL/ATL翻译任务的监督学习数据集，我们创建并整理了一个新的专家验证数据集，用于训练和评估微调模型。在持出测试集上，经过微调的小型开放权重模型（3-7B参数）在与专家注释最一致的LLM评估者下，达到了与强大的少量示例专有API基线相匹配的表现。我们的最佳微调系统达到了0.84的语义准确率，统计上与最强的少量示例专有基线0.86相当，同时保持需求在本地。我们还发现评估者的可靠性与生成器的强度成反比。
🔬 方法详解
问题定义：本文旨在解决多智能体系统中自然语言需求描述到形式规范的转换问题。现有方法缺乏有效的转换机制，导致需求表达的复杂性和错误率高。
核心思路：通过大语言模型（LLMs）将自然语言描述翻译为规范的ATL/ATL*公式，利用微调技术提升模型在特定任务上的表现。
技术框架：整体架构包括自然语言输入、LLM翻译模块、生成的ATL/ATL*公式输出及评估模块。首先，输入自然语言描述，然后通过微调的LLM进行翻译，最后输出形式化的规范并进行评估。
关键创新：最重要的创新在于创建了一个专家验证的数据集，支持NL到ATL/ATL*的翻译任务，并通过微调小型开放权重模型实现了与专有模型相当的性能。
关键设计：在模型训练中，采用了特定的损失函数以优化语义准确率，并对模型参数进行了精细调整，以确保在特定任务上的最佳表现。
🖼️ 关键图片
📊 实验亮点
实验结果显示，最佳微调系统达到了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.