清华姚期智团队提出代数世界模型 AWM，让 AI 从探索走向形式化证明

清华大学姚期智、袁洋团队提出代数世界模型（AWM），把游戏中的对象、关系和规则抽象为代数世界，经探索、凝炼、证明三步生成 Lean 4 可检验的数学断言。在 ARC-AGI-3 测试集上，基于 Opus 5 的 AWM 通关全部 183 个关卡，得分 99.9%，平均通关动作数仅为人类基准的 43%。面对被改成无解的关卡，它两次尝试即证明当前步数下无解，且只需再多一步即可获胜。