LLM能写正确的TLA+规格吗？评估自然语言到TLA+

TLA+ 已支持亚马逊和微软等公司的工业验证，但从自然语言编写正确的 TLA+ 规范仍然需要时间和专业知识，这限制了采用。大语言模型显示出了希望，但之前没有研究衡量它们是否从自然语言中生成语义正确的 TLA+ 规范。本文首次对基于 LLM 的自然语言 TLA+ 规范合成进行了系统评估。我们的研究在包含 205 个 TLA+ 规范的精选数据集上评估了 8 个系列的 30 个大语言模型：4 个提示策略（2,600 次运行）的 25 个开放权重模型和少数样本提示下的 5 个专有模型（130 次运行），所有这些均经过 SANY 解析器和 TLC 模型检查器验证。大语言模型的语法正确率高达 26.6%，但语义正确率仅为 8.6%，其成功仅靠渐进式提示。结果表明，模型大小并不能预测质量，例如，DeepSeek r1:8b 在所有策略中都优于其 70B 变体，这表明推理对齐对于形式语言的重要性。由于主流语言训练的负迁移，代码专用模型始终表现不佳。我们确定了五种反复出现的幻觉类别，所有这些类别都可以追溯到特定的训练数据偏差。这些结果表明，如果没有专家的监督，当前的大语言模型不会生成可靠的 TLA+ 规范。我们发布了评估框架、代码和数据集，以支持可重复性和未来的研究。