代数世界模型 AWM：从探索到 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% 的动作。

评论：	29 页，9 幅图，14 张表。项目页面：此 https URL。附属文件包含运行示例 lp85 的 Lean 4 模型
主题：	人工智能（cs.AI）；计算机科学中的逻辑（cs.LO）
引用为：	arXiv:2610.40503 [cs.AI]
	（或 arXiv:2610.40503v1 [cs.AI] 用于此版本）
	https://doi.org/10.48550/arXiv.2610.40503 由 DataCite 颁发的 arXiv DOI

提交历史

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