姚期智团队提出代数世界模型以实现形式化推理

姚期智团队提出代数世界模型（AWM），通过三阶段流程将陌生环境的交互转化为可在Lean 4中验证的形式化证明，实现对通关路径的构造与不可达性的严格证明。实验显示，AWM在ARC-AGI-3测试中六次均生成通过检查的封闭证明，且在通关效率上优于人类基线，行动次数仅为人类的43%。