Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

想象一下，你正试图教一个非常聪明、博学多才的机器人如何为一个复杂的机器编写一份严格的数学配方。这个机器是一个“分布式系统”（比如运行亚马逊或微软服务的云端服务器），而这份配方是用一种名为 TLA+ 的特殊语言编写的。

这种语言就像是一个高风险的谜题。如果你漏掉了一个微小的符号，或者逻辑稍有偏差，机器在配方中看起来可能没问题，但在现实运行中却会崩溃。问题在于，手工编写这些配方既困难又缓慢。因此，研究人员提出了一个问题：我们能不能直接要求现代人工智能（大语言模型，简称 LLM）来替我们编写这些配方？

这篇论文是关于这个问题的第一份重大评估报告。以下是他们的发现，通过简单的解释呈现如下：

1. “语法与意义”之间的鸿沟

研究人员要求 30 个不同的 AI 根据纯英文描述来编写这些 TLA+ 配方。

• 好消息（语法）： 大约 26% 的时间内，AI 编写的配方在表面上看起来是正确的。其“拼写检查器”（称为 SANY）表示：“好的，单词和符号的顺序是正确的。”
• 坏消息（意义）： 然而，当他们实际将配方通过“逻辑测试器”（称为 TLC）来检查它是否真的有效时，只有 8.6% 的时间能够通过测试。

类比： 想象你要求一名学生写一份法律合同。该学生使用了完美的拼写和语法（成功率 26%），但他们写的合同实际上表达的意思与原意相反，或者遗漏了一个关键条款，导致合同在法律上毫无用处（成功率仅为 8.6%）。AI 擅长模仿这种语言的外表，但在理解其背后的逻辑方面经常失败。

2. 规模并不总是代表更好

通常，我们会假设更大、更强大的 AI 会做得更好。但在本研究中，情况并非如此。

• 令人惊讶的结果： 一个较小的 AI 模型（DeepSeek r1:8b）表现得比它的“大哥”（DeepSeek r1:70b）要好得多。
• 原因： 较小的模型经过专门训练，能够“逐步思考”（就像一名展示解题步骤的数学系学生），而较大的模型由于在海量的通用互联网数据上进行了训练，反而被 TLA+ 严格的规则搞混了。这就像是一位知道如何制作舒芙蕾的专业厨师，对比一位虽然什么都会做但可能会在特定食谱上过度思考的通才。

3. “代码专家”也失败了

研究人员测试了一些以编写计算机代码（如 Python 或 Java）闻名的 AI。令人惊讶的是，这些“代码专家”的表现甚至不如通用型 AI。

• 原因： 这些模型太习惯于编写带有分号 (;) 或花括号 ({}) 的代码了，以至于它们会不自觉地将这些符号带入 TLA+ 配方中。由于 TLA+ 不使用这些符号，配方会立即报错。这就像一名木匠试图修理手表，却因为习惯了使用锤子而误用了锤子。

4. “逐步进行”的技巧效果最好

研究人员尝试了四种不同的向 AI 求助的方法。最成功的方法被称为 “渐进式提示”（Progressive Prompting）。

• 运作方式： 他们没有要求 AI 一次性写完整个配方，而是让它一部分一部分地构建：“首先，写标题。现在，写变量。现在，写规则。”
• 结果： 这是唯一能产生任何完整工作配方的方法（即那 8.6% 的成功率）。这就像盖房子：如果你试图一次性完成屋顶、墙壁和地基，你很可能会失败；但如果你一间房一间房地建造，成功的机会就会更大。

5. AI 的“幻觉”

论文发现了 AI 反复犯错的五种特定方式，研究人员称之为“幻觉”：

1. 错误的符号： 使用了华丽的数学符号（如 ∧），而不是 TLA+ 所要求的普通文本符号（如 /\）。
2. 语言混杂： 意外地加入了其他编程语言中的分号或反引号。
3. 思维外泄： AI 有时会将自己的“思考过程”（如 ...）直接粘贴到最终的配方中，从而导致配方失效。
4. 长度错误： 有时 AI 写的配方比要求的长 9 倍，或者有时几乎什么都没写。
5. 结构损坏： 缺少了配方的“结束”标记，导致文档不完整。

总结

论文得出结论：目前的 AI 还无法独立编写可靠的 TLA+ 规范。 虽然它们可以模仿这种语言的外观，但在逻辑错误方面仍然过多，无法在没有人类专家逐行检查的情况下被信任。

研究人员建议，为了解决这个问题，我们需要：

• 使用“逐步进行”的提示方法。
• 使用专注于推理的较小模型，而不是庞大的通用模型。
• 构建自动修复常见错误（例如移除错误的符号）的工具，在 AI 尝试运行配方之前就完成处理。

在此之前，编写这些关键系统的配方仍然是一项需要人类专家完成的工作，而 AI 只能充当一个有用但容易出错的助手。