Algebraic World Model：从探索到证明

AI 在数学领域取得了显著进展，能够借助 Lean 中可由机器检查的证明解决具有挑战性的问题，但通常依赖预先定义的数学定义和形式化规范。这引出了一个自然的问题：AI 能否对一个未知世界进行严格推理？我们提出 Algebraic World Model（AWM），这是一个将与陌生环境的交互转化为支持形式化推理的显式数学模型的框架。AWM 探索环境并构建可执行的 Python 假设，持续根据观察结果对其进行测试和修订。随后，它将这些假设组织成带类型的对象和共享规则，通过范畴论指导的变换简化其结构，并在 Lean 4 中将所得模型形式化，以证明可达性和不可实现性。AWM 能够形式化证明某个目标不可达，即使该目标超出了已探索的轨迹范围。在两个不可能通关的游戏关卡上，它构造了闭合的、经内核检查的 Lean 证明，排除了六次运行中所有合法的获胜序列；而配备编码工具的 Claude Opus 5.5 和 GPT-6 Astra 在十二次基线运行中均未能构造出任何此类证明。AWM 初始给出的六个界限中有四个是正确的，而 Opus 5.5 正确一个、GPT-6 Astra 一个也没有；在仅获得“存在更低成本的获胜方式”这一反馈后，AWM 修订了其规则并构造出新的证明，最终六个界限全部正确。此外，AWM 生成的数学模型具有可解释性，其规则可以逐步检查和测试。在全部 25 个公开的 ARC-AGI-3 游戏中，这些模型使 Lean 能够重放 183 个关卡的所有获胜轨迹，并推广到观察到的游戏过程之外，预测未见过的状态转移并检测游戏机制的变化。结合 Claude Opus 5，AWM 以 99.9 分通过了所有关卡，而其经认证的获胜轨迹仅使用了人类基线行动次数的 43%。