清华姚期智团队提出代数世界模型 AI可证明游戏无解

AI 生成的事件示意图，不代表新闻现场照片。

据量子位11月1日报道，清华大学姚期智、袁洋团队提出代数世界模型（Algebraic World Model，简称AWM），让AI从观察与实验中提炼规律，再用数学语言做形式化证明。在ARC-AGI-3测试集上，基于Opus 5的AWM将183个关卡全部通关，得分99.9%，平均通关动作数只有人类基准的43%，是目前已知系统里效率最高的。论文已挂arXiv（编号2610.40503）。

第谷的笔记本，与开普勒的定律

ARC-AGI-3是前沿模型的新试炼场：没有规则，没有目标，全靠自己摸索。据量子位报道，GPT Astra配合Provider Adapter框架能拿到99.9%的高分，它会把游戏机制整理成密密麻麻的符号化规则。但在这篇论文看来，那更像第谷的观测记录本——精确，却只记录现象；真正从数据里推出行星运动三定律的，是开普勒。

只记录现象，代价很快就到。研究人员把sc25游戏改成不可能通关：第四关本来至少要19步才能赢，只给18步。Astra试了8轮，断言18步不行，估计至少要22步才能获胜。12次类似测试里，GPT-6 Astra与Claude Opus 5.5加起来只有5次判断出「不可能」，其中4次给出的最低步数仍是错的。

Astra整理出的符号化游戏规则。来源：量子位

AI 生成的事件示意图，不代表新闻现场照片。

三步走：探索、凝炼、证明

AWM把流程拆成三步：先探索，把看到的现象写成可执行的Python代码，当作初步假设；再凝炼，用新观察验证、修正假设，提炼出更通用的对象与规则；最后证明，把规律形式化成Lean 4语言，变成机器可以自动检查的数学断言。

回到那个无解关卡，基于Opus 5.5的AWM只尝试了两次，就直接证明：当前步数下无解，且只要再多一步就能获胜。它从范畴论里借来两个工具——投射极限负责「下定义」，把已有概念组合出新东西；归纳极限负责「找共性」，把不同现象统一进更抽象的框架。零散的Python假设就这样反复迭代，收敛成一个可以推理、可以证明的世界模型。

投射极限与归纳极限：AWM提炼世界结构的两种思维方式。来源：量子位

AI 生成的事件示意图，不代表新闻现场照片。

局部真理，与人的位置

论文署名也少见：两位共同第一作者都是本科生，一位是浙江大学休学来清华做研究的潘冠成，一位是清华姚班的谭淇心。指导者中，袁洋是清华大学交叉信息研究院、人工智能学院副教授；姚期智是2000年图灵奖得主、中国科学院院士，现任清华交叉信息研究院院长、人工智能学院院长。

AWM的证明只对它「观测到的世界」成立，探索不够全面，得到的就只是局部真理。有效路径仍是那个循环：观察、假设、实验、抽象、证明、再观察。技术正在学着像牛顿一样思考——而决定什么值得证明的，始终是人。