清华姚期智团队提出代数世界模型 AWM，让 AI 像牛顿一样从现象推导规律

清华大学姚期智、袁洋团队提出代数世界模型（AWM），通过探索、凝炼、证明三步把观察到的规律形式化为 Lean 4 可检查的数学断言。在 ARC-AGI-3 测试集上，基于 Opus 5 的 AWM 通关 183 个关卡，得分 99.9%，平均动作数仅为人类基准的 43%；面对步数不足的无解关卡，它用两次尝试即证明其无解并指出再加一步即可获胜。