当我们谈论大模型是否能替代人类编写形式化规格说明时，常常陷入两种极端：要么盲目乐观，认为 AI 已经可以处理任何工程问题；要么过度悲观，认定形式化方法永远是人类的自留地。SysMoBench 基准的出现提供了一个务实的评估框架，它不满足于简单询问「模型能否写 TLA+」，而是将验证拆解为四个递进的检查维度，让失败原因变得可定位、可量化、可修复。本文将深入分析这四个维度揭示的具体失败模式，以及它们对工程实践的启示。
基准设计：从整体准确率到细粒度诊断
SysMoBench 由南京大学、微软亚洲研究院、不列颠哥伦比亚大学和伊利诺伊大学香槟分校的研究者共同构建，其核心思路是将大模型生成 TLA+ 规格的能力分解为四个逐步严格的验证层次。第一层检查语法正确性，即生成的 TLA+ 代码是否能够通过 TLC 模型检查器的编译；第二层验证运行时可行性，确认模型在 TLC 中可以正常执行而不触发错误；第三层检验代码合规性，将真实系统的执行轨迹输入模型，看模型是否接受这些行为；第四层验证不变量正确性，检查安全性和活性不变量是否在所有可能的状态转换中得到维护。
这种分层设计的价值在于，它将一个模糊的「模型能否建模」问题，转化为四个独立可测量的子问题。当我们发现模型在第四层失败时，不需要回头去质疑第一层是否通过，因为每一层的评估都是独立的。这种思路与软件测试中的单元测试、集成测试、系统测试的分层理念一脉相承，只是将测试对象从代码换成了规格说明。
基准当前涵盖十一个真实系统工件，包括 etcd 和 Redis 的 Raft 共识实现、ZooKeeper 的领导者选举、以及 Asterinas 操作系统中的自旋锁、互斥锁和环形缓冲区。这些系统的共同特点是它们都是并发或分布式系统中的关键组件，其行为正确性直接影响到整个系统的可靠性。选择真实系统而非教科书示例，使得评估结果更具工程参考价值。
四层验证的具体失败模式
语法与运行时层面的基础障碍
在第一层和第二层，模型面临的主要挑战是 TLA+ 特有的语法约束和类型系统。与多数编程语言不同，TLA+ 采用一阶谓词逻辑作为基础，其变量声明、集合运算和操作符重载都有严格的语法规则。常见的失败模式包括：常量未定义就引用、集合运算中类型不匹配、操作符使用不符合 TLA+ 惯例、以及模块导入路径错误。这些问题看似基础，但对于没有经过专门形式化方法训练的大模型而言，恰恰是最常见的绊脚石。
一个典型的例子是模型可能将普通编程语言中的数组索引语法直接迁移到 TLA+，而 TLA+ 使用的是集合论表示法。模型生成的代码可能在语法上看起来合理，但 TLC 在执行时会因为无法解析运算而崩溃。更棘手的是，某些语法错误不会在编译阶段暴露，而会在模型检查阶段才表现为运行时错误，这意味着即使通过了第一层验证，第二层仍可能失败。
代码合规性：规范与实现的鸿沟
第三层验证是 SysMoBench 最具创新性的设计。它要求模型不仅能写出语法正确的 TLA+ 规格，还要让这些规格能够接受真实系统的执行轨迹。这一层的失败揭示了一个根本性问题：模型生成的规格与实际代码的行为之间存在语义鸿沟。
以 ZooKeeper 的领导者选举为例，真实的选举过程涉及复杂的超时机制和选票比对逻辑。如果模型在规格中简化了这些细节，比如假设选举总是立即完成或忽略了网络延迟的影响，那么当真实系统的执行轨迹输入模型时，模型会拒绝这些本应合法的行为序列。反之，如果模型过度泛化，接受了不该接受的行为，安全性不变量就可能在下一层被突破。
这一层的评估方法值得深入探讨。研究者们首先在真实系统中植入探针，收集系统运行时的状态转换序列，然后将这些轨迹作为输入提供给 TLC 模型检查器。如果模型正确建模了系统行为，这些轨迹应该被模型接受；如果模型规格与实现存在偏差，模型会标记某些状态为不可达或非法。这种方法类似于反向工程，只是从代码逆向出规格，再用规格来验证代码的一致性。
不变量验证：安全性的终极检验
第四层验证不变量正确性，是 SysMoBench 对模型最严格的要求。安全性和活性不变量是形式化方法的核心产物，它们用数学语言描述系统必须始终满足的性质。例如，互斥不变量要求任意时刻最多只有一个进程进入临界区；活性不变量则要求每个请求最终都会得到响应。
模型在这一层的失败模式尤为值得关注。首先是模板实例化错误：SysMoBench 采用了模板驱动的评估方法，先定义不变量的通用结构，再由模型根据具体系统填充细节。模型可能在实例化过程中引入错误的变量引用，比如将 processId 和 nodeId 混淆，或者在条件判断中使用了错误的比较操作符。其次是遗漏关键约束：某些安全属性需要考虑多个条件的组合，模型可能只捕捉到部分约束，导致不变量过于宽松，无法捕获实际的违规行为。
一个具体案例是模型为自旋锁生成的互斥不变量可能写成 ENABLED(EnterCriticalSection) <= 1，但正确的规格应该考虑锁的持有时间窗口和释放时序。如果模型忽略了锁状态转换的具体时序，不变量虽然形式上正确，但无法有效验证并发安全性。
对工程实践的参数化启示
虽然当前大模型在 SysMoBench 上的整体表现表明形式化建模能力仍有显著提升空间，但基准的细粒度评估为工程应用提供了可直接落地的参数建议。对于希望在工作中引入 AI 辅助形式化建模的团队，可以考虑以下实践策略。
在语法层面，建议在提示工程中添加 TLA+ 语法检查清单，包括常量声明顺序、模块导入规范和集合运算类型匹配规则。同时，可以在模型输出后串联一个轻量级的语法验证步骤，及时捕获基础错误，避免错误向上层传播。根据 SysMoBench 的实验数据，这一层的人工干预成本最低，但能显著提升后续验证的效率。
在合规性层面，最有效的策略是采用迭代式建模：先让模型生成粗粒度的规格框架，再通过真实系统的测试用例逐步细化。具体做法是在系统中植入日志探针，提取关键状态转换，然后将典型轨迹反馈给模型，让它据此调整规格描述。这种人类在环的迭代方式比一次性生成完整规格的成功率更高。
在不变量层面，建议将不变量的验证与代码审查流程绑定。每当模型生成一个新的安全或活性不变量时，应该安排人工 review，确认变量引用和条件判断的准确性。同时，可以利用 TLC 的反例输出功能，当不变量验证失败时，分析具体的违规模式，这比从头调试规格更为高效。
基准方法论的价值与局限
SysMoBench 的四层验证框架为评估 AI 形式化建模能力提供了一个可复用的方法论。它的贡献不仅在于提供了基准数据，更在于展示了如何将一个宏观问题分解为可独立测量的子问题。这种方法可以推广到其他形式化规格语言的评估，比如 Coq、Isabelle 或 Dafny。
然而，基准本身也存在局限性。首先，当前覆盖的十一个系统虽然涵盖了分布式系统、操作系统和共识协议，但相对于形式化方法的广泛应用领域而言，样本量仍然有限。其次，基准主要评估的是规格生成的正确性，而非规格的质量本身一个语法完美且满足不变量的规格，可能因为过度抽象而失去工程价值。最后，基准假设模型已经理解了系统的代码实现，但在实际工程中，让模型理解大型代码库本身就是一项挑战。
尽管存在这些局限，SysMoBench 仍然为大模型在形式化方法领域的能力评估奠定了基础。它的出现意味着我们能够更精确地定位模型的薄弱环节，并有针对性地改进提示策略或模型架构。对于形式化方法社区而言，这提供了一个重新审视 AI 辅助工程的可能性；对于 AI 研究者而言，这指出了一个具体且有价值的模型能力提升方向。
参考资料
- SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems, arXiv:2509.23130
- Review: SysMoBench, emptysqua.re/blog/review-sysmobench
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。