「如果只让AI学习牛顿发现万有引力之前的知识，它自己能不能推出来？」这类思想实验长期卡在数据污染与场景不可复原上。清华大学姚期智、袁洋团队提出的代数世界模型（Algebraic World Model，AWM），尝试换一条路：让模型从观察与实验出发，把规律凝炼成可机器检查的断言。
团队用ARC-AGI-3游戏集作试金石。这类关卡几乎不给规则说明，要求自行摸索。顶尖模型可以把机制整理成密密麻麻的符号化规则，像第谷式观测本——精确记录现象，却未必抓住本质。把某关初始步数改成客观上不可通关的数值后，模型仍可能给出错误的「最少步数」估计，暴露「只靠直觉试错」的幻觉。
AWM的做法分三步：先探索，把现象写成可执行的Python假设；再凝炼，用新观察修正并提炼更通用对象与规则；最后证明，把规律形式化为Lean 4断言，交给机器自动检查。它从范畴论借用「投射极限」与「归纳极限」两类操作，在概念组合与共性抽象之间迭代，让零散假设收敛成可推理结构。
公开结果称，基于Claude Opus等底座的AWM，能更快证明「当前步数无解且再多一步可胜」；在ARC-AGI-3全量关卡上取得极高通关率，平均动作数显著低于人类基准。共同一作包括浙大休学在清华做研究的潘冠成与清华姚班谭淇心；指导教师为袁洋与姚期智。项目页与论文已公开（arXiv:2610.40503）。
边界同样清楚：证明只在「观测到的世界」内成立，探索不全就会得到局部真理。真正可用的路径仍是观察—假设—实验—抽象—证明的循环。对智能体产品来说，AWM的启发不在刷榜数字，而在「任务不可能时能否说清为什么不可能」——这比再堆一串看似专业的伪规则更接近工程可信，也更接近科学史里从现象走到定律的工作方式。