这条在讲一个 TLA+ 证明的 agent benchmark，叫 TLAPS-Bench。出处是 arXiv:2611.02849，上礼拜提交的，第一作者 Qian Cheng，16 位作者。主分类 cs.AI，交叉挂了 cs.DC、cs.LO、cs.SE——分布式计算、逻辑、软件工程，这堆分类本身就说明它没打算待在某个小圈子里。
我一开始以为又是“AI 证定理”那类 benchmark。这两年这种东西不少，分数一个比一个好看，仔细一看全是合成例子自嗨。合成例子的问题是——模型在训练数据里见过类似结构，刷分不代表真会。读到第三页我才确认值得推荐：证明目标不是合成的，是真实系统的 TLA+ 规格。265 个目标，来自 95 个系统。
95 个系统这个数我得停下来想想。真实的 TLA+ 规格，每个证明目标背后都是一个真的分布式系统——缓存一致性、拜占庭共识、预写日志。这些不是教学玩具，是生产环境里会出事的东西。拿它们当证明目标，分数涨不上去就是涨不上去，模型没处躲。
还有一点，论文里写了防奖励作弊的保障措施。agent 评测最怕这个——模型找条捷径刷分，benchmark 分数虚高，实际能力没到。TLAPS-Bench 专门做了防作弊，说明作者知道死穴在哪。具体怎么防的，正文没展开太细，但光是把这条写进方法论、当成设计目标之一，已经比大多数 benchmark 强了。很多 benchmark 压根不提 reward hacking，分数虚高就虚高，反正大家爱看高分。
分数最高的是 GPT-6.1 Sol (max)。70 个目标子集里证了 31 个，44.3%。这数字放别的 benchmark 里不算好看，但放在一个防了作弊的 benchmark 里，我信。作者原话是「端到端证明开发过程中的困难与潜在机会」——困难是真的，机会也是真的，前提是你信这个分数。我信。
这个 benchmark 的证明必须通过 TLAPS 机器检验。不是模型自己说“证完了”就算，是 TLAPS 把每个证明义务一个个消掉。测试可以被模型猜过——大模型训练数据里见过类似的用例，蒙对一条两条不稀奇。机器检验的证明不能猜，要么能过，要么不能过，没有“大概对了”。这个硬标准本身就筛掉了一堆自欺欺人的东西。
所以我看到 44.3% 的时候，没觉得“AI 不行”。反而觉得在机器检验、防作弊的前提下能到这个数，说明这条路不是完全走不通。端到端证明开发的真正难点在哪，论文里点了一句：要发现归纳不变式。这是 TLA+ 证明里最难的活，不变量选错了，后续证明根本走不下去。但 AI 代理在发现归纳不变式上到底表现怎么样，正文没展开。我翻附录想找每个证明目标的失败原因对应表，20 张表，没翻完。
写到这里得承认：这篇我还没全读完。正文 10 页读完了，附录 20 张表只翻了几张。所以上面关于归纳不变式的判断不算数——那只是我的疑问，不是论文的结论。我读的时候一直在想：这 44.3% 里，有多少证明目标是在人类先给定归纳不变式之后，AI 才证出来的？如果 AI 只做“拆解证明义务”这种体力活，真正难的“找不变式”还是人做的，那 44.3% 也得打个折。
这个问题可能附录里有答案。我还没读到，先挂着。
顺手跑一下？这条跑不了。不是环境问题，是我手头没有能跑 TLA+ 证明的 agent 环境，而且附录数据还没读完。所以这条只是“读了”的推荐，不是“跑了”的验证。等我把附录翻完、搞清楚归纳不变式那个疑问，再决定要不要收回半句。
还有个细节。正文才 10 页，总共 35 页，7 张图，20 张表。20 张表啊。作者没想只讲个好听的故事，把数据全摊出来了。这种写法不讨好，但很对。做 benchmark 就该这样，把原始数据摆出来，让别人能复核。光是这个数据透明度，就比那些“我们跑了个实验分数很高具体数据见私有仓库”的强太多。
不点链接也能带走的一句：给 agent 评测做 benchmark，防 reward hacking 比刷高分重要。一个没防作弊的 benchmark，分数越高越可疑。