Algebraic World Model: From Exploration to Proofs

📄 arXiv: 2610.40503v1 📥 PDF

作者: Guancheng Pan, Qixin Tan, Yang Yuan, Andrew Chi-Chih Yao

分类: cs.AI, cs.LO

发布日期: 2026-10-29

备注: 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)

关键词: 代数世界模型 形式推理 自动定理证明 复杂系统建模 游戏智能

📋 核心要点

  1. 现有方法通常依赖于预定义的数学定义，缺乏对未知环境的严格推理能力。
  2. 代数世界模型（AWM）通过与环境互动生成数学模型，支持形式推理并进行假设测试与修正。
  3. AWM在多个实验中表现优异，成功证明了目标不可达，且在游戏中超越了其他基线模型的表现。

📝 摘要（中文）

人工智能在数学领域取得了显著进展，能够通过可机器检查的证明解决复杂问题，但通常依赖于预定义的数学定义和形式规范。这引出了一个自然的问题：它能否对未知世界进行严格推理？本文提出了代数世界模型（AWM），该框架将与不熟悉环境的互动转化为支持形式推理的明确数学模型。AWM探索环境并开发可执行的Python假设，持续测试和修正这些假设。最终，它将这些假设结构化为类型化对象和共享规则，并通过范畴理论指导的变换简化其结构，最后在Lean 4中形式化模型以证明可达性和不可能性。

🔬 方法详解

问题定义：本文旨在解决人工智能在未知环境中进行严格推理的能力不足问题。现有方法通常依赖于预定义的数学定义，无法有效处理不熟悉的环境。

核心思路：代数世界模型（AWM）通过与环境的互动生成可执行的假设，并不断测试和修正这些假设，从而形成明确的数学模型，支持形式推理。

技术框架：AWM的整体架构包括环境探索、假设生成与测试、模型结构化、简化和形式化等主要模块。首先，AWM探索环境并生成Python假设；然后，测试这些假设并根据观察结果进行修正；接着，结构化为类型化对象和共享规则；最后，在Lean 4中形式化模型以进行证明。

关键创新：AWM的主要创新在于其能够在未探索的轨迹上证明目标不可达，这一能力超越了现有的推理方法。AWM通过构建可解释的数学模型，使得推理过程透明可检验。

关键设计：AWM采用了范畴理论指导的变换来简化模型结构，确保生成的假设能够被有效测试和验证。模型的设计允许逐步检查和测试规则，增强了其可解释性和可靠性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

AWM在两个不可能的游戏关卡中成功构建了封闭的、经过内核检查的Lean证明，排除了所有合法的获胜序列。在六次实验中，AWM的四个初始界限是正确的，而对比的Claude Opus 5.5和GPT-6 Astra在十二次基线实验中均未能产生有效证明。AWM的表现显著优于其他模型，展示了其在复杂推理任务中的优势。

🎯 应用场景

代数世界模型（AWM）在多个领域具有广泛的应用潜力，尤其是在自动定理证明、游戏智能和复杂系统建模等方面。通过提供可解释的数学模型，AWM能够帮助研究人员和工程师更好地理解和优化系统行为，推动智能体在未知环境中的决策能力。未来，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.