清华团队提出 Algebraic World Model 框架，将未知环境探索转化为 Lean 4 形式化证明

查看 PDF HTML (实验性)

摘要:AI 在数学领域取得了显著进展，能够在 Lean 中以机器可检验的证明解决具有挑战性的问题，但通常依赖于预定义的数学定义和形式化规范。这引出一个自然的问题：它能否对未知世界进行严谨的推理？我们提出了代数世界模型（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%。

Comments:	29 页，9 幅图，14 张表。项目页面：this https URL。附件文件包含运行示例 lp85 的 Lean 4 模型
Subjects:	Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
Cite as:	arXiv:2610.40503 [cs.AI]
	(或 arXiv:2610.40503v1 [cs.AI] 指向此版本)
	https://doi.org/10.48550/arXiv.2610.40503 arXiv 发行的 DOI，经 DataCite

提交历史

来自: Qixin Tan [查看邮件]
[v1] 2026年10月29日星期四 17:20:31 UTC (1,326 KB)