这篇文章探讨了大型语言模型(LLMs)是否能够使用TLA+形式化建模语言来准确模拟现实世界系统，主要关注LLMs在复杂系统建模方面的潜力和局限性。

大语言模型能否用TLA+为现实系统建模？——来自Specula团队的探索

核心发现

研究团队发现，当要求Claude等大语言模型为Etcd的Raft实现编写TLA+规范时，模型生成的代码虽然能通过语法检查和TLC模型验证器，但实际上只是复现了Raft论文附录中的通用规范，并未准确反映Etcd的具体实现细节。这一现象引发关键问题：如何区分LLM是在真实建模系统，还是在复述文献内容？

SysMoBench评估框架

为解决该问题，团队开发了SysMoBench自动化评估平台，其特点包括： 1. 多维度评估：包含语法检查、运行时验证、一致性检验（通过轨迹验证）和不变性验证四个阶段 2. 细粒度诊断：提供动作级和不变式级的详细诊断，而非单一总分 3. 测试系统：涵盖11个并发同步和分布式系统（如Etcd、ZooKeeper等）

LLM建模的典型问题

评估发现主流LLM（Claude、GPT、Gemini等）存在两类系统性缺陷： 1. 过度泛化：规范允许实际系统不会出现的状态（如ZooKeeper选举中错误保留历史投票） 2. 过度简化：将多步操作合并为原子守卫，遗漏关键中间状态

评估结果对比

• 语法阶段：几乎所有LLM都能达到近100%正确率
• 运行时阶段：正确率降至30%-92%
• 一致性验证：平均仅46%通过率
• 不变性验证：平均41%通过率（最佳模型Gemini 3.1达81%）

开放挑战

1. 轨迹采样覆盖不足问题
2. 状态抽象导致的信息丢失
3. 跨任务泛化能力有限
4. 新系统评估仍需人工编写测试套件

未来方向

团队正在开发专用智能体Specula，其特点包括： - 能自主阅读代码库并决定建模内容 - 在当前SysMoBench任务中实现100%一致性验证 - 通过公开排行榜持续追踪模型进展

（注：本文保留了核心技术细节，删减了重复的导航菜单、历史文章列表等非关键内容，合并了部分同类数据呈现）

以下是评论内容的总结，平衡呈现不同观点并保留关键引用：

1. 支持Verus等集成验证方法的观点

   • dgacmu认为Verus将实现与验证耦合的方式更优，可避免模型与实际实现脱节 关键引用： "This post reads like an accidental advertisement for approaches like Verus" "I'm personally much more optimistic about the verus approach"

2. 关于TLA+应用的讨论

   • tmaly提到NVIDIA曾赞助TLA+挑战赛
   • tombert指出Claude在TLA+建模能力上的进步，举例成功建模大富翁规则 关键引用： "Claude has certainly been getting better with TLA+" "I got it to model the rules of Monopoly last night"

3. 对LLM自动生成模型的质疑

   • atomicnature质疑完全自动化会失去人类设计意图
   • simplegeek指出LLM在安全性和活性属性方面仍有不足 关键引用： "if one automates all this there is no human intent/design anymore" "they struggle to come up with correct safety and liveness properties"

4. LLM辅助建模的实践建议

   • simplegeek建议先手工起草再使用LLM辅助
   • iFire转向使用Lean 4进行实际系统建模 关键引用： "I always try to write the first draft with hand" "I don't use tla+ to model real-world systems anymore"

5. 相关工具与基准测试

   • alhazrod介绍TLAiBench基准测试套件 关键引用： "TLAiBench: A dataset and benchmark suite for evaluating LLMs"

6. 开放性问题

   • pzoln提出让LLM根据源代码生成TLA+规范的设想 关键引用： "what if you give LLM just a source code...ask it to create a TLA+ spec"