独家｜姚期智下场做世界模型： AI 在陌生 游戏 里自己写数学证明

就在刚刚，计算机大牛、中国科学院院士、清华大学教授姚期智发表了一篇新研究论文。

这次不是一个理论内容，而是一个真正的代数世界模型（Algebraic World Model）。

实际上，现在的大模型在数学证明上已经走得很远。

近期，Anthropic 报告了 Lean 验证的黎曼 zeta 函数相关进展；而OpenAI团队宣称在纳维斯托克斯千禧年问题上取得了部分形式化结果。

但是，这些工作有一个共同前提，就是人类已经把问题空间、定义系统和证明目标全部给定。AI 做的事是在一个设计好的形式系统内部搜索答案。

那么，如果把 AI 扔进一个完全陌生的交互环境呢？

没有规则手册，没有形式定义，连状态空间都要从像素里猜。AI能不能自己观察、自己假设、自己压缩成紧凑模型，最后写出机器可检查的定理。

这就是清华大学交叉研究院和浙江大学团队这篇论文提出的问题。论文提出的框架叫代数世界模型，缩写 AWM。

作者包括姚期智教授、清华大学交叉信息研究院副教授袁洋等人。

我们简单分析一下这篇论文，姚院士到底要向学术界讲怎样一个新故事？

第一阶段：把每一次点击变成可执行假设

AWM 的运行分三步：

第一步叫探索与原型。

Agent 在一个部分可观察马尔可夫决策过程设定下跟环境交互，每一步观察像素、选择动作、接收反馈。跟传统强化学习不同的是，AWM 同时维护一本概念手册。

每一条经验被提炼成一段 Python 代码，论文里叫 concept。每个 concept 包含自然语言解释、适用条件、一个 checker 函数和一个可选的 predictor。

Checker 的作用是快速证伪。给定一条观察 x，如果跟 concept 矛盾就返回假，如果不在适用范围内就返回 NA。

Agent 每执行完一个动作，就用新获得的转换记录重新检查所有现存 concept。矛盾的 concept 必须立刻修订或撤回，否则探索不允许继续。这个设计把发现错误从事后复盘变成了边玩边纠错。

经过足够多轮交互，Agent 手里攒了一批 Python 函数。这些函数各自解释一部分观察到的转换，但它们之间可能重叠、可能冗余、可能在边界条件上冲突。它们是草稿，不是模型。

第二阶段：范畴论把草稿压成公理

第二阶段叫结构与简化。

目标是把零散的 concept 手册压缩成一个紧凑的、带类型的世界模型。AWM 从观察里抽出对象类型，把 concept 重写为作用在这些对象上的规则，然后用范畴论里的两类极限做变换。

投影极限方向做分解和复合两件事：分解是把一个复杂规则拆成更简单的组件规则，对应整体到部分；复合是把多个已验证的简单规则拼成一个组合规则，对应部分到整体。

归纳极限方向也做两件事：泛化是从多个具体案例里抽参数化的通用规则，特化是把通用规则细化成绑定了具体参数的案例规则。

论文里举了一个 1p85 关卡的例子。这个游戏里有四种按钮机制，第一阶段 Agent 学出了十一条 concept。

而通过泛化操作，十一条被压缩成一条共享规则，按下按钮的颜色等于面板颜色的变换函数。

每一次变换都伴随一个 Lean 辅助引理，由内核检查兼容关系。硬约束是压缩不能丢掉已发现的反例。压缩后的模型必须覆盖所有被记录为失败的转换。

第三阶段：在 Lean 里证明这关赢不了

第三阶段叫形式化与证明。

压缩好的对象和规则被翻译成 Lean 4 定义。对象用投影极限和归纳极限形式化，规则用模式匹配方程写出来。

从这一刻起，AWM 做的不再是行为预测，而是定理证明。

它证两类命题。

第一类是可达性，存在一条合法动作序列从初始状态到达目标状态。第二类是不可达性，在给定预算 B 下不存在任何合法序列能到达目标。后者难得多，因为它要求排除所有可能路径，包括那些从未被探索过的分支。

实验最硬的证据在 sc25 关卡。

这个游戏里方块在网格上移动，通过一个三乘三面板施放咒语到达出口。移动和点面板各花一个单位成本，施放咒语多花一个单位，燃料回复花费十个单位，完成最后一步获胜动作免费。团队把两个关卡的预算压到最小获胜成本以下，得到两个不可能关卡。

AWM 跑了六次独立实验，六次都构造出封闭的、内核检查过的 Lean 证明，严格排除了预算内的所有合法获胜序列。

对照组 Claude Opus 5.5 和 GPT-6 Astra 在相同设定下跑了12次，没有一次产出这种证明；在第四关，AWM 形式化证明最小获胜成本是十九，预算只有十八，因此必输。

GPT-6 Astra 在单次实验内尝试八次后声称存在一条成本22的获胜路径，这个声明既没有证明支撑，也跟真实最优解对不上。

经过反馈修正后，AWM 六次实验下的信息全部正确。Opus 5.5 和 GPT-6 Astra 即使拿到同样的反馈，也无法产出机器检查过的证明。

学到的是带证明的世界模型

在 ARC-AGI-3 的25个公开关卡上，AWM 用 Claude Opus 5.5 作为底层模型，得分 99.9，认证通关二十三个关卡，总动作数 7448，是人类基线动作数的 43%。

对比 Memento 3 的 7518 动作和 Rodionov 智能体的 8347 动作，AWM 在更省动作的同时还附带了机器检查过的证明。

Lean 形式化的结果更能说明问题。25个关卡中学到的二十个世界模型，在 Lean 里形式化为 220 条规则，对应 1374 条定理，公理只用到了 propExt、Classical、choice、Quot 和 sound 这几个标准逻辑常量。183 条已记录的获胜轨迹全部能被 Lean 重放并验证。

论文自己也划了边界。

目前，其验证环境都是离散动作、即时反馈、完全可观察的 POMDP。延迟奖励、部分可观察、随机转移这些更接近真实世界的场景还没测。

Lean 证明的正确性完全依赖模型抽象出来的前提是否跟真实环境一致。前提错了，证明再严谨也是在一个错误世界里自洽。

但这条路径的意义是清楚的。过去世界模型研究的终点是一个能预测下一步的神经网络。

AWM 把终点往前推了一步，让世界模型本身变成可形式化、可证明、可追溯的数学对象。

AI 不再只是在人类给的公理体系里解题，而是开始自己发现公理、压缩公理、再在自己造的公理体系里写证明。