姚期智团队新作：代数世界模型

假设有一个游戏关卡，AI尝试了很多次都没能通关，那么究竟是它还没找到解法，还是给定的行动次数根本不够？ 前一个问题，只要找到任意一条获胜路线就能回答，但要证明无解，就必须排除所有合法路线，包括那些尚未尝试过的路线。 如果游戏连规则都不公开，AI还需要先弄清自己究竟在证明什么。 通关和证明无解，难度完全不同。

为此，图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队提出了“代数世界模型”（Algebraic World Model，AWM），一个将与陌生环境的交互转化为支持形式化推理的显式数学模型的框架。 AWM首先通过交互探索环境，提出并修正规则假设，再将这些规则组织成数学模型，最终写入Lean 4，构造可由内核检查的形式化证明。 借助这套方法，AI不仅能够回答怎样获胜，还能证明在给定约束下为什么无法获胜。 这项工作的核心，是把经验观察与证明所依赖的前提连接起来。

传统形式化推理通常从预先给定的数学定义和规则出发。 AWM则需要从陌生环境中主动发现这些结构，并在后续交互中不断检验和修正学到的规则。 整个过程分为三个阶段。 第一阶段，agent主动探索环境，将对机制的猜测写成可执行的Python假设，再用观察到的状态变化测试这些假设。 当预测与反馈不一致时，系统不会直接把已有经验当作确定规则，而是选择继续修正模型。 第二阶段，AWM将假设整理为带类型的对象和规则，并在范畴论指导下变换结构，识别共性、简化表示。

具体而言，系统通过分解、组合、泛化和特化四种变换，重新组织对象类型与规则。 这些变换都需要在Lean中接受检查，以确保模型在简化过程中保留已经检验过的行为特征。 第三阶段，系统在Lean 4中完成形式化建模，并构造相应证明。 对于可通关的关卡，一条合法的获胜行动序列就能证明目标可达。 对于无法在预算内通关的关卡，系统则可以寻找行动过程中始终成立的不变量，或者证明任何获胜序列所需成本的下界，从而排除预算范围内的所有合法获胜路线。 团队在ARC-AGI-3上检验了这种不可达推理能力。 这些游戏不预先公开规则和目标。

他们以sc25的两个关卡为基础，保留机制，将行动预算设置为略低于最低获胜成本，构造出两个无法在预算内通关的变体。 每个关卡运行三次，AWM在全部六次运行中都构造出了通过Lean内核检查的封闭证明，在所学模型下排除了预算内所有合法获胜序列。 团队报告，配备编程工具的Claude Opus 5.5和GPT-6 Astra在合计十二次基线运行中，均未产生这类证明。 不过，证明通过检查，并不等于系统学到了完全正确的环境规则。 AWM最初六次运行给出的获胜成本下界中，四次与真实最低成本相符。

Opus 5.5有一次给出正确界限，但未附证明，Astra则没有给出正确界限。 其余基线运行存在界限错误或未得出结论的情况。 其中一个例子发生在第4关。 GPT-6 Astra声称最低获胜成本为22，但未提供证明。 AWM则在所学模型下证明了19的紧下界，并验证了一条成本为19的获胜路线，与游戏实际最低获胜成本一致。 这也提示了必须区分的两类错误：推理可能严格遵循规则，但规则本身仍可能与环境不符。 形式化证明不能替代对建模前提的检验。 他们还考察了模型能否准确表达已观察到的游戏过程。

AWM为全部25个公开游戏构建的模型中，对象类型数量中位数为6，规则数量中位数为10。 这些模型支持在Lean中回放全部183个关卡的获胜轨迹，检查模型所表示的状态转移与最终目标条件。 此外，团队还测试了模型对未观察过行为的预测能力。 在部分游戏中，AWM冻结探索阶段学到的规则，再将其用于随机游戏轨迹和经过修改的游戏机制。 实验显示，模型能够预测未见过的布局变化，也能够识别与原有规则不一致的机制变化，说明其学习到的规则具备一定的泛化能力。

在通关表现方面，使用Claude Opus 5的AWM在全部关卡中取得了99.9分的成绩，表现接近领先的代码执行型系统。 其经过认证的获胜轨迹总共使用7,448次行动，仅为人类基线17,135次行动的43%。 需要说明的是，这几组实验分别考察了模型对已观察行为的复现、对未见行为的泛化，以及游戏通关效率。 它们能够说明AWM在环境建模和任务执行方面的表现，但仍需与对真实环境的不可达性证明区分开来。 他们也指出了这项研究的局限性：目前，AWM主要在具有离散动作、即时可观察反馈的ARC类环境中得到验证。

对于包含更复杂隐藏状态、延迟反馈和随机动态的环境，其适用性仍有待进一步测试。 此外，Lean能够保证证明从模型明确给出的前提出发，按照形式化规则正确推导，但这些前提是否准确描述真实环境，仍需要通过交互来确认。 研究团队认为，AWM将模型规则和证明依赖关系显式呈现出来，有助于定位问题所在，并通过进一步探索修正错误。 未来，还需要在更多类型的环境和任务中检验这种形式化推理能力。 总体来看，AWM尝试让AI在规则未知的环境中，先通过交互发现对象与规律，再将它们整理成明确的代数模型，借助Lean证明目标能否达成。

这套方法的意义，在于让AI的推理能够覆盖尚未探索过的行动序列，同时让结论所依赖的假设变得清晰、可检查。 当模型与真实环境出现偏差时，系统还可以追溯证明所依赖的具体规则，通过进一步探索修正模型。 从经验探索到数学建模，再到形式化证明，AWM为AI在未知环境中开展严谨推理提供了一条新的技术路径。