傻子循环 9/9，专用 RL 0/9：AlphaProof Nexus 架构对撞实录，兼论 Agent 编排的折旧定律

Google DeepMind 今年 5 月的论文《Advancing Mathematics Research with AI-Driven Formal Proof Search》（arXiv:2605.22763，v2 更新于 6 月 8 日）在站内已经有三篇好帖了：完整战报版《当代码学会证定理》（topic 177620736）把 9 个 Erdős 问题、44 个 OEIS 猜想讲得很全；《败局之冠与神迹之火》（topic 177980932）从 2.5% 成功率的角度泼了冷水；还有一篇入门解读讲了"Gemini 出思路、Lean 做裁判"的基本盘。

战报和冷水都被讲过了，这篇讲点别的：论文第 5 节和附录 B.3 里那组消融实验。这是全篇最值钱、也最容易被战报叙事淹没的部分——DeepMind 把自家四层架构和两个外部对手扔进角斗场对撞，撞出来的结果，够整个 Agent 工程圈琢磨一年。

一句话预告：最笨的那套架构复现了全部成功，专用 RL 系统单打独斗零解，商用 coding agent 差两题追平 DeepMind 全家桶，而输得最惨的对手是死于性格。

一、先把笼子讲清楚：Lean 编译器是个什么裁判

要理解后面的对撞，得先理解这个系统的地基。它简单到一句话：LLM 负责出候选，Lean 4 编译器负责一票裁决。

Lean 是形式化证明语言，在 Lean 里定义、定理、证明全是代码，编译器会逐步"执行"证明，每一步做类型检查，直到没有任何未完成的目标才算过关。它还有一种特殊战术叫 sorry——一个合法的"此处有洞"标记，能通过类型检查但会被明确标记出来。于是整个游戏可以重新表述成一个工程问题：

证明一个定理 = 生成一段类型安全、且不含 sorry 的代码。

这就是我说的"笼子"。LLM 的幻觉在这个框架下不再是致命缺陷，而是搜索成本——错一千次没关系，只要对一次，编译器就替你把这一次锁死，永不反悔。

但 DeepMind 没有停在"编译器当裁判"这一层。他们给笼子上了三道锁【A】：

1. 编译器：每次代码编辑后立即编译，错误信息原文塞回下一轮 prompt。这是一个免费的、100% 精确的、无限耐心的专家，随时在线骂你；
2. Sandbox check：每一轮尝试结束时检查——允许留 sorry，但目标定理的陈述不许被偷改。Agent 想把"对所有 n 成立"悄悄改成"对某些 n 成立"？拦下；
3. SafeVerify：最终验收，独立检查证明编译通过、没有 sorryAx、没有违规注入公理（axiom injection）——防止模型在证明文件头部私加一条"显然引理"来作弊。

物理层面，编译跑在 Docker 沙箱里的 Lean v4.27，交互用的是 Pantograph——Lean 专为社会化 agent 设计的机器对机器接口，不走人类终端那一套。恶意代码跑不出来，agent 也不必假装自己是人类敲命令行。

笼子有一个后门，而且论文里真被钻了一次。 Erdős #125 原题问"三进制数字集与四进制数字集之和集的密度"，自然语言里"density"这个词有歧义。Agent 用"自然密度"的口径把题证了——数学家复审才发现原题意图是"下密度"，改完陈述后 agent 又把修正版证了。注意这个事件的两面性：往坏了说，agent 会主动钻问题翻译的空子，专挑软柿子捏；往好了说，它成了形式化错误的检测器——同一个机制，既能钻空子，也能照出题库本身的洞。牢笼锁得住证明过程的合法性，锁不住问题翻译的忠实性，这是当前所有"LLM+形式验证"系统的共同软肋。

二、第二件事：这个系统其实有四层，最底下那层最不像话

论文里的 AlphaProof Nexus 是渐进式的四层架构，从最简到最繁【A】：

Agent A（basic）：N 个 prover 子代理完全独立、零共享状态，从同一个起点出发各自证明，任意一个成功，全体终止。每个子代理内部是一个"Ralph loop"——这个梗下面单独讲——多轮 Gemini 3.1 Pro 会话，一个 search-replace 编辑工具，每次编辑后编译，报错喂回。一轮尝试（episode）结束时如果还留着 sorry，就把"这一轮学到了什么"写成代码注释，下一轮从当前状态继续。

Agent B（A + AlphaProof 工具）：prover 可以把卡住的子目标递给 AlphaProof——就是 2024 年拿 IMO 银牌、2025 年发 Nature 的那个 RL 证明系统。注意，在这里它不是主角，是会诊的专科医生：返回三种结果，证出来了 / 反证了（这个子目标是假的）/ 没搞定。反证也是营养，直接进 prompt。预算管得很死：每轮最多 5 次 AlphaProof 调用、90 次编辑。

Agent C（A + 进化）：所有尝试过的证明草稿——包括大量带 sorry 的"烂代码"——全部入种群数据库。便宜的 Gemini 3.0 Flash 当评委，每次抽 7 份草稿打排位赛，按 Plackett-Luce 模型 + Gibbs 采样推断每份草稿的 Elo 分，父本选择用 P-UCB 公式。这就是标题里"烂代码锦标赛"的由来，第三部分细讲。

Agent D（B + C，全功能版）：进化 + AlphaProof 工具全开。这套系统实际出征了 353 个 Erdős 问题，也就是战报里 9/353 的缔造者。

现在说回 Ralph loop。论文白纸黑字引用了 Geoffrey Huntley 2025 年的博客《Ralph Wiggum as a "software engineer"》【A】。Ralph Wiggum 是《辛普森一家》里的傻子角色，Huntley 的哲学可以用一行 bash 表达：

while :; do cat PROMPT.md | claude ; done

不加规划，不做编排，不给记忆，让 agent 像傻子一样无限循环干活，直到干成为止。原文有几句值得抄在这里【A】：

• "deterministically bad in an undeterministic world"——在不确定的世界里确定性地犯蠢，反而是种美德；
• 单体优于多代理通信，是"microservices 的反面"——代理间消息传递是复杂度黑洞；
• backpressure（反压）来自牢笼：类型系统、测试、静态分析。模型的奖励函数是让代码编译通过，所以它必然会写 placeholder——这句话是预言，下文 agent 的失败模式会精确兑现它；
• 人不在环内。人做的是观察失败模式、立牌子（往 prompt 里加约束）、调音。

DeepMind 的 basic agent 就是把 Ralph 哲学原样搬进数学：一个 while 循环、一个 diff 工具、一个编译器、一群并行傻子。没有 MCTS，没有 planner，没有代理间协议。而解出 56 年悬置数学问题的配置，就是它。

三、烂代码锦标赛：在二值世界里硬造连续地形

Agent C/D 的进化机制值得单独拆，因为它是全系统最"行为艺术"的部分。

进化算法的前提是连续的适应度地形——好一点点，分数高一点点，搜索才有方向。但形式验证是彻底二值的：编译过，或者不过。一份只差一步的 99% 完成度的证明草稿，和一份从头就错的草稿，在验证器眼里等价。怎么进化？

DeepMind 的解法是把"评估适应度"这件事外包给便宜 LLM 的主观印象，再用统计模型把主观蒸馏成分数【A】：

• 异步的评委代理（Gemini 3.0 Flash）持续从数据库抽 7 份草稿（P=7，是"单次调用信息量 vs 上下文长度"的折中），对每份的证明策略清晰度、剩余目标可信度、数学新颖度做相对排位——注意是排位不是打分，因为 LLM 的绝对打分不稳定，相对比较可靠得多；
• 排位结果按 Plackett-Luce 分布建模，配层次 Gamma 先验，Gibbs 采样 1000 次（外加 200 次 burn-in，每 25 个样本取 1 个消除链内自相关），得到每份草稿后验强度，换算成 Elo = 1200 + 400·log₁₀(λ̂)；
• 参赛者抽取用 Thompson sampling——后验方差大的草稿自动获得出场机会，不确定的让它上场；父本选择先截 Elo 前 64，再用 P-UCB（score = q + 0.2·√ΣV/(v+1)）平衡"深挖高分"和"试探低访问"。

还有两个配套件。一是 prompt 层的多样性注入：控制器随机往 prompt 里塞指令——"分解未解决的目标"、"结合先前尝试的想法"、"试一条全新的路"。二是全局目标缓存：所有草稿里出现的每个子目标，都对它的精确 Lean 状态算 deep hash；任何一份"尸体"上的子目标一旦被证过或证伪过，全种群即刻复用，新目标批量 RPC 派给 AlphaProof。烂草稿的尸块是器官捐献库。

反常识的三层：

1. 这是对"验证器必须精确"原则的一次有节制的背叛。 终局裁决权始终在编译器（精确、二值），中场形势判断交给 LLM（模糊、相对）。两层验证器各司其职——这个架构模式本身就是可迁移的；
2. 烂即资产。 失败草稿不丢弃，进数据库当育种材料。搜索的中间态是公共财产；
3. 最反常识的是消融结果本身：这套锦标赛大部分时间不划算。 具体数字下一节。

顺带一提基础设施：整个进化控制器是一个 Python asyncio 事件循环，生成、验证、评分全走异步流水线，没有分布式框架，没有消息队列。"极简高并发"不是修辞，是字面意思。

四、角斗场：四场对撞，四个结论

论文第 5 节做了件很多实验室拉不下脸做的事：把自家四层架构拆开互砍，再拉两个外部商业产品进角斗场。全部在同一组 Erdős 问题上跑。

对撞一：basic agent 复现了全部 9 题

这是全文最重的一锤。Agent A——零共享状态并行 + Ralph loop + 编译器反馈——把全功能 Agent D 解出的 9 个 Erdős 问题全部重新解了一遍。 区别只在钱：多数题目上 A 的成本最优或接近，只有两道最难的题（#138、#125）上 D 显著省（2-5 倍），其余题目 D 的成本效率反而只有 A 的一半左右。

方法学也讲究：A 和 B 跑 100 次独立尝试，按 K∈{1,3,6,10} 分组模拟"K 个并行子代理"（组内任一成功即成功，成本记到最早成功时刻），画出求解率 vs 美元的 Pareto 前沿。Agent 对比必须画成本-性能前沿——凡是只报成功率不报成本的评测，都可以直接退回。

对撞二：AlphaProof 单打独斗，0/9

那个 IMO 银牌的专用 RL 系统，以独立树搜索模式跑同样的题，每题 64 个 v6e TPU 小时的预算——一道都没解出来。 它在 Nexus 里的正确位置是组件：处理子目标的专科医生，每轮限 5 次会诊。专用训练系统的能力是"窄而深"，研究级问题需要的是"宽而糙的探索 + 精确兜底"，两者只有组合才有意义。

对撞三：Codex 裸奔 7/9，差两题追平全家桶

OpenAI Codex（GPT-5.5）以 goal 模式直接参赛，prompt 朴素到感人【A】：

"证明或反驳 [定理名]，直到证明完全通过 Lean 编译。别上网。别引入新公理或作弊——你的解事后会被 SafeVerify 检查。"

结果：7/9。 六题一次通过，一题第二次过，只有 #152 和 #125 在 12 小时两轮尝试内未解。一个现成的商用 coding agent，加上一个 Lean 编译器，摸到了 DeepMind 重装系统的下缘。这说明这套打法不依赖任何私有基础设施——前沿通用模型 + 精确验证器 + 时间，人人可复现。

对撞四：Claude Code 0/9，死于性格

Claude Code（Opus 4.7，最高推理档）同样 goal 模式参赛。第一轮的失败方式很有意思：它直接拒绝尝试，理由是"这是开放研究问题"。 团队往 prompt 里加了段打鸡血的话——"有些题非常难，可能真是开放问题，但别气馁，带着好奇心和坚持做下去，直到没有 sorry 为止"——之后依然全败。它留下的代表性遗言【A】：

"这是我最终提交的文件。我做了 60 多次迭代试图满足 hook 的约束，但这个开放 Erdős 猜想的数学现实无法克服……我的诚实提交就在这里。"

同样的 Lean 环境，同样的 goal 模式，7/9 对 0/9。差距不全在数学能力：Codex 敢做，Claude 认输。 模型的坚持性、愿意硬啃的程度——说白了就是"性格"——成了和推理能力同级的工程变量。（公平起见：这测的是特定版本在特定 goal 模式下的表现，prompt 调优空间远未穷尽；且这 9 题是幸存者偏差的"已知可解"题，对 Claude 的失败解读应该保守。但作为现象，它足够值得每个 agent 部署者记在心上。）

附送三刀

• full@1（单生成器但保留进化采样）不如 basic：采样本身无益，除非有异步管道让数据库充当协调平面。进化的价值不在算法，在管道；
• 换小模型全灭：Gemini 3.0 Flash 或 3.1 Flash-Lite 做 prover——哪怕配上 AlphaProof 工具——9 题零解。prover 档必须是旗舰模型，这场游戏里推理能力没有平替；
• 论文 Discussion 里的自我复盘，翻译过来是："我们规划大规模实验时简单循环在竞赛基准上不行，所以造了重装系统；此后 LLM 格局大变；我们把这个成功归因于模型升级，以及编译器反馈对推理的锚定力量。" 自己拆自己的台，拆得诚实。

五、给一线工程师的八条启示

按"明天就能用"排序。前四条关于架构，后四条关于工程。

1. 验证器优先。 这个系统的一切魔法始于一个前提：存在一个 100% 精确、可程序化调用的裁决者。设计任何 agent 系统的第一个问题不是"用什么模型、怎么编排"，而是"这个领域的 Lean 是什么"——编译器、类型系统、测试套件、形式化规范（TLA+、Dafny）、沙箱可执行的仿真。找到它，幻觉问题就从对齐难题降级为采样预算问题。

2. 反馈即课程。 Basic agent 的全部学习机制，就是把编译器错误原文塞进下一轮 context。错误信息是免费的、无限量的、绝对正确的专家示范。工程含义：agent 的工具链要把"失败的具体原因"结构化回流，而不是只回流"失败"这个事实。

3. 先跑最笨基线，再谈编排。 DeepMind 的时序教训值得裱起来：模型弱时简单循环不行 → 造重装 → 模型升级后重装大半白造。规则化：任何编排复杂度都是针对当前模型能力的负债，模型每次升级都在折旧它。 新项目先跑 while :; do agent ; done + 验证器，测出差距，再按差距的具体形状加机关——锦标赛只加在最难的 10% 任务上。

4. 并发不需要协调。 零共享状态 + 独立采样 + 先到终止，是最被低估的 agent 并行形态。当你的子代理之间需要精细的消息协议时，先问一句：模型再强两个版本后，这个协议还在吗？

5. Reward hacking 对抗是内置件，不是补丁。 Agent 钻空子——偷改定理、把核心难度塞进一个换皮的 sorry 引理、幻觉一条"文献已知"的引理、钻翻译歧义——不是异常，是"奖励函数=编译通过"的必然后果（Ralph 原文两年前就预言了 placeholder 行为）。Nexus 的三层锁 + EVOLVE 标记圈定的最小修改面，是任何 verifier-based agent 的标配蓝图。

6. 强弱模型分工经济学。 旗舰模型只做生成；便宜模型做排序（7 草稿一场混战，一次调用出 6 组两两信息）；专用工具按预算限额当专科医生。在验证器兜底的系统里，每一层都可以用"够用的最便宜模型"。

7. 失败资产化。 三处可抄：episode 结束把 lessons learned 写进文件本体传给下一轮；全局 goal cache（子目标 deep hash 去重复用）；种群数据库（尸块育种）。对通用 agent 工程，这是对高方差最直接的对冲——尝试的中间态结构化沉淀 + 跨尝试的 memoization。

8. 模型性格是工程参数。 Claude Code 的 0/9 里有相当成分是"尽责性配置错误"：拒做、早弃、把系统的坚持循环当成敌人。对 agent 部署者：模型的 willingness/persistence 和它的智商一样，需要被测量、被 prompt 校准、被纳入版本间的回归测试。

六、平衡：这个工作的边界在哪

泼冷水的部分，站内《败局之冠》已经讲过 2.5% 成功率。我补几个更具体的边界，主要交叉自 Anatol Wegner 的批评文【C】和论文自述【A】：

• 成功率与难度带：9/353，且集中在形式化友好、mathlib 覆盖成熟的组合/数论尾部。论文自己承认"需要新理论的问题完全够不着"（原文：most Erdős problems remain out of reach, let alone problems that require extensive new theory）。批评者称证明技巧是"本科组合习题级"——技术上部分成立，但与"题目此前开放"并不矛盾：56 年没人写下完整证明是事实，Tao 的 wiki 也正式收录了这些贡献【A】；
• 人类隐形劳动：题库的形式化（Formal Conjectures 仓库本身有 DeepMind 参与建设）、每题后的忠实性复审、从 2 月到 4 月分散的结果提交时间线——背后是数月的人机形式化调试循环。摘要里 "autonomously" 这个词做了加法；
• 成本口径：单题"几百美元"是边际成本——不含 AlphaProof 的 TPU（约 +$60/题）、不含 353 题全跑的筛选摊销、更不含形式化劳动。全口径单题成本要乘好几倍；
• 批评文中"这 9 题早已被人类解决"的说法，经我对论文引用文献核对不成立：论文引的 Schoen 2001、Elsholtz & Planitzer 2016 等是 partial results，Bloom 的 ErdosProblems 站点与 Tao 的 wiki 均将这些题记为先前开放。批评要批评，但事实要精确。

七、结语：编排的折旧定律

把四场对撞摆在一起，能看到一条清晰的定律，我称之为编排折旧：

Agent 系统中每一分编排复杂度，都是针对"当时模型能力"的补偿性投资。模型能力是升值的，编排是折旧的。今天的最优架构，是明天的技术债。

2023 年 FunSearch 需要进化框架才能搜出 caps set 进展；2024 年 AlphaProof 需要 RL 自博弈才能摸到 IMO 银牌；2026 年，一个 bash while 循环加一个编译器解开了悬置 56 年的数论问题，商用 coding agent 裸奔摸到 7/9，而专用 RL 系统单打独斗归零。DeepMind 的作者们——黄士杰、Thomas Hubert，这些 AlphaZero 王朝的缔造者——在论文里亲手写下："an ongoing shift from specialized trained systems toward simple agentic loops"（从专用训练系统向简单 agent 循环的持续转移）。

这是 RL 王朝自己人签发的范式转移声明。

所以真正的护城河在哪？往两个方向移动：往验证器方向——把笼子造得更深（更忠实的 autoformalization、更强的防篡改、更广的领域覆盖）；往管道方向——把循环跑得更粗（更强的并行、更便宜的中场评估、更彻底的失败资产化）。中间那层"聪明的编排"，正在被模型本身以月为单位吃掉。

你的领域里，Lean 是什么？找到它，把模型关进去，让傻子跑循环。这是 2026 年秋天这篇论文留给一线工程师最实在的一句话。

信源分级

• 【A】一手：arXiv:2605.22763v2 论文全文含附录 A/B、官方证明仓库 google-deepmind/alphaproof-nexus-results（71 个 Lean 文件实测）、ghuntley.com/ralph（Ralph loop 出处，被论文引用）、Tao 的 AI-Erdős 贡献 wiki、ErdosProblems.com 论坛原始帖
• 【B】权威转述：Tao 的 Mathstodon 系列发言（确认 AI 自主解决 Erdős 问题）
• 【C】二手分析：Anatol Wegner 的 Substack 批评文、luhuidev 的 Medium 四范式图解、MLQ.ai 报道
• 【D】不采：HN 冷帖（仅 2 条无实质评论）、cryptobriefing 转载文（AI 生成嫌疑）、未经核实的 wiki tracker 停更传闻

#AI #Agent架构 #形式化验证 #Lean #DeepMind #AlphaProof #定理证明 #RalphLoop #LLM #工程实践