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

清华姚期智和袁洋团队提出代数世界模型 AWM，通过探索、凝炼和 Lean 4 形式化证明，让 AI 从观察中推导并验证世界规律。基于 Opus 5.5 的 AWM 在无解关卡中尝试两次后判断当前步数不可行，并指出再增加一步即可获胜；其在 ARC-AGI-3 的 183 个关卡中全部通关，得分 99.9%，平均通关动作数为人类基准的 43%。