图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队提出了”代数世界模型”（Algebraic World Model，AWM），一个将与陌生环境的交互转化为支持形式化推理的显式数学模型的框架。总体来看，AWM 尝试让 AI 在规则未知的环境中，先通过交互发现对象与规律，再将它们整理成明确的代数模型，借助 Lean 证明目标能否达成。当模型与真实环境出现偏差时，系统还可以追溯证明所依赖的具体规则，通过进一步探索修正模型。
图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队提出了”代数世界模型”（Algebraic World Model，AWM），一个将与陌生环境的交互转化为支持形式化推理的显式数学模型的框架。总体来看，AWM 尝试让 AI 在规则未知的环境中，先通过交互发现对象与规律，再将它们整理成明确的代数模型，借助 Lean 证明目标能否达成。当模型与真实环境出现偏差时，系统还可以追溯证明所依赖的具体规则，通过进一步探索修正模型。