模型官方一手
清华 Algebraic World Model 用 Lean 4 证明 ARC-AGI-3 六关不可通关
Tsinghua's Algebraic World Model Proves ARC-AGI-3 Levels Unwinnable With Lean 4
精选理由
清华和浙大搞了个 AWM，用 Lean 4 把 ARC-AGI-3 六个关卡的规则写成数学证明，直接证明全部不可通关，前沿模型全卡壳。
清华大学与浙江大学提出 Algebraic World Model（AWM），用于分析 ARC-AGI-3 基准。该模型先学习游戏规则，再将规则形式化为 Lean 4 证明语言，最终数学证明全部六个密封关卡不可通关。这些关卡此前连前沿模型都无法通过。项目来自清华大学 Andrew Yao 团队。
原文 · Pandaily
Tsinghua's Algebraic World Model Proves ARC-AGI-3 Levels Unwinnable With Lean 4
Tsinghua and Zhejiang University's Algebraic World Model learns ARC-AGI-3 game rules, formalizes them in Lean 4 and proved all six sealed levels unwinnable, where frontier models failed.
- 量子位11-01 08:02原文
