清华姚期智团队提出代数世界模型AWM，让AI用Lean 4形式化证明推理

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