超越教科书：评估 LLM 在真实世界 TLA+ 建模中的表现

多年来，TLA+ 一直是规范并发和分布式系统的金标准，允许工程师在编写第一行代码之前就发现关键的设计缺陷。随着大语言模型 (LLM) 的兴起，人们越来越倾向于将这一严谨的过程委托给 AI。然而，一个关键问题仍然存在：AI 究竟是在对当前系统进行建模，还是仅仅在背诵其训练数据中广为人知的教科书式实现？

来自 Specula 团队的最新研究引入了 SysMoBench，这是一个旨在揭示“教科书式建模”与忠实系统表示之间差距的自动化基准测试。通过对十一个真实世界系统（从并发同步原语到像 Etcd 和 ZooKeeper 这样复杂的分布式协议）进行 LLM 评估，该团队揭示了当前 LLM 在处理形式化规范时存在的系统性失败。

正确性的幻觉

当被要求为 Etcd 的 Raft 实现编写 TLA+ 规范时，领先的 LLM 通常会生成通过语法检查并在 TLC model checker 中无错误运行的代码。乍一看，结果看起来很完美。然而，经过仔细检查，该规范往往反映的是原始 Raft 论文的附录，而不是 Etcd 实际实现中的特定架构选择。

这是基于 LLM 的建模的核心挑战。因为 LLM 已经见过网上几乎所有的 TLA+ 示例，要求编写“Raft spec”会触发其召回机制而非抽象机制。要真正地对一个系统进行建模，LLM 必须能够从复杂的源代码中抽象出逻辑，并将该抽象转化为正确的形式化模型。

SysMoBench 如何工作

为了区分召回与建模，SysMoBench 采用了四阶段评估流水线：

  1. Syntax Phase: 检查规范是否可以编译。
  2. Runtime Phase: 验证 TLC model checker 是否可以在不崩溃的情况下执行该规范。
  3. Conformance Phase: 使用轨迹验证 (trace validation) 将实际代码的执行轨迹与模型进行比较。
  4. Invariant Phase: 检查规范是否满足关键的安全属性 (safety) 和活性属性 (liveness)。

虽然大多数前沿 LLM 在语法阶段得分接近 100%，但在一致性 (conformance) 和不变性 (invariant) 测试期间，它们的表现大幅下降。在复杂的分布式系统中，即使是最强大的模型的总分也经常降至 10% 到 50% 之间。

“教科书式建模”的两种模式

研究识别了两种反复出现的失败模式，即 LLM 依赖通用模板而非实现细节的情况：

1. 承认不可能的状态

LLM 经常使用与系统实际数据结构不匹配的形式化模板。例如，在 ZooKeeper Fast Leader Election (FLE) 规范中，Claude Sonnet 将服务器的 recvset 视为集合并集，允许它累积所有投票作为证据。在真实的 ZooKeeper 代码中，这是一个以发送者为键的 map，意味着新投票会覆盖旧投票。这种差异导致规范进入了真实系统永远无法到达的状态。

2. 抹除可达状态

相反，LLM 经常将多个实现步骤合并为一个单一的原子守卫 (atomic guard)。在同一个 ZooKeeper 示例中，LLM 将更新本地逻辑时钟和处理消息的行为合并为一个步骤。在实际代码中，这些是顺序发生的。通过将它们合并，LLM 抹除了真实系统在每个选举轮次中都会进入的状态，使得规范中的某些转换 (transitions) 变得不可能。

转换验证：细粒度方法

为了精准定位这些失败，SysMoBench 利用了 Transition Validation。该系统不再对整个模块进行二元化的通过/失败判断，而是从实际运行中收集执行轨迹，并将其切割成“转换窗口” (pre-state, action, post-state)。

每个窗口都会输入给 TLC 以验证规范中的动作 (action) 是否真的能将系统从前置状态 (pre-state) 移动到后置状态 (post-state)。这提供了一个针对每个动作的评分卡，允许开发者准确看到究竟是哪个特定的状态转换失败了以及为什么，而不是依赖于粗略的聚合分数。

更广泛的影响与开放挑战

研究结果表明，虽然 LLM 在 TLA+ 的语言方面表现出色，但在特定实现的逻辑方面却很吃力。这引发了关于形式化方法未来的广泛讨论：

  • 耦合验证 (Coupled Verification): 一些人主张采用 Verus 等方法，将实现与验证耦合在一起，以防止模型与代码发生偏离。
  • 人类意图 (Human Intent): 有一种哲学上的担忧，即自动化设计过程会消除人类意图。正如一位评论者所指出的，如果 LLM 生成了设计和代码，那么“证明”可能缺乏有意义的人类保证。
  • Liveness Properties: 用户注意到，与安全属性 (safety properties) 相比，LLM 在处理活性属性 (liveness properties) 时尤其困难。

尽管存在这些障碍，Specula 团队正在开发专门的智能体 (agents) 能够自主阅读代码库并驱动规范工作流。他们的专用智能体 Specula 已经展示了在当前 SysMoBench 任务中实现完全一致性 (conformance) 和不变性 (invariant) 分数的能力，这表明未来的路径在于智能体工作流，而非单纯的 LLM 提示词工程。

结论

编写一个可以编译的 TLA+ 模块是低门槛；使该模块与特定系统的实际行为保持一致才是真正的挑战。随着我们向智能体化模型检查迈进，重点必须从语法转向一致性。目标不是生成一个看起来像 Raft 的规范，而是生成一个是该系统的规范。

Sources