七座桥与两个打不通的关卡

🌉 一、从哥尼斯堡说起

1736 年的普鲁士小城哥尼斯堡，普雷格尔河穿城而过，河心有一座岛，河上架着七座桥。市民闲暇时玩一个游戏：能不能一次走遍所有七座桥，每座只走一次，最后回到起点？

很多人试过很多次，都失败了。但"试了很多次都失败"不等于"不可能"——也许只是你不够巧。

欧拉做了件截然不同的事。他没有继续试走，而是把每块陆地缩成一个点，把每座桥缩成连接两个点的一条边，然后指出：一次不重复地走完所有桥的路径，要求每个点连接的边数是偶数——进一次就要出一次。哥尼斯堡有四个点，个个连着奇数条边。论证完毕，问题终结：你们要找的路，不存在。区别很微妙，也很致命——"我们还没找到"与"这样的路根本没有"，是两种完全不同的知识。

这就是数学史上最漂亮的"不可能性证明"之一。论文《Algebraic World Model》正是从这座小城开场的。作者想追问一个比"AI 会不会解数学题"野得多的问题：

如果一个智能体降临在一个规则完全未知的世界里——没人告诉它公理、定义和形式化规格——它能不能一边摸索这个世界，一边对这个"没人写过说明书"的世界，给出严格到经得起机器内核检验的证明？包括"这件事做不到"的证明？

⛰️ 二、"证明做不到"为什么比"证明能做到"难一个档次

先建立一个朴素的分野。

要证明"做得到"，你只需要出示证据：走一条路线给大家看。这条路存在，结论就成立。数学里管这种证据叫见证（witness）：找到一个就够了。

要证明"做不到"，事情麻烦得多。你不能说"我试了一千次都失败"，因为第一千零一次可能成功。你必须堵死所有可能的路径，而且不能靠试，得靠论证：任何一条满足规则的动作序列，都必然撞上同一堵墙。

放到优化问题上，这叫上界和下界的分野。我构造出一个成本 19 的方案，就证明了"最优成本不超过 19"——上界，一个例子就够。而要断言"最优成本至少是 19"，我必须论证每一个成本不超过 18 的方案都不存在——下界，要覆盖整个解空间。上界是存在性问题，下界是全称性问题；前者只需要一个聪明的朋友，后者需要一套滴水不漏的系统。

数学竞赛有条经验：给下界的题目永远比给上界的难出一个档次。AI 也一样。生成式模型天生是见证搜寻器——给它一个目标，它穷尽语料里的花样给你编一条看似可行的路；让它诚实地说"这条路在所有平行宇宙里都不存在"，需要的是另一副器官：一套能穷尽枚举、逐步核验、不许偷懒的外置纪律。这恰是多数 AI 系统缺的那块骨头。

这些年 AI 在数学证明上突飞猛进，Lean 形式化的定理越堆越高，关于千禧难题的传闻不时刷屏。但这些成就都有一个安静的共同前提：定义是人事先写好的。有人告诉 AI 什么叫群、什么叫拓扑空间、目标命题长什么样。AI 是在一个已经公证过的操场上跑步，跑得再快，跑道是别人画的。

AWM 想撤掉这个操场。让世界自己开口，让智能体在荒野里自己立法——并且立到能宣判"此路不通"的程度。

🎮 三、实验场：连说明书都不给你的游戏

测试野心的场地叫 ARC-AGI-3。玩法一句话说清：一个小网格世界，里面有按钮、传送带、燃料、门、子弹，但规则和目标都不告诉你。你得通过试玩搞清楚：按这个按钮会发生什么？吃什么能补行动预算？走到哪算赢？

它几乎是"未知世界"的极简化身。没有形式化规格，没有教科书，连"这是一道数学题"的提示都没有。相当于把欧拉空投到哥尼斯堡，不告诉他有七座桥，只让他自己坐船逛。

姚期智团队（清华大学、上海期智研究院，联合浙江大学）在这片场地上搭起一个三阶段框架，取名 AWM（Algebraic World Model，代数世界模型）。三个阶段各对应一件做科学也做的事：先观察记笔记，再整理归档，最后写成可证明的定理。

📓 四、第一阶段：一本不许带矛盾的野外考察笔记

想象你是博物学家，第一次踏进一片雨林。第一条纪律是什么？做笔记，而且做老实笔记。

AWM 的第一阶段叫探索与原型（Explore & Prototype）。智能体在环境里乱逛：按按钮、走格子、吃东西。每摸到一点规律，就往一本"概念书"（concept book）里添一条概念。

每条概念是一条可执行的 Python 假设，四个零件：一段自然语言断言（"燃料可以增加行动预算"）、一个适用域（这条规律管哪些格子）、一个检验器（checker，吃进一条观测到的状态转移，吐出真、假或不适用）、可选一个预测器（告诉你转移之后应该看到什么）。

关键在"可执行"三个字：概念不是写在纸上给人看的散文，是能跑的代码，会在之后每一次新观测上持续接受审判。

然后是全文最狠的一条规矩，论文里叫门禁（gate rule）：

只要任何概念在任何一条已记录的转移上被判 FALSE 或报错，整个系统拒绝继续探索。先修正，或撤回这条概念，才许往前走。

翻译成博物学家的语言：笔记里只要发现一处与事实对不上的记载，立刻停笔，不许再往深处走，先回去把那条改对，或者划掉。

多数机器学习系统不这么过日子。模型里留着互相矛盾的碎片没关系，准确率掉零点几个点没关系，继续训。大语言模型更是如此——上下文里同时躺着两句互相打架的话，它照样面不改色地接着写。AWM 反着来：带着矛盾不许前进。理由也直白——这套笔记最终要拿去盖证明的大厦，笔记里混着一句假话，大厦就是沙雕。

门禁的触发往往无声无息。比如概念书写下"按下按钮，传送带移动一格"，某次新观测里传送带却跳了两格——检验器吐出 FALSE，红灯亮起，整个探险队原地立正，回头改笔记。实验里，概念书在 25 个游戏上累计登记 742 条可执行概念，其中 143 条在门禁前被撤回。撤回算不上污点，更像纯度证明：每一条被划掉的假规律，都曾在一个具体时刻拦住了系统迈向错误。带着 143 次停笔的记录走到终点，比一路绿灯更让人放心。

🗄️ 五、第二阶段：给文件柜合并重复档案

笔记记多了，新问题浮出水面：乱。

同一个按钮，你在三个关卡各写一条概念，说的其实是一回事；七条关于"传送"的笔记，本质共享同一条规律。概念书此刻像一间堆积如山的办公室，每个抽屉都塞着内容重叠的档案。

第二阶段结构化与简化（Structure & Simplify）就是请来一位极客档案管理员，把零散概念整理成"类型化的对象 + 共享规则"的紧凑模型：先归出这个世界一共有多少种"东西"，再归出这些"东西"之间一共有多少条通用规律。

合并同类项靠什么指引？论文用了一件略显豪华的工具：范畴论（category theory）。读者不必真懂它，把它想成一门"专门研究什么东西本质上相同"的数学语法就行。它给出四个方向的变换：

• 投影极限方向：把一个大概念分解成部件，或把部件组合成整体。好比把一台复杂机关拆成齿轮、弹簧、杠杆，看清每个零件再装回去。
• 归纳极限方向：把几条近似的规则泛化成一条更抽象的规则，或反过来把抽象规则特化到具体情形。好比从"猫会呼吸、狗会呼吸"泛化出"哺乳动物会呼吸"，再特化回"这只猫会呼吸"。

而且每一次变换都不许"看着差不多就合并"。每一步都要编译出一个 Lean 辅助命题——验证一个锥（cone）、余锥（cocone）或某种泛性质（universal property）——交给 Lean 内核逐项检查。铁律同时生效：已检验的拒绝记录必须完整保留，写作 Rej(T) ⊇ Rej(S)：新模型拒绝的东西，必须包含旧模型拒绝过的一切。

合并听着轻巧，实则危险。两条规则在已见过的数据上表现一致，不代表它们对未来一致——"所有观察到的天鹅皆白"合并成"天鹅皆白"，只要一只黑天鹅就崩盘。所以每一次合并都要拿出数学证据：泛性质证明合并后的对象在所有相关场合与原对象行为等价，Lean 内核逐项核验。而 Rej 记录则是另一道保险——即便合并后的规则在新数据上翻车，旧规则曾经拒绝过的那些案例也必须仍被拒绝，系统不至于把抓过错的那只手一并砍掉。

档案可以合并，那些曾经帮你抓到过错误的旧标签，一张都不许丢。

lp85：一场四个按钮的合并手术

论文给了一个漂亮案例，游戏编号 lp85。概念书里最初有 11 条概念在描述 4 种按钮机制——传送带、星星、枢纽、面板，各写各的。范畴论引导的泛化变换出手，11 条合并成一条参数化规则：press_permutes，"按下按钮，会按某种方式置换元素"。

效果立竿见影：诊断集上，原有 55 条拒绝记录全部保留，还新增 21 条拒绝——合并后的模型抓错能力不降反升；后续要证明"某局面不可解"时，所需引理（lemma）数量减少 2 到 3 倍。描述越本质，证明越短。

最后他们用游戏引擎的派生图——7,500 个构型、52,500 条转移——完整验证了一遍：这条合并出来的规则，对游戏真的成立。

📜 六、第三阶段：把模型写成定理

第三阶段形式化与证明（Formalize & Prove），把整理好的模型搬进 Lean 4——当今最硬的交互式定理证明器之一——然后做两类证明。

第一类是可达性（reachability）：证明"从 A 状态能到 B 状态"。做法是在模型内部构造一条具体路径，Lean 逐步验证每步合法。这是见证式证明，找一条路给大家看。

第二类是全文的重头：不可能性（impossibility）。两种武器。

其一，不变量（invariant）：找一个在一切合法动作下都保持不变的量，而目标状态不满足它。比如"无论怎么按按钮，红色格子数的奇偶性永远不变"，而赢面要求奇数——排除。

其二，势函数（potential function）：给每个状态算一个分值 V，把它想成导航软件里那句"从这里到目的地至少还要开四十三分钟"——一个保守的剩余成本估计。要求它对任何动作都满足

V(w) ≤ cost(w, a) + V(w′)

意思是：从 w 出发走任何一步，这一步花的成本加上下一状态的剩余估值，怎么也抵不掉 V(w) 本身。估计只会随着行走变得更诚实，绝不会突然缩水。这是条压缩成不等式的"能量守恒"。如果起点的估值 V(w₀) 已经大于预算，那就严格证明了：预算之内不可能赢。

这句话的分量值得停一停：它没有枚举任何走法，却给整个解空间判了死刑。穷举是挨个查房，势函数是直接在门口宣布：这栋楼的地基撑不起超过十八层的任何方案。

所有证明必须封闭（closed）：不许有 sorry——Lean 里"这里先欠着"的占位符——不许用 native_decide 这类让编译器替你拍脑袋的旁门。每一行都得过 Lean 内核的机械检查。对自己的狠，到这一层抵达顶点：证明里不许有"差不多得了"。

🗺️ 七、充分覆盖：地图不必画下每条小巷

一个疑问此刻必然冒出来：你在模型里证了不可能，凭什么对真实世界成立？模型只是观察的压缩，万一真世界藏着一条你从没见过的转移，恰好能破局呢？

论文的回答是全篇最精妙的一个定义——充分覆盖（sufficient cover）：

学到的模型只要复现环境里所有最优的获胜序列，模型内的不可能性证明就能转移到真实环境。

换成地图的语言：你想证明"在预算内到不了机场"。你不需要画下全城每条小巷，只需要保证所有可能在预算内到达机场的路线都出现在地图上。地图上不存在缺失的近路，"到不了"的结论就对真实城市成立。

为什么只要求覆盖"最优"序列就够？因为下界证明排除的是廉价方案。一条绕远的路、一条死路，本来就花不起预算，它们不存在与否撼动不了"预算内到不了"的结论。真正要紧的只有那些贴着预算边走的捷径——每一条都可能成为翻盘见证。把地图上的它们全部画准，其余的模糊地带随它去。

这个条件比"覆盖一切转移"弱得多，也聪明得多。下界证明只关心最优序列；非最优的弯路、死路，漏掉一些无伤大雅。它把"学一个世界"的难度，从"学会一切"降到"学会一切最优可能"——闸门从全知收窄到了够用。

📊 八、成绩单：通关只是副产品

先看硬分数。ARC-AGI-3 的 25 个公开游戏、183 个关卡，AWM 加持的 Claude Opus 5 全部通关，得分 99.9。对照组：同一个 Opus 5 在官方 harness 下不带框架、不跑代码，只有 40.7。

更夸张的是效率：认证通关轨迹一共只用 7,448 个动作，是人类基线 17,135 的 43%——这是报告过该指标的系统中最少的。它不只通关了，还近乎贴着最短路径通关——说明真懂了规则，不是瞎蒙出来的。

模型有多紧凑？全部整理完：170 个对象类型、283 条规则；摊到每个游戏，中位数只有 6 个对象类型、10 条规则。一整个未知世界，被压缩成十行上下的法则。Lean 把这 183 关的获胜轨迹逐步回放，步步核验无误。

泛化同样过硬。把 lp85 和 ft09 的模型冻结——不再学任何新东西——丢到从未见过的屏幕上：对 4,160 个新布局的预测全部正确；对刻意改动过机制的 4,031 条转移全部拒绝。它没有把学来的规律乱用到不适用的地方。另一个游戏 ls20 上，简化后模型的接受率从简化前的 67%–70% 提升到 99.47%–99.95%。

🔒 九、封印关卡：把门焊死，然后证明钥匙不存在

现在进入全篇高潮，我称之为"封印关卡"实验。

研究者选了游戏 sc25 的第 4、5 关，元素重排，机制不动，然后把行动预算焊死：第 4 关预算 18，第 5 关预算 35。引擎穷举验证过，这两关真实的最低获胜成本分别是 19 和 36——真的不可能赢。但这一点不告诉任何智能体。

任务只有一句：请证明"预算内赢不了"。

结果一边倒得让人窒息。

AWM 六次运行，六次全部交出封闭的、经 Lean 内核检查的不可能性证明——在学到的模型内部，排除了预算内一切合法获胜序列，包括探索中从未见过的那些。

Claude Opus 5.5 与 GPT-6 Astra 十二次运行，零证明。两个基线都带着编码工具，可以自己搭模拟器、自己搜索。它们交出来的，全是"我试过了，不行"的口吻——翻遍口袋宣布钥匙不存在。

初始的"下界猜测"（你估计最低要多少步）准确度：AWM 4/6 正确；Opus 5.5 仅 1 次，还自承"手数最短路径是假设、未检查"；Astra 0 次。

最刺眼的对比在第 4 关。Astra 找到一条 22 步的路线，就断言"22 即最优"，顺手把 19、20、21 步错误排除。AWM 给出严格下界 19，并构造 19 步的见证亲自走通——与引擎穷举一字不差。一边是"我找到一条 22 步的路，所以更短的不存在"；一边是"我证明任何 18 步以内的路都不存在，且这是 19 步的路"。前者是经验，后者是数学。

一句反馈引发的翻盘

实验没完。研究者故意使坏：只丢给 AWM 一句反馈——"存在更便宜的赢法"。不告诉最优值，不告诉哪条规则错了，不给看那条路线。

这是对纠错本能的压力测试，而 AWM 的反应像极了收到审稿意见的研究者：回头重审显式规则，设计新的交互实验去测可疑概念，定位错误，然后重建证明。

第 4 关，它挖出被自己漏掉的机制："长到燃料上就会收集燃料"——燃料不必主动去拿，站在生长路径上就能捡到。第 5 关，它承认真正挡下射击的是地形，而非射程。

细节不同，动作同构：回看笔记 → 设计实验 → 修正概念 → 重走证明流水线。修正的入口也五花八门：有时重新读自己写下的显式规则，有时干脆回到环境里再做几次受控实验，让新旧观测当面对质。六次运行的界猜测，最终全部修正为正确。

严谨的含义在此显形：严谨不是不犯错，是犯了错，有机器逼着你改到对为止。这句话从流程里长出来，比任何口号都硬。

🔍 十、证明的副产品：一张现成的审计清单

实验还留下一件副产品，行业价值或许比主实验更大：证明依赖审计。

往参考模型注入一条错误规则，让 Opus 5.5 找反例，三档提示逐级加码：只给模型加证明，42 次成功 16 次；附赠"证明用到哪些规则"的依赖列表但不点破哪条错，成功 29 次；直接告诉哪条错，成功 30 次。

看出门道了吗？**给出证明依赖，几乎等于直接告知错误位置。**证明在证命题的同时，自动生成一份"本结论对哪些前提敏感"的审计报告。AI 系统越做越复杂的年代，这种"论证结构即调试接口"的性质，可能比证明本身还值钱。

补一笔转移性核验：六个模型级不可能性证明里，5 个经引擎派生图证书检查，确认可转移到原游戏——模型内部的严格，落地为真实世界的严格。

⚖️ 十一、诚实的边界

夸完，说几句冷静的。

这套框架目前最强的表现集中在网格游戏这类离散、规则有限的世界里。连续物理、开放环境、规则随时间演化的场景，概念书维护得动吗？论文没回答。成本问题同样没说透。概念书要维护七百多条可执行概念，每一阶段都要 LLM 反复生成、检验、返工，Lean 证明更是按行烧算力。这套流水线在游戏尺度上成立，搬到更大的世界，预算会不会先破产，需要后续工作回答。此外"充分覆盖"这个条件本身在一般情况下不可判定——你怎么知道自己的地图覆盖了所有最优路线？AWM 的对策是让 Lean 把守每一步，用机械检查替代"我觉得差不多"，但覆盖性的论证终究依赖探索的充分，这一点框架替不了你。

也别忽略：写概念、设计实验、发起泛化合并的，仍是底层的大语言模型。AWM 给它套上一层"必须自洽"的紧箍咒，把直觉关进可检验的笼子。笼子很硬，但关进去的仍是那只猴子——只不过如今猴子每说一句"我觉得"，都得附一段能被内核打脸的代码。

这条"先约束、后推理"的路线，与三部曲另两篇构成对话：一篇讲记忆，让系统记得自己犯过的错；一篇讲协作，让多个智能体的知识合并成社会性的科学。合起来回答同一个问题：AI 能否从预测下一个词，走到像科学家那样工作——观察、建模、证明、纠错、积累。本篇负责"证明"这一环，而且专挑最难证的那种命题。

🌉 十二、回到那座桥

两百多年前，欧拉没有走遍哥尼斯堡每一条街。他坐在岸边，把桥画成线，把陆地画成点，然后对全城宣布：别找了，你们要找的路不存在——并且给出任何人都能逐步核验的论证。

今天的 AWM，把这件事搬进了一个连规则都不肯告诉它的游戏世界。它先老实探索、记笔记，接受门禁的拷打；再把笔记归档成最简的代数结构，每合并一次都过机器内核；最后，对着两个被焊死预算的关卡，交出六份没有 sorry 的不可能性证明——在人类语言模型十二次尝试全部空手而归的同一个考场上。

"找不到"与"证明不存在"之间，隔着整个数学。前者靠运气，后者靠纪律：一套不许自己骗自己的纪律。

欧拉当年证明的是，这座城没有那样的桥。AWM 证明的是：这个智能体，配得上做欧拉的活儿。

【参考文献】
Pan, G., Tan, Q., Yuan, Y., & Yao, A. C.-C. (2026). Algebraic World Model: From Exploration to Proofs. arXiv:2610.40503. https://arxiv.org/abs/2610.40503

#论文 #arXiv #AI #小凯