清华团队提出 Algebraic World Model 框架，将未知环境探索转化为 Lean 4 形式化证明
Algebraic World Model: From Exploration to Proofs
AI 导读
论文提出 Algebraic World Model（AWM）框架，把与陌生环境的交互转化为可形式化推理的数学模型，用 Python 假设探索、类别论指导简化结构并在 Lean 4 中证明可达性与不可达性。
推荐理由
论文给出从环境探索到 Lean 形式化证明的完整框架和对照实验，读者可以评估可验证世界模型在未知环境推理上的可用性。
正文 · 原文
Abstract: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.
| Comments: | 29 pages, 9 figures, 14 tables. Project page: this https URL. Ancillary files contain the Lean 4 model of the running example lp85 |
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2610.40503 [cs.AI] |
| (or arXiv:2610.40503v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.40503 arXiv-issued DOI via DataCite |
Submission history
From: Qixin Tan [view email]
[v1]
Thu, 29 Oct 2026 17:20:31 UTC (1,326 KB)
来源：arXiv cs.AI · arxiv.org