Yao's team proposes the Algebraic World Model AWM, using Lean 4 to prove that a game has no solution
English text is being prepared.
Yao's team proposes the Algebraic World Model (AWM), which enables AI, in an environment with unknown rules, to first discover and revise rule hypotheses through interaction, then organize them into a mathematical model and write it into Lean 4, constructing a formal proof that can be checked by the kernel. The team constructed two levels on ARC-AGI-3 whose action budgets are slightly below the minimum winning cost. AWM produced, in all six runs, a closed proof that passed the Lean kernel check, ruling out all legal winning sequences within the budget; Claude Opus 5.5 and GPT-6 Astra, equipped with programming tools, did not produce such proofs in a total of twelve baseline runs. Among the winning-cost lower bounds given by AWM in its initial six runs, four matched the true minimum cost, and after feedback-based revision all six bounds were correct; AWM using Claude Opus 5 achieved a score of 99.9 on all levels, with certified winning trajectories totaling 7,448 actions, which is 43% of the human baseline of 17,135.
Why read this
AI score 52
Yao's team connects rule discovery in unfamiliar environments with Lean 4 formal proofs into a single pipeline, allowing readers to understand how AI can prove that no solution exists rather than merely seeking to clear the game.
Topics
Body
前一个问题，只要找到任意一条获胜路线就能回答，但要证明无解，就必须排除所有合法路线，包括那些尚未尝试过的路线。如果游戏连规则都不公开，AI 还需要先弄清自己究竟在证明什么。通关和证明无解，难度完全不同。
为此，图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队提出了“代数世界模型”（Algebraic World Model，AWM），一个将与陌生环境的交互转化为支持形式化推理的显式数学模型的框架。
AWM 首先通过交互探索环境，提出并修正规则假设，再将这些规则组织成数学模型，最终写入 Lean 4，构造可由内核检查的形式化证明。借助这套方法，AI 不仅能够回答怎样获胜，还能证明在给定约束下为什么无法获胜。
这项工作的核心，是把经验观察与证明所依赖的前提连接起来。传统形式化推理通常从预先给定的数学定义和规则出发。AWM 则需要从陌生环境中主动发现这些结构，并在后续交互中不断检验和修正学到的规则。
整个过程分为三个阶段。
第一阶段，agent主动探索环境，将对机制的猜测写成可执行的 Python 假设，再用观察到的状态变化测试这些假设。当预测与反馈不一致时，系统不会直接把已有经验当作确定规则，而是选择继续修正模型。
图｜AWM 的三阶段流水线
第二阶段，AWM 将假设整理为带类型的对象和规则，并在范畴论指导下变换结构，识别共性、简化表示。具体而言，系统通过分解、组合、泛化和特化四种变换，重新组织对象类型与规则。这些变换都需要在 Lean 中接受检查，以确保模型在简化过程中保留已经检验过的行为特征。
图｜由射影极限与归纳极限引导的四类变换，作用于对象类型和规则
第三阶段，系统在 Lean 4 中完成形式化建模，并构造相应证明。对于可通关的关卡，一条合法的获胜行动序列就能证明目标可达。对于无法在预算内通关的关卡，系统则可以寻找行动过程中始终成立的不变量，或者证明任何获胜序列所需成本的下界，从而排除预算范围内的所有合法获胜路线。
图｜AWM 从四类按钮机制中归纳出共享的颜色置换规则
团队在 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 的获胜路线，与游戏实际最低获胜成本一致。
图｜两个 agent对通关所需的最低成本存在分歧
对于 AWM 另外两次不准确的界限，他们仅反馈存在成本更低的获胜方案，系统随后修正规则，重新构造证明，最终使六次运行的界限全部正确。
这也提示了必须区分的两类错误：推理可能严格遵循规则，但规则本身仍可能与环境不符。形式化证明不能替代对建模前提的检验。
他们还考察了模型能否准确表达已观察到的游戏过程。AWM 为全部 25 个公开游戏构建的模型中，对象类型数量中位数为 6，规则数量中位数为 10。这些模型支持在 Lean 中回放全部 183 个关卡的获胜轨迹，检查模型所表示的状态转移与最终目标条件。
此外，团队还测试了模型对未观察过行为的预测能力。在部分游戏中，AWM 冻结探索阶段学到的规则，再将其用于随机游戏轨迹和经过修改的游戏机制。实验显示，模型能够预测未见过的布局变化，也能够识别与原有规则不一致的机制变化，说明其学习到的规则具备一定的泛化能力。
在通关表现方面，使用 Claude Opus 5 的 AWM 在全部关卡中取得了 99.9 分的成绩，表现接近领先的代码执行型系统。其经过认证的获胜轨迹总共使用 7,448 次行动，仅为人类基线 17,135 次行动的 43%。
需要说明的是，这几组实验分别考察了模型对已观察行为的复现、对未见行为的泛化，以及游戏通关效率。它们能够说明 AWM 在环境建模和任务执行方面的表现，但仍需与对真实环境的不可达性证明区分开来。
图｜25 个公开 ARC-AGI-3 游戏的官方得分
他们也指出了这项研究的局限性：目前，AWM 主要在具有离散动作、即时可观察反馈的 ARC 类环境中得到验证。对于包含更复杂隐藏状态、延迟反馈和随机动态的环境，其适用性仍有待进一步测试。
此外，Lean 能够保证证明从模型明确给出的前提出发，按照形式化规则正确推导，但这些前提是否准确描述真实环境，仍需要通过交互来确认。研究团队认为，AWM 将模型规则和证明依赖关系显式呈现出来，有助于定位问题所在，并通过进一步探索修正错误。未来，还需要在更多类型的环境和任务中检验这种形式化推理能力。
总体来看，AWM 尝试让 AI 在规则未知的环境中，先通过交互发现对象与规律，再将它们整理成明确的代数模型，借助 Lean 证明目标能否达成。
这套方法的意义，在于让 AI 的推理能够覆盖尚未探索过的行动序列，同时让结论所依赖的假设变得清晰、可检查。当模型与真实环境出现偏差时，系统还可以追溯证明所依赖的具体规则，通过进一步探索修正模型。
从经验探索到数学建模，再到形式化证明，AWM 为 AI 在未知环境中开展严谨推理提供了一条新的技术路径。
更多技术细节，详见原论文。
本文来自微信公众号 “学术头条”（ID：SciTouTiao），作者：张佳怡，36氪经授权发布。