清华团队提出代数世界模型：让AI从试错走向可证明推理

导语

让AI像科学家一样工作，关键不只是让它看到更多数据，还要让它能够从现象中提炼规律，并检验这些规律是否真的成立。清华大学姚期智、袁洋团队提出的代数世界模型（Algebraic World Model，AWM），正是在尝试解决这一问题。

从“记笔记”到“建理论”

在ARC-AGI-3这类缺少明确规则和目标的交互环境中，AI需要通过试错摸索世界。素材提到，部分顶级模型能够把游戏中的现象整理为大量符号化规则，甚至取得很高分数。但这些规则更像观测记录：它们描述了发生过什么，却未必说明背后的机制，更难回答“当前任务是否根本无解”以及“为什么无解”。

研究者用修改后的关卡测试这一能力。当可用步数少于理论最低步数时，模型有时会继续尝试，甚至给出错误的最低步数判断。对于游戏，这只是效率问题；放到现实任务中，智能体错误地声称某个方案可行或不可行，可能带来更严重的后果。

AWM如何工作

AWM把环境中的对象、关系和操作抽象为一个可计算的代数世界，主要包含三个环节：

• 探索：通过交互收集现象，并将初步规律写成可执行的Python假设。
• 凝炼：用新的实验结果检验、修正和合并假设，形成更一般化的对象与规则。
• 证明：将关键规律转写为Lean 4中的形式化命题，由机器检查其逻辑是否成立。

这套流程的核心变化，是把“多试几次猜答案”转为“建立模型并验证模型”。素材称，在一个无解关卡上，基于Opus 5.5的AWM经过两次尝试即可证明当前步数不足，并判断只需增加一步便能完成任务。报道还称，AWM在ARC-AGI-3测试集的183个关卡中全部通关，平均动作数为人类基准的43%。这些结果说明，形式化建模可能同时改善智能体的效率与可解释性。

范畴论带来的抽象视角

AWM借鉴了范畴论中的投射极限和归纳极限：前者可理解为组合已有概念及其关系，后者则用于从不同现象中提炼共同结构。通过两种操作反复迭代，零散的程序化假设可以逐步变得更统一、更简洁，也更适合推理和证明。

意义与边界

AWM的价值不在于让AI简单模仿牛顿，而在于提供了一种“观察—假设—实验—抽象—证明”的工作流。它有望被用于游戏环境、智能体规划以及更复杂的交互任务，尤其适合需要判断可行性、解释失败原因的场景。

不过，形式化证明只能保证模型内部逻辑一致，不能自动保证模型已经观察到了完整世界。如果探索遗漏关键规则，得到的仍可能只是局部真理。因此，未来系统还需要扩大实验覆盖范围，并持续在真实反馈中修正世界模型。

来源：量子位