Algebraic World Models：证明游戏无解之前，先证明你建对了世界
Lean通过的证明，什么时候仍然不能转移到真实游戏？
这项工作让智能体在交互中建立可执行规则，再把模型形式化为Lean定义与证明。最重要的边界是：证明对模型成立，与模型覆盖了游戏所有合法行为，是两件事；论文的封闭关卡实验也出现过转移失败。
图解主要方法
Lean通过的证明，什么时候仍然不能转移到真实游戏？
- 1
图1左：从交互记录形成可反驳规则
探索阶段用Python维护对象、属性与状态转移假设，对全部已观察转移输出TRUE、FALSE、NA或ERR。新动作前检查已有概念，失败就修订规则，保留与观察的对应关系。
- 2
中部：结构化并简化模型
以类型与范畴结构指导分解、组合、泛化和特化，辅助Lean检验结构性质。修改后必须保留对已观察记录的判断，并检验人为扰动的负例，避免通过放宽规则把错误也吞进去。
- 3
右部：把规则写成定义，再写证明
Lean4中先定义状态、动作与转移，再证明可赢轨迹或预算下不可能性；禁止sorry与native_decide作为证明捷径。可行轨迹提供成本上界，势函数等提供下界，两者相遇才支持最优成本。
- 4
把模型内结论与引擎结论分开
若模型漏掉真实游戏允许的捷径，“模型无解”可能错误外推为“游戏无解”。需要明确动作覆盖、状态抽象和转移映射的假设；一次合法胜利回放只证明一个上界，不自动证明所有更短路径不存在。
实验与证据
已阅读正文与相关证明边界、实验协议及附录访谈提示，核对实验条件与原图；未独立复现。
来源证据25游戏183关，报告全部胜利轨迹Lean验证并回放，分数99.9；7448是认证动作数，总交互动作24604，22个游戏已有此前未认证会话。 公开ARC3实验 ↗
我的解读不能把7448当全部探索成本，也不能将允许编程的系统与禁代码排行榜无条件横比。
来源证据两关真实最低成本19/36，给18/35预算，每关三次运行；6/6得到模型内证明，但初始只有4/6成本界正确，在获知存在更便宜胜利后修到6/6。 封闭sc25预算关卡 ↗
我的解读反馈没有直接给路线仍然提供了重要信息，最终结果不是一次无反馈自动发现。
来源证据模型到引擎的证明转移为5/6；42次故障诊断中利用依赖证明提升16→29次，已指出故障位置的对照为30次。 证明转移与诊断 ↗
我的解读恰好一次失败说明抽象覆盖是实质风险，形式化工具不替代建模验证。
开放情况与使用许可
官方项目页和论文提供方法与证明案例线索，本次未确认包含全部实验、数据及统一许可的完整可复现仓库。公开Lean案例不等于完整系统开源。
LICENSE作者版权；arXiv非独占托管许可
我的判断
独立分析 · 未复现实验正方 · 为什么值得投入
把不确定规则、可执行模型和可检查证明串起来，使智能体的“无解”结论比自然语言自信判断更可审计。
反方 · 哪些结论还不够
证据集中于离散确定性游戏，包含先前会话与代码权限差异；随机、连续、部分可观测环境尚未验证。
综合判断
值得借鉴为规则学习的审计流程，不能据此声称世界模型已具备一般形式可靠性。
我会先做的验证
未执行的验证方案：在隐藏捷径、未观察动作和随机转移的关卡上，记录模型内证明、引擎覆盖检查与反例发现率；强制报告无法转移的前提而非只报证明编译成功。