通过 LLM 将自然语言翻译为战略时间规范

系统要求的严格形式化是多代理系统（MAS）验证的基本先决条件。然而，众所周知，编写正确的形式规范是一项容易出错、耗时且需要大量专业知识的任务。这种困难在 MAS 中进一步加剧，其中要求必须捕获战略能力和临时目标。目前，还没有从自然语言导出 MAS 规范的既定方法。我们提出了一个框架，用于使用 大语言模型 (LLM) 将战略需求的自然语言描述转换为格式良好的 ATL/ATL* 公式。由于没有可用的数据集支持 NL 到 ATL/ATL* 翻译任务的监督学习，因此我们创建并整理了一个经过专家验证的新颖数据集，用于训练和评估微调模型。在保留的测试集上，根据与专家注释最一致的 LLM 判断进行评估，小型开放权重模型（3 - 7B 参数）的域内 微调 与强大的少数样本专有 API 基线相匹配。我们经过最佳微调的系统达到了 0.84 的语义准确性，统计上与最强的少数样本专有基线的 0.86 相当，同时保持了本地需求。我们进一步发现判断可靠性与生成模型能力成反比。开放权重的 Llama-3.3-70B 最密切地跟踪人类的判断，而最强大的专有模型是最不可靠的法官，过度拒绝参考文献的忠实释义。为了评估生成的规范的实际适用性，我们将我们的工具嵌入到现有的战略逻辑模型检查器中，使非专家用户能够用自然语言指定战略属性。