Algebraic World Model: From Exploration to Proofs
一句话概括
AWM 把陌生环境中的交互经验转化为可执行的数学模型，再用 Lean 4 形式化，从而证明目标可达或不可达。它在不可解游戏关卡上给出了内核检验的排除性证明，而基线模型未能给出。
速览
- 任务：让 AI 对未知环境建立显式数学模型，并做形式化推理与证明。
- 方法：探索环境 → 生成 Python 假设 → 按观测修正 → 范畴论引导化简 → Lean 4 形式化。
- 关键数字：2 个不可解关卡、6 次运行全部给出封闭证明；基线 12 次运行均无证明；ARC-AGI-3 全部 25 个游戏、183 个关卡可被 Lean 重放。
- 数据与开源：摘要未给出数据集与代码开源情况。
问题背景
当前 AI 在数学上进展明显，能在 Lean 中产出机器可检验的证明。但这些工作通常依赖预先给定的数学定义与形式化规格。
于是出现一个更基本的问题：面对一个未知世界，AI 能否严格推理？这里的困难不在计算，而在建模——环境规则未知，目标是否可达也无从判断。
作者把这一能力称为「代数世界模型（Algebraic World Model, AWM）」，强调模型应是显式的、可执行的、可形式化的。
方法要点
AWM 的流程分四步。
- 探索环境，提出可执行的 Python 假设，并持续用观测检验和修正。
- 把假设整理为带类型的对象（typed objects）与共享规则，形成结构化模型。
- 借助范畴论（category theory）引导的变换化简模型结构。
- 将模型形式化到 Lean 4，证明可达性与不可能性。
关键点在于「不可能性证明」：AWM 能证明某目标不可达，且结论覆盖已探索轨迹之外的情形。摘要称其证明为封闭的、经内核检验的（kernel-checked）。
关键结论
- 在 2 个不可解游戏关卡上，AWM 在 6 次运行中均构造出封闭的 Lean 证明，排除所有合法获胜序列。
- 同样配备编码工具的 Claude Opus 5.5 与 GPT-6 Astra，在 12 次基线运行中未产出任何此类证明。
- 初始界（bound）正确率：AWM 6 次中 4 次正确；Opus 5.5 为 1 次；GPT-6 Astra 为 0 次。
- 仅给出「存在更省步数的获胜方式」这一反馈后，AWM 修正规则并重建证明，达到 6/6 正确。
- 在全部 25 个公开 ARC-AGI-3 游戏中，这些模型让 Lean 重放全部 183 个关卡的获胜轨迹，并能预测未见转移、检测游戏机制变化。
- 配合 Claude Opus 5，AWM 通关全部关卡，得分 99.9；其经认证的获胜轨迹仅用人类基线 43% 的动作数。
读后思考
这篇工作的价值在于把「会解题」推进到「会建模」。前者依赖给定规格，后者要求在规格缺失时自己造出规格，并让机器检验它。
「不可能性」是更硬的检验标准。可达性可以靠一次成功轨迹证明，不可达则必须排除全部合法序列，这正是形式化的用武之地。
另一个值得注意的点是可解释性：模型规则可被逐步检查和测试，这使 AI 的推理过程从黑箱变为可审计对象。
局限与开放问题
- 摘要未给出方法的计算开销、探索预算与失败情形。
- 实验集中在游戏环境，能否迁移到更开放的未知世界，摘要未给出证据。
- 范畴论化简的具体作用与必要性，摘要未给出消融结果。
- 初始界 4/6 正确说明规则归纳仍会出错，修正依赖外部反馈，自主发现问题仍是开放点。
- 代码与数据是否开源，摘要未给出。