一条通关路线只是上界：AWM 用 Lean 4 证明"不可能"，以及六次里那次没迁回真实环境的失

10 月 29 日，arXiv 上出现一篇题为《Algebraic World Model: From Exploration to Proofs》的论文，作者栏里有姚期智，副标题挂着袁洋。11 月 1 日，清华交叉信息研究院团队公开介绍。论文编号 2610.40503。

这篇论文做的事，和过去两年"世界模型"这个词的常见用法不一样。主流路线是预测下一帧——猜下一秒画面长什么样，猜得越准说明理解越深。AWM 换了目标：把环境里的对象和规则写成可执行的数学模型，然后用 Lean 4 证明"某个目标能到达"或"某个目标到不了"。

真正值得工程侧关注的，不是"AI 像牛顿一样思考"这类说法，而是一个很具体的能力：当 Agent 说"做不到"的时候，它能不能把这句话变成一份可被机器逐行检查的证明。

论文在这个点上给出了目前最干净的对照数据，也主动交代了一处失败：六条模型级证明里，只有五条能迁回原始环境。

一、先把"找到了"和"最优"分开

实验设在一个叫 ARC-AGI-3 的基准上。这是 ARC Prize 2026 年 3 月 25 日发布的第三代版本，也是第一个交互式推理基准。智能体被丢进一个全新环境，没有规则说明，没有目标提示，没有自然语言指令，得靠自己动手试出这个世界的物理法则。发布时前沿模型的平均分低于 1%。

团队没有直接刷这个榜。他们从基准里挑了一个叫 sc25 的游戏，机制保持不变，只做一件事：把通关步数预算压到比理论最优值少一格。

第四关，引擎穷举确认最少需要 19 步，预算只给 18 步。第五关，最优 36 步，预算给 35 步。

按构造，这两关在数学上不可能赢。

然后让模型去玩，看它敢不敢说"过不去"，以及这个结论有没有依据。

GPT-6 Astra 试了 8 轮，给出判断：18 步肯定不行，我估计至少要 22 步。

这个回答里藏着一个工程上极常见的混淆。Astra 确实找到了一条 22 步的通关路线，这条路线是真的。但"存在一条 22 步的路线"只能说明最优解不超过 22，它给出了一个上界。有了上界之后，它顺手把 19、20、21 三档全排除了，这一步没有依据。

十二次对照实验里，GPT-6 Astra 与 Claude Opus 5.5 加起来只有 5 次判断出"不可能"，其中 4 次给出的最少步数还是错的。Claude Opus 5.5 唯一答对的那次，理由写的是"我手算的路径长度确实是最小"——把它当成了已知条件，没有去核。

在游戏里，这个错误最多让你多试几次。放到生产环境，一个 Agent 告诉你"这个配置组合满足不了 SLA"，然后给出一个错得挺远的数字，后果是另一回事。

上界靠搜索就能拿到，下界必须靠证明。 这是整篇论文的分水岭，也是后面三阶段流水线存在的理由。

二、十二次对照：0/6 与 6/6 之间隔着一个内核

同一组不可能关卡，各跑六次。结果如下。

三个基线都有代码执行能力，都能写 Python、能跑搜索。它们的差别不在算力，在产物形态：模型给出的是一个数字，AWM 给出的是一个证明。

数字可以错得很难看，而且错了你没办法当场知道。证明不能——Lean 4 的内核会逐行检查，通不过就是通不过。

这里有个容易被滑过去的细节：AWM 的初始界限也不是全对，六次里错了两次。但它拿到"游戏里存在更省的路"这一句反馈之后，四轮之内两次都重新产出了封闭证明，最终六次界限全对。第四节的自我修正环节会专门讲这个过程。

还有一个口径问题需要标出来。量子位同一篇报道里出现过"基于 Opus 5.5 模型的 AWM"和"它用 Opus 5"两种写法，论文表格里记的是 Claude Opus 5，对照基线用的是 Opus 5.5 与 GPT-6 Astra。本文按论文表格采用 Opus 5，但这一点属于媒体报道不一致，读者引用时注意。

三、势函数：整篇论文只有一个数学机制

"证明不可能"听起来是个很重的任务。AWM 用的是一个在算法课里很常见的东西。

定义一个势函数 V，对每一个合法状态转移都满足：

V(s) ≤ c(s → s') + V(s')

V(goal) ≤ 0

把不等式沿任意一条通关路径累加，中间项全部消掉：

V(s0) ≤ Σc + V(goal) ≤ Σc

于是任何一条通关序列的总成本都不低于起始点的 V(s0)。只要 V(s0) = 19，就能断言"18 步预算内无解"，而且这个断言覆盖了所有路径，包括从未被探索过的分支。

做过 A* 搜索的人会立刻认出这个形状：这就是 admissible heuristic 的定义，h(s) ≤ c(s,s’) + h(s’)，启发函数不高估真实代价就保证搜索最优。AWM 的本质，是让大模型从交互里自己学出一个启发函数，并且证明它确实是 admissible 的。

这个对照有实用价值。在经典规划里，下界通常由人手工设计（松弛问题、地标法、模式数据库）。设计错了会导致搜索剪枝掉最优解，而且很难察觉。AWM 把这一步交给模型自动产出，再用 Lean 内核兜底：会不会剪错，由证明来回答，不由人肉审查回答。

第四关那次，AWM 交的是两件东西拼起来的紧界：一句"预算 18 内无解"的证明，加一份"预算 19 的通关见证"。前者证明下界 ≥ 19，后者证明上界 ≤ 19，两个加起来才是"最优恰好 19"。Astra 只交了后者，却宣布了前者的结论。

四、阶段一 · 探索：边玩边纠错的三值检查器

整套流水线分三段。第一段把每一次点击变成一条可执行假设。

Agent 在部分可观察马尔可夫决策过程（POMDP）设定下与环境交互，每一步观察像素、选择动作、接收反馈。和常规强化学习不同的是，它同时维护一本概念手册。每条经验被提炼成一段 Python 代码，论文里叫 concept，包含四样东西：

三值返回是关键设计。常规的单值校验器只有"对"和"错"，遇到适用范围之外的观测只能勉强给个结果，噪声就从这里进来。NA 让"不知道"成为一个合法返回值，规则库因此不会被迫在边界上编造结论。

配套的硬约束是：每执行完一个动作，就用新获得的转移记录重新检查所有现存 concept。任何一条被证伪或报错，探索立刻停止，必须先修订或撤回它。

这条约束把纠错的动作从"事后复盘"挪到了"边玩边改"。25 个公开游戏跑下来，团队记录了 742 条可执行概念，过程中撤回了 143 条——撤回率约 19%。

【推算】742 − 143 = 599 条概念存活进入下一阶段，最终收敛成 283 条规则，压缩比约 2.1 : 1。单游戏平均约 29.7 条概念、11.3 条规则，与论文给出的"中位数每游戏 6 个类型、10 条规则"吻合。

五、阶段二 · 凝炼：11 条压成 1 条，且不许丢反例

第二段的目标是把零散的 concept 手册压成紧凑的、带类型的世界模型。

AWM 从观察中抽出对象类型，把 concept 重写为作用在这些对象上的规则，然后用范畴论里的两类极限做变换：

概念上，投射极限对应"下定义"——把一堆已有概念和它们的关系拼在一起，共同定义一个新东西；归纳极限对应"找共性"——观察一堆不同的东西，找共同点，统一到更抽象的框架。两个方向来回倒腾，模型越压越简洁。

论文给的具体例子是 lp85 关。这关里有四类按钮机制：传送带、星形、枢纽、面板。探索阶段学出 11 条概念。泛化变换识别出四类机制本质都是对方块位置的置换，11 条合并成一条带参数的规则 press_permutes。

合并有两条硬约束，写得很实在：

1. 每次变换必须编译出对应的 Lean 辅助引理，并通过内核检查。
2. 压缩不许丢掉已经测出来的东西。 用旧规则集 S 换成新规则集 T，必须满足 T 拒绝的样本集合包含 S 拒绝的样本集合。

第二条是防"过度泛化"的闸门。泛化做过头会把反例一起泛掉，模型变得又简洁又错。团队用一组被扰动过的转移做诊断集来验：合并后的 press_permutes 保住了源概念在诊断集上的全部 55 个拒绝样本，还额外拒绝了 21 条被污染的转移。

副作用是引理数量下降。一条颜色计数不变量就能覆盖所有按钮，原来需要两到三倍的引理数量。结构收束带来的不只是可读性，还有证明成本。

六、阶段三 · 证明：220 条规则、1374 条定理、三个公理

压缩好的对象和规则被翻译成 Lean 4 定义。对象用两类极限形式化，规则用模式匹配方程写出来。从这一步起，AWM 做的不再是行为预测，而是定理证明。

Lean 侧的实际账目：

最后一行值得单独说。整个形式化只用到 propext、Classical.choice、Quot.sound 三个常量，都是 Lean 标准逻辑自带的，论文没有塞进任何一条自家公理。所有证明都是封闭的，不留未证明的占位符，也不使用绕过内核的计算。

对做形式化验证的人来说，这三条是判断一份证明"能不能当真"的第一道筛子。用了 sorry 或者自定义公理的证明，在内核眼里和一个假设没区别。

183 个关卡的通关轨迹全部能被 Lean 重放并验证。

这里有一处口径缺口要标出来：25 个游戏产出了 283 条规则，但只对 20 个世界模型做了形式化，规则数降到 220 条。剩下 5 个游戏为什么没进 Lean，论文没有说明。可能是形式化成本，可能是抽象难度，也可能是这三者之外的工程原因。这一条属于未披露。

七、数字先自洽一遍：43% 和 99.9 是怎么来的

论文给了一组容易误读的成绩。先算一遍。

动作数 43%：AWM 的认证通关轨迹共 7448 步，人类基准 17135 步。

7448 ÷ 17135 = 43.47%   → 官方口径 43%，对得上

横向对比同报告该指标的系统：Memento 3 用 7518 步，Rodionov 智能体用 8347 步。AWM 比前者少 70 步，比后者少 899 步。差距不算悬殊，差别在附带物：AWM 的每一步背后有机器检查过的证明。

平均分 99.9：这个数需要拆开看。ARC-AGI-3 用平方制计分，单关得分等于人类基准步数除以 AI 步数再平方。

单关得分 = (人类步数 / AI 步数)²
若 AI 步数 = 人类的 43%  →  单关得分 = (1/0.43)² ≈ 5.4 倍

原始值远超 100，会被截到 100。所以一旦 AI 步数低于人类基准，这一关就是满分，再省也加不上去。

实际分布是：25 个游戏中 23 个满分，其余每个至少 97.6。

【推算】按 23 个满分反推：(23 × 100 + 97.6 + x) ÷ 25 = 99.9，解得 x ≈ 99.9。也就是说剩下两个游戏里，一个卡在 97.6，另一个接近满分。这个反推与官方给出的边界一致，说明 99.9 不是"每关都略差一点"，而是"绝大多数关饱和到 100、少数关掉下来"。

结论：99.9 分和"183 关全通"基本是同一件事的两面，因为平方制下步数优势会直接顶到计分上限。真正有信息量的是那个 43%——它说明 AWM 不是靠穷举赢的，穷举在这个计分下会被惩罚得很惨。

同一批模型换到 ARC 官方标准 harness（不提供代码执行），平均分是 40.7。这个落差说明：AWM 的分数很大一部分来自"能写代码 + 能检查"，而不是底座模型本身变聪明了。

八、只给一句话反馈，界限从 20 降到 19

自我修正那段是全文最有工程价值的部分，因为它描述的是一个真实运维场景：模型给了一个结论，你知道它偏了，但不知道该改哪儿。

初始六次实验里有两次界限偏高。团队给的反馈只有一句：游戏里存在更省的路。不告诉它成本多少，也不说哪条规则错了。

第四关那次，AWM 回去检查自己的显式规则，发现踩到燃料格会顺便收集燃料，这个副作用在模型里漏了，补上之后界限从 20 降到 19，正好命中真值。第五关那次，它找到失败的真正原因是地形限制而不是射程限制，界限从 47 降到 37（它的记账约定把通关那一步也算成本，对应引擎口径的 36）。

四轮额外尝试之内，两次都拿到了新的封闭证明。

对比一下基线的表现。Claude Opus 5.5 和 GPT-6 Astra 拿到同样的反馈，仍然产不出机器检查过的证明。它们能调整自己说的数字，但调整之后的数字依旧没有依据。

这一步说明的事比原始成绩更重要：显式规则 + 机器检查，让"改错"变成一个有方向的搜索过程。 规则是写在 Python 和 Lean 里的，可以逐条读、逐条改、逐条测。改完之后能不能通过内核，是一秒钟之内就能知道的事。

如果规则藏在一个神经网络隐状态里，“界限从 20 改成 19"这种修正是没法被引导的——你只能说"再试试”，不能说"去查一下燃料格的副作用"。

九、六条证明里，一条没能迁回真实环境

这是论文里最该被反复引用的部分，也是最容易被标题盖掉的。

证明成立的前提是模型和真实环境一致。 而屏幕到状态的转换，发生在 Lean 之外的 Python 代码里。

论文自己把这件事写得很直接：模型可能比游戏本身更严格。如果抽象时加了一条环境里并不存在的限制，那么"这个目标不可达"的证明在模型里成立、在环境里却可能是假的——证明再严谨，也只是在一个错误的世界里自洽。

团队为此引入了一个叫"充分覆盖"的定义：只要模型能逐步复现环境里那条最优通关序列，模型里的不可能性证明就能迁移回真实环境。然后用引擎穷举出的转移图，逐条核对证明里的势函数不等式和不变量条件。

结果：6 条模型级证明里，5 条通过迁移校验，1 条没有。

失败率 1/6 看着不高，但意义不小。它说明这套校验不是形式主义的仪式——它真的会拦下东西。如果 6 条全过，反而要担心校验条件是不是太松。

这个结构的价值在于它把责任分清了：

最后一行的"靠人看"是这套流水线目前的真实边界。Lean 检查通过不等于自然语言层面的推理正确，这一条有独立证据：2026 年 10 月 arXiv 上另一篇论文《纳维-斯托克斯在翻译中丢失》专门讲这个坑——AI 把自然语言证明自动转成 Lean，转译本身可能在数学内容上出错，而 Lean 只会忠实地检查那个已经被转歪的东西。

AWM 的应对方式是把假设显式摊开：前提写在规则里，规则的依赖关系写在 Lean 里，出了偏差能顺着依赖图倒查回某一条具体规则。这条路更慢，但错在哪一目了然。

十、证明的依赖图本身就是调试信息

论文还测了一个很实用的问题：证明能不能帮人定位错误。

做法是往参考模型里塞一条错误规则，再让 Claude Opus 5.5 去找出模型预测与游戏不一致的那次转移。

【推算】三个百分比按 16/42、29/42、30/42 计算。

第二行是关键。把"这条结论依赖哪些规则"告诉模型，定位率从 38% 提到 69%，已经逼近直接给答案的 71%。也就是说，依赖关系携带的信息量，几乎等于答案本身。

这条结论可以直接迁到 Agent 工程上。现在大部分 Agent 出问题时，能给的只有一条执行日志和一段思考文本，人得靠猜。如果能给出"这个结论由哪几条规则推出"，排查就从通读日志变成二分查找。

反过来说，凡是 Agent 给出重要结论的场景，都值得顺手记下它的依据链——不是为了审计合规，是为了下次它错的时候你还找得到。

十一、没测的东西，和论文自己划的边界

论文的边界交代得比多数同类工作清楚，这部分不该跳过。

这几条合起来，画的是一条相当窄的适用边界：结构离散、规则稳定、反馈即时、可被形式化的世界。

好消息是，工程里这类世界比想象中多。调度器的资源约束、状态机的合法转移、网络策略的可达性、权限模型的越权路径、流水线的依赖环——这些本来就是离散、确定、即时反馈的，也正是形式化方法用了几十年的地盘。

坏消息是，机器人操作、自动驾驶、推荐系统这类连续、随机、延迟反馈的场景，短期内套不上。论文也把这一条写在了结尾：更复杂的环境和任务，才是这类形式化推理的下一个自然测试场。

十二、工程迁移：什么时候值得给 Agent 加一层证明

不是所有 Agent 都需要 Lean。判断标准可以落成一张对照表。

四条以上落在左列，才值得考虑。否则成本压不住：1374 条定理对应的是一份精简到 283 条规则的模型，形式化本身的工作量不小。

对暂时不上 Lean 的团队，这套论文里还有三个可以立刻拿走的东西，成本远低于形式化：

其一，把"估计"和"证明"在输出里分开。 Agent 说"这事不行"时，要求它明确标注这是搜索到的上界，还是推导出的下界。Astra 那个错误不是能力问题，是表述问题——它把上界当成了结论。改提示词就能拦住大部分同类错误。

其二，用三值检查器替代二值校验。 真 / 假 / 不适用，比真 / 假多一个状态。规则库遇到适用范围之外的输入时能诚实返回 NA，而不是硬给一个结论。这个改动在工程上极便宜，对减少边界噪声效果明显。

其三，压缩时守住"拒绝集单调不减"。 任何一次规则合并、抽象升级、提示词重构，都要用一组固定的失败样本回归一遍，确保新版本拒绝的样本集覆盖旧版本。这条约束在 AWM 里是用来防过度泛化的，搬到工程里就是防"改了一版反而更宽松"。

十三、关键要点

1. 上界不等于最优。 找到一条 22 步的通关路线，只能说明最优不超过 22。要断言"19 步以内无解"，需要覆盖全部路径的下界证明。这是 GPT-6 Astra 出错的地方，也是绝大多数 Agent 出错的地方。

2. 下界的唯一机制是势函数。 V(s) ≤ c(s→s') + V(s') 且 V(goal) ≤ 0，沿路径累加即得任何通关成本不低于 V(s0)。这就是 A* 里 admissible heuristic 的定义，只是这次由模型自己学出来、由 Lean 证明它成立。

3. 三阶段流水线各有一道闸门。 探索阶段靠三值 checker 边玩边证伪，742 条概念撤回 143 条；凝炼阶段要求每次变换编译出 Lean 引理，且拒绝集单调不减；证明阶段不留 sorry、不引自定义公理，只用 Lean 自带三个常量。

4. 结构收束会降低证明成本。 lp85 关 11 条概念泛化成 1 条 press_permutes，保住 55 个拒绝样本、额外拒绝 21 条污染转移，引理数量降到原来的三分之一左右。抽象不是为了好看，是为了少证明。

5. 99.9 分和 43% 是同一组数据的两个切面。 平方制计分下，步数低于人类基准即饱和到满分，所以 99.9 与"183 关全通"高度重合。真正有信息量的是 7448 步对 17135 步的 43%。同一批模型去掉代码执行后降到 40.7 分，说明分数来自"能写代码 + 能检查"。

6. 证明的依赖图约等于答案。 给出"结论依赖哪些规则"后，错误定位率从 38.1% 提到 69.0%，逼近直接告知答案的 71.4%。这条比成绩更有工程价值。

7. 前提一致性是最大风险，而且会真的失败。 Lean 只检查模型内的推导，屏幕到状态的抽象发生在 Lean 之外。6 条模型级证明里 5 条通过充分覆盖校验，1 条没有。校验条件不是仪式。

8. 适用边界很窄但很实在。 离散、确定、即时反馈、可抽象为类型的系统。调度约束、状态机、策略可达性、权限越权路径落在里面；机器人操作、自动驾驶、推荐系统还在外面。