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

清华大学姚期智和袁洋团队提出代数世界模型（AWM），把交互环境中的对象与规则抽象为代数世界，经探索、凝炼、证明三步形成可机器检查的Lean 4断言。在ARC-AGI-3测试集上，基于Opus 5的AWM通关183个关卡，得分99.9%，平均通关动作数为人类基准的43%；面对无解关卡，基于Opus 5.5的AWM尝试两次即可证明其无解并指出再多一步即可获胜。