摘要AI 可以在形式化数学题中生成 Lean 证明但这类任务通常已经给定了数学对象和规则。面对规则未知的游戏智能体首先要通过交互发现物体、动作和目标再判断自己的模型是否足以支持严谨推理。论文提出 Algebraic World ModelAWM把探索、可执行规则、代数结构整理和 Lean 4 证明连接起来使智能体不仅能证明如何获胜还尝试证明在给定预算内不可能获胜。论文版本arXiv:2610.40503v2标题为Algebraic World Model: From Exploration to Proofs版本日期为 2026 年 10 月 30 日。阅读重点本文同时解释模型证明的边界。Lean 可以保证证明确实从形式模型的定义推出证明能否推广到真实环境还取决于学习到的模型是否覆盖相关环境行为。文章目录一、这篇论文想解决什么问题二、先建立直觉从探索到证明论文图 1AWM 的三阶段流程三、AWM 的“世界模型”究竟由什么组成四、探索把观察变成可执行假设4.1 交互记录是什么4.2 检查与修正机制五、结构化为什么要从很多规则抽象出共享机制论文图 2从相似案例中抽取共享结构5.1 合并不是单纯的代码重构5.2 lp85 的共享置换示例六、形式化Lean 能证明什么6.1 证明能够获胜6.2 证明在预算内不可解论文图 3预算边界、正确下界与未证明的估计七、最重要的边界形式证明依赖世界模型7.1 论文如何描述证明迁移7.2 论文也报告了模型学错后再修正的情况八、实验结果该怎样读8.1 公开 ARC-AGI-3 游戏8.2 两个预算受限的密封关卡九、AWM 的独特贡献9.1 从交互中学习可审查的显式规则9.2 将结构化简化与证明辅助结合9.3 从成功路线扩展到不可解性证明9.4 证明依赖也可以帮助调试模型十、方法的限制与适用范围十一、如何复现和阅读这篇论文十二、总结参考资料一、这篇论文想解决什么问题使用 AI 解数学题时题目通常直接给出对象、定义、假设和目标。证明器可以在这些规格之内寻找推理步骤。未知环境更棘手。例如一个游戏可能只显示方格、按钮、角色和目标却不告诉智能体什么东西是可交互对象按钮会怎样改变环境什么条件表示成功某一步动作的代价是多少已经找到一条获胜路径能否证明所有更便宜的路径都不存在最后一个问题尤其重要。找到获胜轨迹只能证明“至少有一种方法可以赢”。它不能证明这条路线是最便宜的更不能通过几次失败的尝试证明“所有路线都行不通”。论文提出代数世界模型Algebraic World ModelAWM目标是从交互中学习环境的对象、规则和目标再将这些内容形式化到 Lean 4使证明器能够在形式模型中验证可达性、不可解性及相关性质。二、先建立直觉从探索到证明AWM 分成三个阶段Explore Prototype探索并构造原型。智能体试探环境把观察到的状态变化整理为可执行的 Python 假设并不断用新数据检查和修正。Structure Simplify组织结构并化简。将分散的假设整理成类型化对象和规则合并可共享的机制同时保留已经测试出的行为差异。Formalize Prove形式化并证明。将模型写入 Lean 4证明可达路径、不可解边界或其他状态性质。论文图 1AWM 的三阶段流程图片来自论文 v2 第 2 页 Figure 1。整体逻辑是先从交互数据形成可执行假设再把假设整理成明确模型最后让 Lean 检查模型上的定理。这一顺序有实际意义如果一开始就写 Lean却不知道环境中的规则是什么形式化的对象可能并不对应真实游戏如果只写代码模拟器模拟器虽然能跑也未必能够证明穷尽所有可能动作。三、AWM 的“世界模型”究竟由什么组成论文把世界模型表示为类型化对象、规则和目标谓词。组成部分回答的问题示例对象类型当前世界里有哪些结构棋盘、格子、按钮、角色、燃料、预算规则动作如何改变这些结构点击按钮后哪些格子会交换颜色目标谓词什么状态算成功角色到达出口且预算没有耗尽动作代价一步操作如何计入资源移动、点击、施法及奖励的成本形式化后可以把环境的核心转移抽象为s t e p ( w , a ) w ′ , \mathrm{step}(w,a)w,step(w,a)w′,其中w ww是当前状态a aa是动作w ′ ww′是执行动作后的状态。此表达是概念性简化论文中的 Lean 模型还包括动作是否合法、终止状态及具体任务条件。探索阶段还会为每项概念保存其适用范围、相关观察、检查器以及可选的预测器。检查器将一条观测到的转移判定为TRUE与规则相符FALSE与规则矛盾NA不在该规则的适用范围内ERR检查器出错、超时或输出无效。如果新观察与某项假设矛盾AWM 必须修改或撤回假设不能继续把它当作已经成立的事实使用。四、探索把观察变成可执行假设4.1 交互记录是什么论文将一次交互抽象为三元组观察到的当前画面 执行动作 执行后的新画面例如按下棋盘左侧按钮 → 一组方格颜色顺着轨道旋转这条观察可以支持一个 Python 假设例如“按下这个按钮会沿闭合轨道循环排列颜色”。但一条样本不足以证明该规则普遍正确。模型还要区分规则适用于哪些对象、哪些画面以及哪些可能只是碰巧同时发生的变化。4.2 检查与修正机制AWM 为规则记录自然语言说明、适用范围、支持它的转移、检查器和可选的预测函数。系统随后将规则重新应用于已收集的交互记录。如果规则对已观察记录给出矛盾结果或者检查程序报错系统需要先修正规则再继续探索。这个过程把“写一个看起来合理的规则”变成“规则必须接受观察数据持续检验”。但是已观察数据只能约束已观察到的行为。少量样本没有覆盖的机制仍可能使模型遗漏真实规则。因此探索质量和模型覆盖性仍是后续结论的关键边界。五、结构化为什么要从很多规则抽象出共享机制探索初期智能体可能为每个按钮都写一条独立规则。若有四种按钮机制就可能有多条相似描述。重复规则会增加形式化与推理负担也不容易看出不同情况背后的共同结构。AWM 借鉴范畴论中的极限与余极限组织对象类型与规则。论文把相关变换概括为四类操作直观含义例子分解将一个复杂对象或规则表达为若干部分把棋盘状态拆成格子、轨道和按钮组合从兼容部分组成整体根据组件定义完整的游戏状态泛化从多个案例找出共用规则将多个按钮都描述成格子位置的置换特化为过于宽泛的规则增加类别或参数按按钮位置选择不同旋转方向论文图 2从相似案例中抽取共享结构图片来自论文 v2 第 6 页 Figure 3。它展示了论文中lp85游戏的一个示例探索阶段记录了 11 条描述四类按钮机制的概念结构化阶段将这些机制归纳为一个带参数的共享规则press_permutes即按钮按其对应方式置换颜色位置。5.1 合并不是单纯的代码重构把多条规则合并成一条规则只有在证据支持时才有意义。否则简化模型可能丢失重要的行为区别。论文通过两类检查约束结构化过程新结构须保持对已记录有效转移的覆盖在用于诊断的扰动转移上不应丢掉旧规则已经识别出的反例。每项结构变换还需要有 Lean 中可检查的辅助声明。范畴论工具在这里用于组织兼容性和共享结构它不会自动发现正确的游戏规则规则仍须通过交互观察及诊断样本验证。5.2lp85的共享置换示例在lp85中点击按钮会改变彩色格子的位置。AWM 将四类按钮机制概括成统一规则按钮指定一种排列方式按下后格子的颜色依照该排列变化。由于置换只改变位置、不改变颜色的总数量模型可以导出一个不变量每次按键之后棋盘上的颜色多重集保持不变。如果把起始状态中的黄色方格重新着色而获胜条件仍然要求目标位置具有黄色那么任何只做位置置换的按钮都不能制造出黄色。Lean 据此证明修改后的关卡不可解。这个证明不是穷举每一串按键而是利用共享规则推导出对所有合法按键都成立的不变量。六、形式化Lean 能证明什么AWM 使用 Lean 4 表示对象、动作转移和目标条件。它的证明分为两种常见方向6.1 证明能够获胜要证明可达性可以给出一串具体动作作为见证并让 Lean 检查每一步转移以及最后是否到达目标。初始状态 w₀ → 动作 a₁ → 状态 w₁ → 动作 a₂ → …… → 获胜状态一条检查通过的获胜轨迹足以证明“存在一条成功路径”。它不能单独证明路径长度最优。6.2 证明在预算内不可解设任务有动作预算B BB任何获胜路线至少需要C min C_{\min}Cmin单位代价。如果证明C min B , C_{\min}B,CminB,就可以推出预算不足以获胜。在sc25案例中论文构造的第 4 关变体预算为 18而其实际最低获胜代价为 19。AWM 在形式模型中证明了 18 预算内不存在获胜序列并验证了代价为 19 的获胜路线。这两部分合起来说明该模型中的最小成本是 19。论文图 3预算边界、正确下界与未证明的估计图片来自论文 v2 第 9 页 Figure 4。图中还说明了一个常见逻辑区别找到成本为 22 的获胜路线只能提供一个“可在 22 成本内获胜”的上界它不能证明最小成本就是 22。论文的关键创新之一是针对未知环境中的不可解性构造闭合、经过 Lean 内核检查的证明。证明能够排除模型中所有合法动作序列包括探索时从未实际尝试过的序列。七、最重要的边界形式证明依赖世界模型“Lean 内核确认了证明”与“真实游戏一定不可解”不是同一句话。Lean 的结论严格对应 Lean 中写入的对象、转移规则、目标定义和预算假设。如果真实游戏中有一个模型遗漏的合法动作或者某个代价规则学错了那么模型中的证明仍然可能完全正确却不能直接迁移到游戏本身。7.1 论文如何描述证明迁移论文提出sufficient cover条件对某个给定任务只要模型能够覆盖真实环境中所有最优获胜序列就足以用模型中的不可解性结果支持关于该任务的不可解结论不必一定覆盖环境的每一个转移。对于预算任务论文还检查与引擎有关的预算可行转移、证明势函数的不等式以及不变量所需的状态条件。这类检查用于评估模型结论是否能迁移到特定游戏配置。所以在描述 AWM 结果时应同时说清楚形式正确性Lean 是否确认定理确由形式模型推出模型忠实度模型规则是否覆盖该任务相关的真实行为任务匹配度目标定义、预算和成本计算是否与游戏一致模型证明非常重要但必须和模型验证结合起来看。7.2 论文也报告了模型学错后再修正的情况密封关卡实验中AWM 首次得到的六个下界有四个符合真实最低成本。另两个虽然在 Lean 模型内有效但模型学得过于严格遗漏了游戏中的较便宜路径导致数值下界过高。只给出“存在更便宜的获胜方式”这一反馈后AWM 重新检查相关规则并对修改后的模型重新生成 Lean 证明。修正规则后六次运行的下界都与游戏参考结果对齐。这个结果揭示了 AWM 的完整研究目标形式证明不是规则学习的替代品它会把推理所依赖的规则暴露出来帮助研究者发现哪里需要继续检查。八、实验结果该怎样读论文评估了两个不同问题AWM 是否能从未知游戏中构造模型并完成游戏AWM 是否能够对预算受限的修改关卡给出不可解性证明这两组实验的任务、设置和基线不同不能混成一个排行榜结论。8.1 公开 ARC-AGI-3 游戏AWM 使用 Claude Opus 5 作为交互智能体对 25 个公开游戏中的 183 个关卡进行探索和解题。论文报告指标论文报告值官方平均得分99.9得分 100 的游戏数23 / 25Lean 回放并检查的获胜关卡数183 / 183Lean 形式化规则数220Lean 定理数1,374已认证获胜轨迹动作数7,448认证解题动作数与人工基线之比43%论文还报告每个游戏模型的中位规模为 6 种对象类型和 10 条规则。这里的 43% 是已认证获胜轨迹的动作数与人工基线之比探索、重置和失败会话也要消耗动作纳入这些会话后论文报告的引擎动作总数为 24,604。关于模型在未见画面上的泛化论文进一步冻结lp85和ft09的规则在从未出现过的画面及经过修改的关卡上检查。结果显示规则既能预测某些未见状态的转移也会在点击机制发生变化时识别不一致。这里的测试覆盖的是特定游戏和测试集不能推断所有未知环境都能同样泛化。8.2 两个预算受限的密封关卡论文在sc25的两个修改关卡上将预算设为比分别已知的最低获胜成本低一个单位。每个智能体在每个关卡上运行三次共比较六次运行。方法经 Lean 内核检查的模型证明初始下界正确数反馈修正后正确数Claude Opus 5.50 / 61 / 61 / 6GPT-6 Astra0 / 60 / 62 / 6AWM6 / 64 / 66 / 6这里的“6 / 6 模型证明”表示六次 AWM 运行都生成了 Lean 检查通过的模型内不可解性证明。初始有两次由于模型规则过于严格数值下界与游戏最低成本不一致。经过有限信息反馈和规则修订后下界正确数达到 6 / 6。这项实验同时支持两个不同结论AWM 可以构造基线未能构造的内核检查证明同时证明是否描述真实游戏还需要检查模型覆盖性和成本定义。九、AWM 的独特贡献9.1 从交互中学习可审查的显式规则许多模型通过内部状态表达环境认知难以逐条检查“为什么这个动作会改变这些对象”。AWM 将规则写为类型化对象、命名操作和可执行检查器研究者可以直接查看预测并与观察结果比对。9.2 将结构化简化与证明辅助结合规则简化不只为代码减少行数。将多个案例归纳成共享规则后一个不变量就可能适用于多个机制从而减少证明需要单独处理的例外。论文还为结构变换提供 Lean 辅助检查使“合并前后所表示的关系”有明确的形式化说明。9.3 从成功路线扩展到不可解性证明在搜索空间很大时几次没有赢并不等于不存在获胜方法。AWM 使用不变量、状态不变性质或成本下界去排除一整类合法动作序列尝试把“没找到解”提升为“在明确条件下证明没有解”。9.4 证明依赖也可以帮助调试模型若定理使用了哪些规则在证明依赖中有记录当结论与环境结果不符时研究者可以优先检查相应规则。论文报告在注入规则错误的测试中将证明依赖提供给 Claude Opus 5.5 后其发现相关反例的成功数从 42 次中的 16 次提高到 29 次。证明因此不仅是结论也可作为定位错误规则的诊断线索。十、方法的限制与适用范围论文关注的是目标明确、具有部分可观测性的确定性环境示范任务集中在 ARC-AGI-3 游戏。它不是面向所有现实开放环境的通用安全证明系统。实践或复现时需要额外考虑覆盖性探索数据是否暴露了影响目标的关键规则隐状态仅凭当前画面是否足以确定后续转移成本一致性不同动作的代价、奖励和预算检查是否一致模型修订规则改动后相关定理是否全部重新检查迁移验证Lean 模型中的转移如何与真实引擎或设备交叉核对扩展成本状态数量和证明复杂度增大时形式化与求解是否仍可管理作者也将研究范围限定在特定交互环境中。将类似框架应用于机器人、工业控制或物理系统需要证明观测模型、动作执行、故障模式和安全约束之间的关系不能直接照搬游戏实验的结论。十一、如何复现和阅读这篇论文论文附有交互网站、Lean 文件和相关运行资料。建议按以下顺序阅读先看论文Figure 1建立三阶段流程图。阅读第 2 节理解概念检查器、结构化变换及形式化方式。对照Figure 3理解共享规则和不变量如何支持证明。阅读第 3 节与 Table 1、Table 2区分公开关卡成绩、Lean 回放和模型规模。阅读第 4 节与 Table 3、Figure 4区分证明有效性、下界正确性和模型迁移。查看附录 A.4了解作者如何讨论模型结论向真实环境迁移的条件。十二、总结AWM 将未知环境中的 AI 推理拆成了可逐步审查的工作流交互产生假设测试推动规则修订结构化操作抽取共享机制Lean 4 检查关于形式模型的定理。它最重要的想法不只是“让 AI 用 Lean 证明”而是把证明和环境建模连接起来系统能够给出获胜见证也尝试证明预算受限时不存在获胜路线与此同时明确暴露证明依赖哪些学习规则为检查模型错误提供入口。理解实验结果时始终应把两件事分开证明是否对形式模型成立以及这个模型是否忠实覆盖了要讨论的真实任务。这一区分决定了模型级形式保证能够在多大程度上变成环境级结论。参考资料Pan, G., Tan, Q., Yuan, Y., Yao, A. C.Algebraic World Model: From Exploration to Proofs. arXiv:2610.40503v2, 2026.论文页面v2论文 PDFv2AWM 交互演示与研究材料本文中插入的图表从用户提供的论文 PDF 第 2、6、9 页裁剪保留了论文的原图说明其余示例与中文解读用于辅助理解。论文成绩和 proof 结果均按 v2 版本报告非本文独立复现实验。 
长河君 · 2026/11/5 5:33:51 · 阅读 1.2k AWM：让 AI 从探索未知世界走向可验证证明
摘要AI 可以在形式化数学题中生成 Lean 证明但这类任务通常已经给定了数学对象和规则。面对规则未知的游戏智能体首先要通过交互发现物体、动作和目标再判断自己的模型是否足以支持严谨推理。论文提出 Algebraic World ModelAWM把探索、可执行规则、代数结构整理和 Lean 4 证明连接起来使智能体不仅能证明如何获胜还尝试证明在给定预算内不可能获胜。论文版本arXiv:2610.40503v2标题为Algebraic World Model: From Exploration to Proofs版本日期为 2026 年 10 月 30 日。阅读重点本文同时解释模型证明的边界。Lean 可以保证证明确实从形式模型的定义推出证明能否推广到真实环境还取决于学习到的模型是否覆盖相关环境行为。文章目录一、这篇论文想解决什么问题二、先建立直觉从探索到证明论文图 1AWM 的三阶段流程三、AWM 的“世界模型”究竟由什么组成四、探索把观察变成可执行假设4.1 交互记录是什么4.2 检查与修正机制五、结构化为什么要从很多规则抽象出共享机制论文图 2从相似案例中抽取共享结构5.1 合并不是单纯的代码重构5.2 lp85 的共享置换示例六、形式化Lean 能证明什么6.1 证明能够获胜6.2 证明在预算内不可解论文图 3预算边界、正确下界与未证明的估计七、最重要的边界形式证明依赖世界模型7.1 论文如何描述证明迁移7.2 论文也报告了模型学错后再修正的情况八、实验结果该怎样读8.1 公开 ARC-AGI-3 游戏8.2 两个预算受限的密封关卡九、AWM 的独特贡献9.1 从交互中学习可审查的显式规则9.2 将结构化简化与证明辅助结合9.3 从成功路线扩展到不可解性证明9.4 证明依赖也可以帮助调试模型十、方法的限制与适用范围十一、如何复现和阅读这篇论文十二、总结参考资料一、这篇论文想解决什么问题使用 AI 解数学题时题目通常直接给出对象、定义、假设和目标。证明器可以在这些规格之内寻找推理步骤。未知环境更棘手。例如一个游戏可能只显示方格、按钮、角色和目标却不告诉智能体什么东西是可交互对象按钮会怎样改变环境什么条件表示成功某一步动作的代价是多少已经找到一条获胜路径能否证明所有更便宜的路径都不存在最后一个问题尤其重要。找到获胜轨迹只能证明“至少有一种方法可以赢”。它不能证明这条路线是最便宜的更不能通过几次失败的尝试证明“所有路线都行不通”。论文提出代数世界模型Algebraic World ModelAWM目标是从交互中学习环境的对象、规则和目标再将这些内容形式化到 Lean 4使证明器能够在形式模型中验证可达性、不可解性及相关性质。二、先建立直觉从探索到证明AWM 分成三个阶段Explore Prototype探索并构造原型。智能体试探环境把观察到的状态变化整理为可执行的 Python 假设并不断用新数据检查和修正。Structure Simplify组织结构并化简。将分散的假设整理成类型化对象和规则合并可共享的机制同时保留已经测试出的行为差异。Formalize Prove形式化并证明。将模型写入 Lean 4证明可达路径、不可解边界或其他状态性质。论文图 1AWM 的三阶段流程图片来自论文 v2 第 2 页 Figure 1。整体逻辑是先从交互数据形成可执行假设再把假设整理成明确模型最后让 Lean 检查模型上的定理。这一顺序有实际意义如果一开始就写 Lean却不知道环境中的规则是什么形式化的对象可能并不对应真实游戏如果只写代码模拟器模拟器虽然能跑也未必能够证明穷尽所有可能动作。三、AWM 的“世界模型”究竟由什么组成论文把世界模型表示为类型化对象、规则和目标谓词。组成部分回答的问题示例对象类型当前世界里有哪些结构棋盘、格子、按钮、角色、燃料、预算规则动作如何改变这些结构点击按钮后哪些格子会交换颜色目标谓词什么状态算成功角色到达出口且预算没有耗尽动作代价一步操作如何计入资源移动、点击、施法及奖励的成本形式化后可以把环境的核心转移抽象为s t e p ( w , a ) w ′ , \mathrm{step}(w,a)w,step(w,a)w′,其中w ww是当前状态a aa是动作w ′ ww′是执行动作后的状态。此表达是概念性简化论文中的 Lean 模型还包括动作是否合法、终止状态及具体任务条件。探索阶段还会为每项概念保存其适用范围、相关观察、检查器以及可选的预测器。检查器将一条观测到的转移判定为TRUE与规则相符FALSE与规则矛盾NA不在该规则的适用范围内ERR检查器出错、超时或输出无效。如果新观察与某项假设矛盾AWM 必须修改或撤回假设不能继续把它当作已经成立的事实使用。四、探索把观察变成可执行假设4.1 交互记录是什么论文将一次交互抽象为三元组观察到的当前画面 执行动作 执行后的新画面例如按下棋盘左侧按钮 → 一组方格颜色顺着轨道旋转这条观察可以支持一个 Python 假设例如“按下这个按钮会沿闭合轨道循环排列颜色”。但一条样本不足以证明该规则普遍正确。模型还要区分规则适用于哪些对象、哪些画面以及哪些可能只是碰巧同时发生的变化。4.2 检查与修正机制AWM 为规则记录自然语言说明、适用范围、支持它的转移、检查器和可选的预测函数。系统随后将规则重新应用于已收集的交互记录。如果规则对已观察记录给出矛盾结果或者检查程序报错系统需要先修正规则再继续探索。这个过程把“写一个看起来合理的规则”变成“规则必须接受观察数据持续检验”。但是已观察数据只能约束已观察到的行为。少量样本没有覆盖的机制仍可能使模型遗漏真实规则。因此探索质量和模型覆盖性仍是后续结论的关键边界。五、结构化为什么要从很多规则抽象出共享机制探索初期智能体可能为每个按钮都写一条独立规则。若有四种按钮机制就可能有多条相似描述。重复规则会增加形式化与推理负担也不容易看出不同情况背后的共同结构。AWM 借鉴范畴论中的极限与余极限组织对象类型与规则。论文把相关变换概括为四类操作直观含义例子分解将一个复杂对象或规则表达为若干部分把棋盘状态拆成格子、轨道和按钮组合从兼容部分组成整体根据组件定义完整的游戏状态泛化从多个案例找出共用规则将多个按钮都描述成格子位置的置换特化为过于宽泛的规则增加类别或参数按按钮位置选择不同旋转方向论文图 2从相似案例中抽取共享结构图片来自论文 v2 第 6 页 Figure 3。它展示了论文中lp85游戏的一个示例探索阶段记录了 11 条描述四类按钮机制的概念结构化阶段将这些机制归纳为一个带参数的共享规则press_permutes即按钮按其对应方式置换颜色位置。5.1 合并不是单纯的代码重构把多条规则合并成一条规则只有在证据支持时才有意义。否则简化模型可能丢失重要的行为区别。论文通过两类检查约束结构化过程新结构须保持对已记录有效转移的覆盖在用于诊断的扰动转移上不应丢掉旧规则已经识别出的反例。每项结构变换还需要有 Lean 中可检查的辅助声明。范畴论工具在这里用于组织兼容性和共享结构它不会自动发现正确的游戏规则规则仍须通过交互观察及诊断样本验证。5.2lp85的共享置换示例在lp85中点击按钮会改变彩色格子的位置。AWM 将四类按钮机制概括成统一规则按钮指定一种排列方式按下后格子的颜色依照该排列变化。由于置换只改变位置、不改变颜色的总数量模型可以导出一个不变量每次按键之后棋盘上的颜色多重集保持不变。如果把起始状态中的黄色方格重新着色而获胜条件仍然要求目标位置具有黄色那么任何只做位置置换的按钮都不能制造出黄色。Lean 据此证明修改后的关卡不可解。这个证明不是穷举每一串按键而是利用共享规则推导出对所有合法按键都成立的不变量。六、形式化Lean 能证明什么AWM 使用 Lean 4 表示对象、动作转移和目标条件。它的证明分为两种常见方向6.1 证明能够获胜要证明可达性可以给出一串具体动作作为见证并让 Lean 检查每一步转移以及最后是否到达目标。初始状态 w₀ → 动作 a₁ → 状态 w₁ → 动作 a₂ → …… → 获胜状态一条检查通过的获胜轨迹足以证明“存在一条成功路径”。它不能单独证明路径长度最优。6.2 证明在预算内不可解设任务有动作预算B BB任何获胜路线至少需要C min C_{\min}Cmin单位代价。如果证明C min B , C_{\min}B,CminB,就可以推出预算不足以获胜。在sc25案例中论文构造的第 4 关变体预算为 18而其实际最低获胜代价为 19。AWM 在形式模型中证明了 18 预算内不存在获胜序列并验证了代价为 19 的获胜路线。这两部分合起来说明该模型中的最小成本是 19。论文图 3预算边界、正确下界与未证明的估计图片来自论文 v2 第 9 页 Figure 4。图中还说明了一个常见逻辑区别找到成本为 22 的获胜路线只能提供一个“可在 22 成本内获胜”的上界它不能证明最小成本就是 22。论文的关键创新之一是针对未知环境中的不可解性构造闭合、经过 Lean 内核检查的证明。证明能够排除模型中所有合法动作序列包括探索时从未实际尝试过的序列。七、最重要的边界形式证明依赖世界模型“Lean 内核确认了证明”与“真实游戏一定不可解”不是同一句话。Lean 的结论严格对应 Lean 中写入的对象、转移规则、目标定义和预算假设。如果真实游戏中有一个模型遗漏的合法动作或者某个代价规则学错了那么模型中的证明仍然可能完全正确却不能直接迁移到游戏本身。7.1 论文如何描述证明迁移论文提出sufficient cover条件对某个给定任务只要模型能够覆盖真实环境中所有最优获胜序列就足以用模型中的不可解性结果支持关于该任务的不可解结论不必一定覆盖环境的每一个转移。对于预算任务论文还检查与引擎有关的预算可行转移、证明势函数的不等式以及不变量所需的状态条件。这类检查用于评估模型结论是否能迁移到特定游戏配置。所以在描述 AWM 结果时应同时说清楚形式正确性Lean 是否确认定理确由形式模型推出模型忠实度模型规则是否覆盖该任务相关的真实行为任务匹配度目标定义、预算和成本计算是否与游戏一致模型证明非常重要但必须和模型验证结合起来看。7.2 论文也报告了模型学错后再修正的情况密封关卡实验中AWM 首次得到的六个下界有四个符合真实最低成本。另两个虽然在 Lean 模型内有效但模型学得过于严格遗漏了游戏中的较便宜路径导致数值下界过高。只给出“存在更便宜的获胜方式”这一反馈后AWM 重新检查相关规则并对修改后的模型重新生成 Lean 证明。修正规则后六次运行的下界都与游戏参考结果对齐。这个结果揭示了 AWM 的完整研究目标形式证明不是规则学习的替代品它会把推理所依赖的规则暴露出来帮助研究者发现哪里需要继续检查。八、实验结果该怎样读论文评估了两个不同问题AWM 是否能从未知游戏中构造模型并完成游戏AWM 是否能够对预算受限的修改关卡给出不可解性证明这两组实验的任务、设置和基线不同不能混成一个排行榜结论。8.1 公开 ARC-AGI-3 游戏AWM 使用 Claude Opus 5 作为交互智能体对 25 个公开游戏中的 183 个关卡进行探索和解题。论文报告指标论文报告值官方平均得分99.9得分 100 的游戏数23 / 25Lean 回放并检查的获胜关卡数183 / 183Lean 形式化规则数220Lean 定理数1,374已认证获胜轨迹动作数7,448认证解题动作数与人工基线之比43%论文还报告每个游戏模型的中位规模为 6 种对象类型和 10 条规则。这里的 43% 是已认证获胜轨迹的动作数与人工基线之比探索、重置和失败会话也要消耗动作纳入这些会话后论文报告的引擎动作总数为 24,604。关于模型在未见画面上的泛化论文进一步冻结lp85和ft09的规则在从未出现过的画面及经过修改的关卡上检查。结果显示规则既能预测某些未见状态的转移也会在点击机制发生变化时识别不一致。这里的测试覆盖的是特定游戏和测试集不能推断所有未知环境都能同样泛化。8.2 两个预算受限的密封关卡论文在sc25的两个修改关卡上将预算设为比分别已知的最低获胜成本低一个单位。每个智能体在每个关卡上运行三次共比较六次运行。方法经 Lean 内核检查的模型证明初始下界正确数反馈修正后正确数Claude Opus 5.50 / 61 / 61 / 6GPT-6 Astra0 / 60 / 62 / 6AWM6 / 64 / 66 / 6这里的“6 / 6 模型证明”表示六次 AWM 运行都生成了 Lean 检查通过的模型内不可解性证明。初始有两次由于模型规则过于严格数值下界与游戏最低成本不一致。经过有限信息反馈和规则修订后下界正确数达到 6 / 6。这项实验同时支持两个不同结论AWM 可以构造基线未能构造的内核检查证明同时证明是否描述真实游戏还需要检查模型覆盖性和成本定义。九、AWM 的独特贡献9.1 从交互中学习可审查的显式规则许多模型通过内部状态表达环境认知难以逐条检查“为什么这个动作会改变这些对象”。AWM 将规则写为类型化对象、命名操作和可执行检查器研究者可以直接查看预测并与观察结果比对。9.2 将结构化简化与证明辅助结合规则简化不只为代码减少行数。将多个案例归纳成共享规则后一个不变量就可能适用于多个机制从而减少证明需要单独处理的例外。论文还为结构变换提供 Lean 辅助检查使“合并前后所表示的关系”有明确的形式化说明。9.3 从成功路线扩展到不可解性证明在搜索空间很大时几次没有赢并不等于不存在获胜方法。AWM 使用不变量、状态不变性质或成本下界去排除一整类合法动作序列尝试把“没找到解”提升为“在明确条件下证明没有解”。9.4 证明依赖也可以帮助调试模型若定理使用了哪些规则在证明依赖中有记录当结论与环境结果不符时研究者可以优先检查相应规则。论文报告在注入规则错误的测试中将证明依赖提供给 Claude Opus 5.5 后其发现相关反例的成功数从 42 次中的 16 次提高到 29 次。证明因此不仅是结论也可作为定位错误规则的诊断线索。十、方法的限制与适用范围论文关注的是目标明确、具有部分可观测性的确定性环境示范任务集中在 ARC-AGI-3 游戏。它不是面向所有现实开放环境的通用安全证明系统。实践或复现时需要额外考虑覆盖性探索数据是否暴露了影响目标的关键规则隐状态仅凭当前画面是否足以确定后续转移成本一致性不同动作的代价、奖励和预算检查是否一致模型修订规则改动后相关定理是否全部重新检查迁移验证Lean 模型中的转移如何与真实引擎或设备交叉核对扩展成本状态数量和证明复杂度增大时形式化与求解是否仍可管理作者也将研究范围限定在特定交互环境中。将类似框架应用于机器人、工业控制或物理系统需要证明观测模型、动作执行、故障模式和安全约束之间的关系不能直接照搬游戏实验的结论。十一、如何复现和阅读这篇论文论文附有交互网站、Lean 文件和相关运行资料。建议按以下顺序阅读先看论文Figure 1建立三阶段流程图。阅读第 2 节理解概念检查器、结构化变换及形式化方式。对照Figure 3理解共享规则和不变量如何支持证明。阅读第 3 节与 Table 1、Table 2区分公开关卡成绩、Lean 回放和模型规模。阅读第 4 节与 Table 3、Figure 4区分证明有效性、下界正确性和模型迁移。查看附录 A.4了解作者如何讨论模型结论向真实环境迁移的条件。十二、总结AWM 将未知环境中的 AI 推理拆成了可逐步审查的工作流交互产生假设测试推动规则修订结构化操作抽取共享机制Lean 4 检查关于形式模型的定理。它最重要的想法不只是“让 AI 用 Lean 证明”而是把证明和环境建模连接起来系统能够给出获胜见证也尝试证明预算受限时不存在获胜路线与此同时明确暴露证明依赖哪些学习规则为检查模型错误提供入口。理解实验结果时始终应把两件事分开证明是否对形式模型成立以及这个模型是否忠实覆盖了要讨论的真实任务。这一区分决定了模型级形式保证能够在多大程度上变成环境级结论。参考资料Pan, G., Tan, Q., Yuan, Y., Yao, A. C.Algebraic World Model: From Exploration to Proofs. arXiv:2610.40503v2, 2026.论文页面v2论文 PDFv2AWM 交互演示与研究材料本文中插入的图表从用户提供的论文 PDF 第 2、6、9 页裁剪保留了论文的原图说明其余示例与中文解读用于辅助理解。论文成绩和 proof 结果均按 v2 版本报告非本文独立复现实验。