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

清华大学姚期智、袁洋团队提出代数世界模型（AWM），把交互环境抽象为代数世界，用Lean 4将规律形式化为可机器检查的证明。在ARC-AGI-3测试集上，AWM基于Opus 5以99.9%得分通关全部183个关卡，平均动作数只有人类基准的43%；面对无解关卡，基于Opus 5.5的AWM两次尝试即可证明无解。