姚期智团队新作：代数世界模型
假设一个游戏关卡，AI尝试了很多次都没能通关。它究竟是还没找到解法，还是给定的行动次数根本不够？前一个问题只要找到任意一条获胜路线就能回答，但要证明无解，就必须排除所有合法路线，包括那些尚未尝试过的路线。如果游戏连规则都不公开，AI还需要先弄清自己究竟在证明什么。通关和证明无解，难度完全不同。
图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队提出的“代数世界模型”（Algebraic World Model，AWM），正是要把与陌生环境的交互转化为支持形式化推理的显式数学模型。论文作者包括姚期智教授、清华大学交叉信息研究院副教授袁洋等人，两位共同第一作者均为本科生：一位是休学在清华大学做研究的浙江大学学生潘冠成，另一位是清华姚班的谭淇心。
一条获胜路线与一份无解证明之间隔着什么
传统形式化推理通常从预先给定的数学定义和规则出发。AI做的事情，是在一个设计好的形式系统内部搜索答案。黎曼zeta函数相关的Lean验证进展、纳维-斯托克斯问题的部分形式化结果，都建立在这个前提之上：人类已经把问题空间、定义系统和证明目标全部给定。
但把AI扔进一个完全陌生的交互环境，情况就变了。没有规则手册，没有形式定义，连状态空间都要从像素里猜。AI能不能自己观察、自己假设、自己压缩成紧凑模型，最后写出机器可检查的定理？这是AWM试图回答的问题。
AWM的核心，是把经验观察与证明所依赖的前提连接起来。它需要从陌生环境中主动发现数学结构，并在后续交互中不断检验和修正学到的规则。这与牛顿面对零散观测数据、从中提炼“力”和“质量”等核心概念、再组织成可推演可检验理论体系的工作方式有相似之处。
把每一次点击写成可执行假设
AWM的运行分为三个阶段，整个过程从探索试错走向建模和形式化证明。
- 探索与原型。 Agent在部分可观察马尔可夫决策过程（POMDP）设定下与环境交互，每一步观察像素、选择动作、接收反馈。与传统强化学习不同，AWM同时维护一本概念手册，把看到的现象写成可执行的Python代码，作为初步的“假设”或“规律”。
- 凝炼。 用新的观察去验证、修正这些假设，再把它们提炼成更通用的对象和规则。这些规则被组织成数学模型，成为后续推理的骨架。
- 证明。 把规律形式化成Lean 4语言，变成逻辑严密、机器可以自动检查的数学断言，最终构造可由Lean内核检查的形式化证明。
借助这套方法，AI不仅能够回答怎样获胜，还能证明在给定约束下为什么无法获胜。其意义在于让AI的推理覆盖尚未探索过的行动序列，同时让结论所依赖的假设变得清晰、可检查。当模型与真实环境出现偏差时，系统还可以追溯证明所依赖的具体规则，通过进一步探索修正模型。
六次运行全部通过Lean内核检查
团队在ARC-AGI-3上检验了这种不可达推理能力。这些游戏不预先公开规则和目标，玩家只能自己摸索。研究者以sc25的两个关卡为基础，保留机制，将行动预算设置为略低于最低获胜成本，构造出两个无法在预算内通关的变体。每个关卡运行三次，AWM在全部六次运行中都构造出了通过Lean内核检查的封闭证明，在所学模型下排除了预算内所有合法获胜序列。
作为对照，团队报告，配备编程工具的Claude Opus 5.5和GPT-6 Astra在合计十二次基线运行中，均未产生这类证明。这说明在“证明某条路走不通”这一任务上，能够写代码、能够试错的通用智能体与形式化不可达推理之间仍存在明显距离。
第4关的19步与Astra的22
证明通过检查，并不等于系统学到了完全正确的环境规则。AWM最初六次运行给出的获胜成本下界中，四次与真实最低成本相符。Opus 5.5有一次给出正确界限，但没有附上证明；Astra则没有给出正确界限。其余基线运行存在界限错误或未得出结论的情况。
一个具体例子发生在第4关。GPT-6 Astra声称最低获胜成本为22，但未提供证明。AWM则在所学模型下证明了19的紧下界，并验证了一条成本为19的获胜路线，与游戏实际最低获胜成本一致。这个对比恰好说明，仅给出一个数字和给出一个经过内核检查的紧界，是两种不同性质的结论。
局部真理：证明再严谨也依赖抽象前提
AWM也划出了自己的边界。目前其验证环境都是离散动作、即时反馈、完全可观察的POMDP；延迟奖励、部分可观察、随机转移这些更接近真实世界的场景还没有测试。更关键的是，Lean证明的正确性完全依赖模型抽象出来的前提是否与真实环境一致。前提错了，证明再严谨也只是在一个错误世界里自洽。
因此，AWM描绘的可能只是“局部真理”，而不是完整的世界。真正的路径是一个不断循环的过程：观察、假设、实验、抽象、证明、再观察。当探索不够全面、遗漏了某些关键规则时，系统需要回到环境中继续修正模型。
从经验探索到数学建模，再到形式化证明，AWM为AI在未知环境中开展严谨推理提供了一条新的技术路径。过去世界模型研究的终点是一个能预测下一步的神经网络，AWM把终点往前推了一步：让世界模型本身变成可形式化、可证明、可追溯的数学对象。AI不再只是在人类给定的公理体系里解题，而是开始自己发现公理、压缩公理，再在自己构造的公理体系里写证明。
