十月三十日，一篇题为代数世界模型的论文挂上arXiv，作者来自清华大学交叉信息研究院，指导教师是图灵奖得主姚期智与副教授袁洋，两位共同第一作者都是本科生，一位来自浙江大学、目前休学在清华做研究，另一位来自清华姚班。论文做的事听起来有点复古：让AI从与陌生环境的交互里，提炼出可以用数学描述、可以证明的规律。团队把它称为代数世界模型，简称AWM。
测试集是ARC-AGI-3，一套以“抽象与推理”为核心的交互式基准，共一百八十三关。基于Opus 5的AWM全部通关，得分百分之九十九点九，平均通关动作数为人类基准的百分之四十三。这个数字比通关率更有信息量：它说明模型不是靠穷举试出来的，而是用更少的动作找到了规则。
面对被人为设置为无解的关卡，基于Opus 5.5的AWM还能在两次尝试后证明“此路不通”，并进一步判断只需增加一步即可获胜。这个能力在游戏里像炫技，在工程里却是刚需。真实世界的调试大多是排除法，能证明某条路走不通，比多试几次更有价值。
把成绩放回上下文，会看到它与主流路线的区别。多数世界模型在像素或潜空间里预测下一帧，评价标准是画得像不像、物理合不合理。AWM不生成画面，它生成的是规则。团队的说法是，世界模型的计算成本不再随分辨率线性膨胀，“理解”第一次有可能脱离“生成”。
具体做法分三步：探索、凝炼、证明。探索阶段，模型在环境里试动作、收集观察，把看到的现象写成可执行的Python假设。凝炼阶段，把这些零散的假设不断合并、简化，去掉冗余与矛盾。证明阶段，把凝炼后的规则形式化为Lean 4断言，交给证明助手校验。三段循环，直到规则能解释所有观察。
合并与简化的工具借自范畴论，用了两个概念：投射极限与归纳极限。前者是“下定义”，把一堆已有概念和它们的关系拼在一起，共同定义一个新东西，相当于分解与组合；后者是“找共性”，观察一堆不同的东西，找到共同点后统一到更抽象的框架里，相当于泛化与特化。两种操作来回倒腾，假设会越来越简洁、一致。
这个思路的参照物是科学史。牛顿面对的不是一道写好答案的题，而是大量零散观测；他的贡献是从现象里找出“力”“质量”这几个核心概念，再把它们组织成可推演、可检验的体系。AWM想教给模型的就是这套工作方式：先造概念，再造定律，最后做证明。
值得注意的是它对基座模型的依赖。论文里的成绩基于Opus 5与Opus 5.5，说明AWM是一层方法论外壳，而不是一个新模型。换一个更弱的基座，写假设与做归纳的质量会下降。这既是它的优势（可以直接受益于基座升级），也是它的限制（无法脱离强模型独立工作）。
“证明此路不通”这件事，在技术上比通关更难。通关只需要找到一条可行路径，证明无解需要论证所有路径都不可行。后者要求模型对环境的规则有完整把握，而不是局部拟合。AWM能做到，靠的是把规则形式化之后交给Lean 4去验证：一旦规则集合足够完备，无解就可以被推导出来。
这也暴露了它的边界。团队自己写得很清楚：证明是基于“观测到的世界”成立的。如果探索得不够全面，遗漏了某些关键规则，那么模型描绘的只是一个局部真理，而不是完整的世界。在这种情况下，“证明无解”可能只是“在我的模型里无解”。
所以要理解成一个循环：观察、假设、实验、抽象、证明，然后再回到观察。每一轮循环都在扩大观测覆盖，同时收紧规则集合。这个循环在游戏里可以自动跑，在真实世界里需要一个能设计实验的执行者，这也是它走向物理世界的第一道门槛。论文里通关的一百八十三关全部是离散、可重置的交互环境，这类环境天然适合形式化描述；一旦进入连续、不可逆的物理系统，规则该怎么写、观测该怎么离散化，本身就会成为新的难题。
把AWM与同期的其他世界模型放在一起，会看到一条清晰的分岔。一条路继续在像素与潜空间里做生成，追求画面的真实度与交互的实时性，代表是各类视频世界模型与机器人仿真器。另一条路放弃生成，只在符号层面建模规则，追求可推理、可验证、可迁移。AWM属于后者。
两条路的成本结构完全不同。生成路线的算力随分辨率与时长线性增长，做长时推演很贵；符号路线的前期成本在“把现象翻译成假设”这一步，一旦规则成型，推演几乎不花算力。前者的产出是给人看的画面，后者的产出是给机器用的模型。
有意思的是，同一天前后，西湖大学也在杭州揭牌了世界模型研究中心。据公开信息，该中心由长期做自动驾驶与世界模型的团队支撑，二〇二四年底转向在隐空间表征物理概念的“概念世界模型”，两条路线在同一周出现，说明“世界模型”这个词已经被拆分成了至少两种东西。
对产业来说，这个分岔意味着选型要更谨慎。如果需求是生成训练数据、做仿真环境，像素路线更直接；如果需求是让机器人在陌生环境里快速建立可用模型、并能解释自己的判断，符号路线更合适。分不清这两层，就很容易把“画面很像”当成“理解正确”。