Algebraic World Model: From Exploration to Proofs
作者: Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao
分类: cs.AI, cs.LO
发布日期: 2026-10-29 (更新: 2026-10-30)
备注: 29 pages, 9 figures, 14 tables. Project page: https://ephemeral6.github.io/awm-site/. Ancillary files contain the Lean 4 model of the running example lp85
💡 一句话要点
提出代数世界模型以解决未知环境中的推理问题
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 代数世界模型 形式化推理 自动化定理证明 未知环境 机器学习
📋 核心要点
- 现有方法通常依赖于预定义的数学定义，无法有效处理未知环境中的推理问题。
- 代数世界模型（AWM）通过与环境交互，生成可执行的假设并进行形式化推理，解决了未知世界的推理挑战。
- AWM在多个实验中表现优异，成功构建了闭合的Lean证明，且在游戏关卡中超越了其他基线模型的表现。
📝 摘要（中文）
人工智能在数学领域取得了显著进展，能够通过可机器检查的证明解决复杂问题，但通常依赖于预定义的数学定义和形式规范。这引出了一个自然的问题：它能否对未知世界进行严格推理？本文提出了代数世界模型（AWM），该框架将与不熟悉环境的交互转化为支持形式推理的显式数学模型。AWM探索环境并开发可执行的Python假设，持续测试和修正这些假设。最终，AWM能够在Lean 4中形式化模型，以证明可达性和不可能性，并在多个实验中展示了其有效性。
🔬 方法详解
问题定义：本文旨在解决人工智能在未知环境中进行严格推理的能力不足，现有方法多依赖于预定义的数学结构，无法有效应对新的挑战。
核心思路：代数世界模型（AWM）通过与环境的交互，动态生成和修正假设，最终形成可形式化的数学模型，以支持严格的推理过程。
技术框架：AWM的整体架构包括环境探索、假设生成与测试、类型化对象构建、分类理论指导的结构简化，以及在Lean 4中的形式化证明。
关键创新：AWM的主要创新在于其能够在未探索的轨迹中证明目标不可达，并通过动态修正假设来适应环境变化，这一能力在现有方法中尚未实现。
关键设计：AWM采用了Python进行假设的执行与测试，利用类别理论进行结构简化，并在Lean 4中实现形式化证明，确保了模型的可解释性和可验证性。
🖼️ 关键图片
📊 实验亮点
在实验中，AWM在两个不可能的游戏关卡中成功构建了闭合的Lean证明，排除了所有合法的获胜序列，而其他基线模型在相同条件下未能产生有效证明。AWM的初始边界中有四个是正确的，而其他模型仅有一个或没有。
🎯 应用场景
该研究的潜在应用领域包括自动化定理证明、机器人导航、游戏AI等。AWM能够在未知环境中进行有效推理，具有广泛的实际价值，未来可能推动智能系统在复杂任务中的应用。
📄 摘要（原文）
AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal specifications. This raises a natural question: can it reason rigorously about an unknown world? We introduce the Algebraic World Model (AWM), a framework that turns interaction with unfamiliar environments into explicit mathematical models supporting formal reasoning. AWM explores the environment and develops executable Python hypotheses, continually testing and revising them against observations. It then structures these hypotheses into typed objects and shared rules, simplifies their structure through category-theory-guided transformations, and formalizes the resulting model in Lean 4 to prove reachability and impossibility. AWM can formally prove that a goal is unreachable, even beyond explored trajectories. On two impossible game levels, it constructs closed, kernel-checked Lean proofs excluding every legal winning sequence in all six runs, while Claude Opus 5.5 and GPT-6 Astra, equipped with coding tools, produce none in twelve baseline runs. Four of AWM's six initial bounds are correct, compared with one for Opus 5.5 and none for GPT-6 Astra; given only feedback that a cheaper win exists, AWM revises its rules and constructs new proofs, reaching six of six correct bounds. Moreover, AWM produces interpretable mathematical models whose rules can be inspected and tested step by step. Across all 25 public ARC-AGI-3 games, these models enable Lean to replay the winning trajectories of all 183 levels and generalize beyond observed play, predicting unseen transitions and detecting changes in game mechanics. With Claude Opus 5, AWM clears all levels with a score of 99.9, while its certified winning trajectories use only 43% of the human baseline's actions.