大语言模型能否用 TLA+ 建模实际系统？

# LLMs能否用TLA+建模真实世界系统？ 来源：https://www.sigops.org/2026/can-llms-model-real-world-systems-in-tla/ ***编辑注：**AI正在积极推动计算系统形式化方法的应用前沿。在本文中，Specula团队（https://github.com/specula-org）分享了他们评估LLMs对系统代码进行建模的经验，这是代理模型检查的基本能力，使用TLA+这一用于并发和分布式系统的规范语言。本文是《系统智能的新地平线》（https://www.sigops.org/2025/the-next-horizon-of-system-intelligence/）系列博客的第七篇。* 几个月前，我们让Claude为Etcd的Raft实现（https://github.com/etcd-io/raft）写一个TLA+（https://lamport.azurewebsites.net/tla/tla.html）规范（spec）。它通过了语法检查，运行了TLC（https://github.com/tlaplus/tlaplus）模型检查器，乍一看像一个完善的形式化模型。随后我们注意到一个问题：这看起来像是Raft论文中的规范，与Etcd的具体细节几乎无关。Claude生成的不是一个Etcd的规范，而是Raft论文（https://raft.github.io/raft.pdf）附录中的规范。后来，我们一直在思考一个问题：我们如何判断AI是在忠实地建模一个计算系统，还是只是在复述系统的参考论文？ 随着大型语言模型（LLMs）不断改进，这个问题越来越难回答。LLMs几乎见过网上所有TLA+的例子。让它“写一个Raft规范”几乎等同于让它回忆训练中的东西。让它“写Etcd的规范”——一个反映Etcd如何分解其原子操作并演化其状态的规范——则是一个完全不同的问题。它考验的是LLMs是否能从复杂实现中抽象出逻辑，并将其转化为正确的形式化模型。 *SysMoBench*是我们通过自动基准测试来区分这两者的尝试。 ## 什么是SysMoBench？ SysMoBench向LLM提供十一个系统，并自动评估它生成的TLA+规范。 表1：SysMoBench中用作工件的系统 这十一个系统跨越了并发同步和分布式协议。对于每个任务，我们提供源代码、trace收集工具和不变式模板。 图1：SysMoBench概述 评估分四个阶段进行： 1. **语法阶段**检查规范是否能编译。 2. **运行时阶段**检查TLC是否能无错误地执行它。 3. **一致性阶段**使用trace验证，这是检查规范-代码一致性的常用方法：将代码的执行trace与模型进行比较。 4. **不变式阶段**检查规范是否满足关键的安全性和活跃性属性。 这四个阶段共同揭示了仅复述教科书与实际建模系统之间的差距。每个阶段产生动作级或不变式级的诊断信息，而不是单一的综合分数，这样我们就能看到规范在哪个动作或不变式上与实现不对齐。 ## LLM建模模式 当我们在SysMoBench上运行当今领先的LLMs——Claude、GPT、Gemini、DeepSeek、Kimi、Qwen等——时，出现了一个反复出现的模式。它们的规范在前两个阶段（语法和运行时）表现得相当好。大多数能干净地编译，许多能无错误地运行TLC。但是，一旦评估到达一致性阶段，两种系统性的“教科书建模”变得明显：（1）规范进入真实系统永远无法达到的状态；（2）规范无法达到真实系统总是能达到的状态。这两种失败模式直接反映在一致性和不变式分数上：即使是最新的领先LLMs，在一致性上平均约46%，在不变式上约41%，而语法分数接近满分。 在规范进入真实系统永远无法达到的状态的情况下，LLMs按照一个常见的形式化模板编写规范，该模板与系统的实际数据结构不匹配，因此规范允许产生真实系统永远不会产生的状态转换。一个具体的例子来自Claude Sonnet为ZooKeeper快速领导者选举（FLE）编写的规范。 图2：LLM生成的ZooKeeper FLE规范中的两种失败模式 在ZooKeeper代码中，每个服务器的recvset是一个以发送者为键的map：当同一个peer在新一轮发送新投票时，它会覆盖peer的旧投票。Sonnet将其写成一个集合并集，recvVotes' = recvVotes ∪ {newVote}，保留旧投票和新投票。“积累所有投票作为证据”的模式出现在许多形式化方法教科书中，但它与ZooKeeper的语义不匹配。因此，每当一个peer的投票在轮次之间发生变化时（在ZooKeeper的选举中经常发生），规范的后状态包含旧投票和新投票，而真实系统只保留新投票。一旦下游的quorum检查依赖于投票计数，规范就会进入真实代码永远不会进入的状态。 在规范无法达到真实系统能达到的状态的情况下，LLM将跨越代码中多个步骤的操作合并为一个单一的原子guard，使规范中的转换不可能实现。在Sonnet的同一个ZooKeeper规范中，HandleNotification动作携带了一个guard，m.electionEpoch <= logicalClock[s]，检查传入消息的epoch是否高于本地logicalClock。如果是，该动作被禁用。但是，ZooKeeper的代码不是这样工作的。当服务器收到具有更高electionEpoch的消息时，它首先将自己的logicalClock增加到匹配的值，然后处理消息。这两个步骤在代码中按该顺序发生。然而，LLM将它们融合到一个单一的guard中，这样做抹去了代码在每一轮选举中都会进入的状态（local epoch=1，incoming epoch=2）。 上述两种模式有一个共同的原因。LLMs生成的是结构完整、类型正确的TLA+模块，但这些是用教科书的形式化模板编写的，而不是反映实际实现。LLM知道Raft和ZAB作为协议是什么样子，但它不知道Etcd或ZooKeeper如何将特定操作分解为多个步骤。这正是为什么语法和运行时评估标准是不够的。LLM生成的所有规范都通过了SANY（https://github.com/tlaplus/tlaplus）TLA+解析器，因为它们结构完整且语法正确。要区分“建模Etcd”与“复述Raft论文”，评估必须到达一致性和不变式阶段，询问每个动作其转换是否与系统实际在运行时产生的状态变化相匹配。 ## 转换验证：以动作粒度读取规范 SysMoBench中的所有阶段都产生每个动作或每个不变式的诊断信息，而不是单一的综合分数。语法阶段不是编译整个模块，而是运行按动作分解来定位哪个动作格式不正确。运行时阶段分析每个动作的状态空间覆盖率，而不仅仅是TLC是否能执行规范。不变式阶段分别验证每个不变式，并让LLM将固定模板转换为每个生成规范的可运行不变式。一致性阶段使用我们所谓的*转换验证*，它最直接地揭示了“复述教科书协议”与“建模系统”之间的差距。 这个想法很简单。我们从系统的真实运行中收集执行trace，然后将每个trace切割成一系列“转换窗口”。一个窗口是一个三元组：（pre_state, action, post_state）。每个窗口独立地提供给TLC，检查规范的action是否可以从pre_state移动到post_state。输出不是单一分数，而是每个动作的明细，每个动作有一个通过率。 一个具体的例子：当我们对Asterinas的RwMutex运行转换验证时，输出是每个动作的记分卡，详细说明每个动作的通过率。粗粒度评估无法提供这种诊断。单一分数只能告诉你规范是通过还是失败，而转换验证不仅告诉你哪个动作不对齐，还告诉你哪个特定的状态转换失败了，追溯到trace中的特定窗口。 ## 发现：分数分化之处 在十一个系统上运行领先的LLMs表明，LLMs擅长生成正确的TLA+语法，但在确保一致性和适当的不变式方面存在困难。 图3：SysMoBench上11个LLMs各阶段的分数（按总分排序）；不同LLMs的排名可在SysMoBench排行榜（https://sysmobench.com/#/leaderboard）查看 大多数LLMs在语法阶段聚集在接近100%：几乎每个前沿LLM都能写出一个语法有效的TLA+规范。运行时阶段已经显示出分歧，从30%到92%不等。真正的差距出现在一致性和不变式上。在不变式阶段，最弱的LLM达到16%，而Gemini 3.1达到81%。 这种一致性和不变式分数较低的模式在系统级别上也是一致的。图4用Claude Sonnet-4.6作为代表性模型说明了这一点。在较简单的系统（Asterinas Spin、Mutex、RwMutex）上，几乎每个LLM都能以高分完成第1阶段（语法）到第4阶段（不变式）。在复杂的分布式系统（Etcd、RedisRaft、CURP、PGo raftkvs）上，LLMs可靠地在第1阶段（语法）获得100%或接近100%的分数，但从第2阶段（运行时）开始崩溃；有些根本无法让TLC运行，而那些能运行的在一致性和不变式分数上落在10%到50%之间。即使是Claude Sonnet 4.6这款最强大的LLM之一，在RedisRaft和CURP上的总分也只有25%。 图4：Claude Sonnet-4.6在不同系统上的总分，按难度等级排序（从易到难）。 我们在LLMs中观察到类似的行为。编写一个可以编译的TLA+模块是可以实现的，但将该模块与特定系统的实际行为对齐是困难的。高语法分数主要反映了训练数据中TLA+例子的丰富性。一旦评估要求像真实代码那样分解动作并匹配状态与数据结构，以前的例子就不再有用了。分别评估一致性和不变式粒度使我们能够区分“编写TLA+”和“建模特定系统”。 ## 开放挑战 有几个问题仍未解决。 首先，窗口级评估高度依赖于trace采样。转换验证无法评估trace未覆盖的代码路径。具体来说，在我们的一次运行中，Asterinas RwMutex中的AcquireUpReadLock动作的窗口为0——不是因为规范失败，而是因为upread()代码路径在该trace中根本没有被执行。转换验证清晰地报告了这一点，但它自己无法填补这个空白。系统地扩展trace覆盖仍然是一个开放问题。 其次，状态抽象不可避免地会丢失信息。将变量log表示为（logLen, logLastTerm）对对于深入检查log内容的操作是有损的，例如HandleAppendEntries检查特定中间条目的term。我们目前在转换验证模块中手动放宽这些限制，没有系统性策略。 第三，跨任务的可扩展性是一个挑战。添加新系统仍然需要手写的工具、不变式模板和转换验证模块。我们正在为这个流程搭建自动化框架，但完全自动化需要更多的工程工作。 这些是我们希望（最好与社区一起）解决的开放问题，而不是我们已经解决的问题。如果其中任何一个问题让你感兴趣，我们希望合作！ ## 下一步 我们将继续迭代SysMoBench，同时构建比原始LLMs更强大的代理工具。 事实上，我们发现前沿代码代理如Claude Code和Codex已经在TLA+建模真实世界系统方面表现出强大的能力：它们可以自主读取目标仓库，决定要建模什么，并推动完整的规范工作流程。我们正在开发Specula（https://github.com/specula-org/Specula），一个专门从事TLA+形式化建模的代理。Specula在当前SysMoBench任务上实现了一致性和不变式的满分（见我们的排行榜https://sysmobench.com/#/leaderboard）。 sysmobench.com（http://sysmobench.com/）上的排行榜正在持续收集新的LLMs和系统。我们欢迎贡献新系统、新的LLMs和新的结果！ - **论文：**https://arxiv.org/abs/2509.23130[1] - **代码：**https://github.com/specula-org/SysMoBench - **排行榜：**https://sysmobench.com/ [1] 随着LLMs的快速发展，本文报告的评估数字可能与原始论文中的不同。实际上，本文正是由最近请求用新一批模型重新运行SyscomBench而推动的。我们的排行榜会跟踪新模型。 本文由Haoran Qiu和Mike Chieh-Jan Liang编辑。