Algebraic World Model（AWM）研究尝试让 AI 从陌生环境中学出可检查的数学规则：先探索并编写 Python 假设，再依据观测修正规则，最终转换为 Lean 4 形式化模型，证明目标可达或不可达。
10 月 29 日公布的论文报告，在两类无解关卡的六次运行中，AWM 都构造了通过内核检查的不可达证明。研究还在 25 个公开 ARC-AGI-3 游戏、183 个关卡上验证模型。证明依赖所建立的环境规则，研究中的评测成绩不应直接理解为适用于任意现实问题。
来源：arXiv · 2610.40503 · 量子位