姚期智团队提出代数世界模型，AI“不可能”结论可获形式化证明

11月4日，由中国科学院院士姚期智与清华大学交叉信息研究院副教授袁洋带领的团队发表论文《代数世界模型：从探索走向证明》，提出“代数世界模型”（AWM）概念，将游戏中的对象、关系和规则抽象为代数世界，利用大模型的数学能力理解世界。

论文在ARC-AGI-3上报告：AWM在6次“密封关卡”运行中全部构造出Lean内核检查的封闭证明，证明给定预算下不存在获胜序列；对比的Claude Opus 5.5和GPT-6 Astra合计12次运行均未产生此类证明。AWM给出的初始最低成本下界有4次与真实最低成本一致，在仅被告知存在更便宜获胜方案后，6次下界全部修正正确。

论文提出，AWM的价值在于当AI声称“做不到”时，能把这个断言变成可被独立程序检查的数学证明，并说明前提与边界。论文第一作者为浙江大学潘冠诚与清华“姚班”谭启新。