h1: A Taste of the Bitter Lesson in Automated Theorem Proving 精读

论文链接：h1: A Taste of the Bitter Lesson in Automated Theorem Proving 发表时间：2026年10月 机构：FAIR at Meta + EPFL + CERMICS ENPC（巴黎综合理工学院）+ NYU 四机构合作；三位作者（Skander Moalla、Niket Patel、Julia Kempe）标注 †Work done at Meta——学生与博后在 Meta 驻场完成工作，属于典型的「企业定义问题与提供基础设施、高校力量攻坚」产学研结构。资深作者 Rémi Munos 与 Julia Kempe 为 FAIR 资深科学家。 领域标签：cs.LG / cs.AI / 自动定理证明（ATP）/ Agent / Harness 设计

一、论文背景

1.1 什么是自动定理证明（ATP）与 Lean

要读懂这篇论文，需要先理解它所处的领域。数学证明的验证传统上依赖人类同行评议——耗时且可能出错。形式化定理证明提供了一条另一条路：把数学命题和证明写进证明助手（proof assistant），让机器逐行检查每一步逻辑。论文使用的是其中最流行的 Lean 4：数学家在 Lean 中写下「定理 + 证明」，编译器检查通过即意味着证明在逻辑上无懈可击，不存在「AI 一本正经胡说八道」的空间。

与之配套的是 Mathlib——一个由社区维护的大型形式化数学库，相当于「已经写好并验证过的数学知识库」，里面有序引理被逻辑链织成依赖图，后来者证明新定理时可以引用。证明开发过程中，编译器会显示 open goals（剩余待证目标），告诉作者「还差什么没证」。

自动定理证明（ATP） 就是让 AI 自动完成上述证明过程。为什么它重要？论文给出直接动机：前沿模型已经开始产出研究级数学，但其自然语言论证难以验证——把 AI 生成的数学变成机器可检查的形式化证明，已成为自动化科学发现的关键环节（OpenAI 的 Navier–Stokes 工作、Anthropic 的费马大定理形式化都属此类）。

1.2 什么是 Harness、测试时扩展与苦涩教训

Harness（挽具/挽架） 指模型外围的一切：工具、上下文与控制循环。好比马车与马：模型是马，harness 是挽具，决定了马力如何转化为前进。近年 ATP 领域的 harness 越来越复杂——规划（planning）、分解（decomposition）、多 agent 编排、专用证明器调度，统统被人类写进代码里。

测试时扩展（test-time scaling） 指在推理阶段投入更多算力以提升效果：多次采样（pass@k）、更长的思考链、更久的迭代修复。s1 论文的「预算强制」（在思考末尾追加 Wait 让模型继续想）是单链条版本的代表。

苦涩教训（The Bitter Lesson） 是 Richard Sutton 2019 年的著名论断：70 年 AI 史反复证明，能随算力扩展的通用方法（搜索与学习）最终胜过依赖人类领域知识的方法。国际象棋、围棋、语音、视觉无一例外。人类知识短期内有效且令研究者满足，长期却会遭遇平台期甚至阻碍进步。

1.3 领域现状与核心矛盾

论文观察到一个分裂：非形式化数学（自然语言推理）的进步主要来自扩展前沿模型的思维链与 agentic 推理；形式化证明却越来越依赖模型外围的人工工作流。为什么？因为形式证明的中间步骤可被机器检查，天然支持结构化搜索——这诱导研究者把搜索结构硬编码进 harness。

问题在于：这些新工作流的成绩往往与更强的模型、更多的算力混在一起，无人知道在匹配模型、匹配预算的公平对比下，人工工作流到底贡献了几分。如果前沿模型本身已具备推理与 agentic 能力，简单循环加上足够算力能否匹敌精巧工作流？这正是论文标题所说的「harness 设计维度的苦涩教训之问」。

二、论文定位和关联工作

2.1 研究谱系一：训练专用证明器（本文的对照面）

从 GPT-f、HyperTree Proof Search 到 LeanDojo 系，早期 ATP 主流是训练更好的证明模型——预测 tactic、生成整段证明、用强化学习磨砺。AlphaProof 用 RL+搜索达到奥赛级别，Seed-Prover 1.5 靠经验学习登顶多个榜单。这类工作贡献的是模型而非 harness，论文只在固定语句上与其报告分数对比（如 FC100-solved 上 h1+Gemini 3.1 Pro 以四分之一预算追平 DM prover agent 的 66 题）。

2.2 研究谱系二：围绕通用模型的人工工作流（本文的直接对比对象）

• Goedel-Architect（普林斯顿，arXiv:2606.06468）：先让模型生成「蓝图」（定义与引理的依赖图），再派多个证明器并行攻克各引理节点，失败则修订蓝图，一次尝试允许至多 16 轮蓝图修订；
• AlphaProof Nexus（APN）（DeepMind，arXiv:2605.22763）：进化式搜索管理证明草图，LLM 评分器 + 并行证明器 + RL 训练的 AlphaProof 协同；
• MerLean：递归分解循环；Numina：通用编码 agent + 非形式化证明器 + 讨论伙伴多模型工作流；OpenGauss：用指令文件给通用 agent 规定「规划-证明-审查-再规划」流程。

2.3 研究谱系三：简单循环（本文的同类与基础）

最近出现了只提供反馈、维持工作的简单循环：AxProverBase（Axiomatic AI，ICML 2026）证明了极简 agent 已有竞争力；APN basic 是 Nexus 的单 agent 版（DeepMind 自己的消融发现它能通过重复采样帕累托支配完整系统）；Humanfia 用编码 agent + 外部审查循环解掉 PutnamBench 全部 672 题；软件工程领域的 Ralph loop（Geoff Huntley）用一行 bash 把同一个 prompt 无限喂给编码 agent 直到验证通过。h1 明确声明构建在 APN basic、AxProverBase 与 Ralph loop 之上。

2.4 本文定位

论文是首个在「匹配模型 + 匹配预算」成本核算下、跨 5 个基准与开放问题的大规模简单循环 vs 专门工作流实证（53 页），也是第一个把 pass@1 预算曲线与 pass@k 的深度-广度权衡摆上台面的工作。

三、问题定义

3.1 从具体场景到抽象问题

具体场景：给定 Lean 定理语句与预算 B，用什么 harness 让前沿模型解出尽可能多的题、花尽可能少的钱？

论文的深层洞察是识别出被领域惯例掩盖的三个混淆变量，把问题还原为一个受控实验设计问题：

1. 模型与 harness 的混淆——新系统的成绩提升究竟来自架构创新还是新模型？必须固定模型比较 harness；
2. 「一次尝试」语义的混淆——Goedel-Architect 的一次尝试含 16 轮蓝图修订，AxProverBase 的一次含 50 轮迭代，都叫 pass@1，实际算力天差地别。必须改用美元成本作为统一算力度量（输出 token 最多比缓存输入贵 100 倍，光数 token 不够）；
3. 深度与广度的混淆——pass@k 只是「每题 k 次固定预算尝试」，而单次尝试可随预算延长。pass@1 不是常数而是一条随预算增长的曲线，深度（延长一次）与广度（重复多次）之间谁划算，是此前从未被系统度量过的权衡。

3.2 形式化定义

• 给定：定理集 D、模型 M、harness H、每题预算上限 B；
• 求解：预算约束下的解题数与成本曲线——解题数 = ai ≤ B 的题目数（ai 为题 i 首次被接受时的成本），平均成本计入失败题目（每题成本以 B 封顶）；
• 核心问题：在 M 固定、成本精确核算下，H 的复杂度（简单循环 vs 人工工作流）如何影响曲线位置？延长单次尝试与重复尝试哪条曲线更优？

3.3 抽象的精妙之处

这个定义把「harness 该多复杂」从品味之争变成可测量的问题；把「算力」从 attempt 计数统一为美元，消除了文献中最大的隐性作弊空间；把 pass@1 从单点还原为曲线，暴露了测试时扩展的完整设计空间。抽象的关键在于存在性主张 + 成本核算：由于每个被接受的证明都经形式化验证，单次运行即可确立「某分数在某成本下可达」的存在性主张——这使得论文大部分单次运行的结论在方法论上是健全的。

四、问题解法

h1 = 高效接口 + 验证器闭环 + 反思压缩，三层机制都不规定「怎么证明」。

4.1 组件一：高效 Lean 接口（类比：IDE 之于程序员）

模型通过 ReAct 循环（推理与工具调用交替）编辑一个持久工作文件。关键设计与 AxProverBase 式「整轮重写」形成对照：

• targeted edits：用 edit_working_file 做小范围字符串替换（而非重新生成整份证明），每次编辑立即编译，返回错误与开放目标；
• 预导入全部 Mathlib：工作文件天然 import Mathlib，无效 import 这类失败「从构造上被消除」（AxProverBase 42.2% 的失败编译卡在坏 import 上）；
• 可选工具集：LeanExplore 语义搜索 / Loogle 类型搜索 / grep 源码搜索 / REPL 试跑证明片段 / LSP 语言服务（悬停查类型、列目标、跳定义）。消融显示任何单一搜索工具或 REPL 即可恢复大部分增益——重要的是「能查证」，不是特定工具；
• 健壮的失败处理：瞬态 API 错误重试、Lean 超时后恢复文件，避免整个尝试因基础设施故障报废（部分 Claude Code 运行正因此失败）。

4.2 组件二：循环掌握停止权（类比：导师不让学生轻易放弃）

多轮 LLM 每轮最多 T 轮工具调用，随后必须提交。外部验证器 SafeVerify 在隔离环境中对照不可变的原始语句做核验——拒绝 sorry 占位符、新公理、native_decide 与一切作弊形式，同时支持 .disproof 形式的反证。验证器拒绝不结束任务，而是触发下一轮迭代：模型带着当前工作文件、拒绝反馈与反思摘要继续干。

这一点与原生 Claude Code 形成尖锐对照：拿到工具的 Claude Code 在 FATE-X 第 19 题上把未修改的文件重复提交了 170 次；h1 在 17 次负反馈后每次都做了修改并最终解出。「模型可以自己喊停」与「循环决定继续」是两种本质不同的系统。

详细的系统 prompt（论文附录 B 全文披露）显式防御三类失败：不许因问题「open/太难」放弃（Persistence 一节甚至讲了 Dantzig 把两道未解名题当作业解掉的故事）；不许 metaprogram 探测沙箱环境找现成答案；反证必须给出可构造的具体反例，「证不出来所以它是假的」是谬误。

4.3 组件三：反思压缩（类比：实验记录本）

每次被拒后，反思 LLM 把长 transcript 压缩为新上下文，包含：已验证的进展（具体引理名）、失败教训、下一步方向。反思 prompt 的纪律设计很细：必须以第三方口吻归因（「你曾认为……」而非断言事实，防止错误信念固化为「神谕」）；不得把放弃情绪带进摘要，只记录具体障碍；区分「被迫提交的检查点」与「声称完成的证明」。

4.4 上下文管理与成本杠杆

延续的上下文每轮从缓存重读，典型比未缓存输入便宜 10 倍、比输出便宜 100 倍。反思间隔（多少轮工具调用后压缩一次）是关键超参：每轮都反思会把缓存全部作废，200 轮不反思则遭遇 context rot（上下文腐烂，模型对超长输入的可靠性下降）。消融给出 10–50 轮的最优区间。此外提高推理努力（每轮想更深）优于多轮浅试：Gemini 3.1 Pro 高努力档解 99 题仅花 $5.34/题，低努力档 89 题花 $20.63/题。

4.5 全景

五、评估指标与实验证据

5.1 指标体系

• 主指标：成本-成功曲线。横轴每题预算（美元），纵轴解题数；模型固定时曲线位置即 harness 效率。美元成本按 token 明细（未缓存输入/缓存读/缓存写/输出）与公开牌价核算；
• 辅助指标：缓存复用率（输入 token 从缓存读取的比例）、输出 token 占成本比例、单次接受尝试的极值统计（最长 1,123 轮反思、95 活跃小时、7,124 行证明——Borsuk–Ulam 定理）；
• 消融指标：工具增删、prompt 简繁、反思间隔（1–200 轮）、推理努力档位、反思输入（全 transcript vs 蒸馏摘要）各自对解题数与成本的影响。

基准选择逻辑：PutnamBench（672 道普特南竞赛题）测效率，已近饱和；FATE-X（100 道博士资格考试级代数题）、FormalQualBench（23 道研究级定理）、FC100-solved（Formal Conjectures 中有已知解的 100 题）未饱和可分高下；Putnam 2025 与 IMO 2026 足够新、模型发布早于题目（排除基准污染）；开放问题（Formal Conjectures 236 个目标）检验超越已知解的能力。对比截止日 2026 年 8 月 27 日，全部 SOTA 主张相对该日公开结果。

5.2 核心数据

SOTA 结果（单次运行，无重复无并行）：

开源便宜模型也能打：DeepSeek V4 Flash 在 h1 中 FATE-X 解 43 题（$14.35 上限），超过专门训练的 Leanstral 1.5 发表的 34 题；FC100-solved 以 <$0.30 追平 AlphaProof 的 50 题、$4.89 达 64 题。Gemini 3.1 Pro 在 FC100-solved 以 $25 上限追平 DM prover agent 的 66 题（对方 $100 上限），$150 达 73。

匹配模型对比专门工作流：

707 题对比中仅 2 题专门工作流胜出：Erdős 125（h1 全部 16 次尝试 Lean 超时——接口限制而非循环问题）；BurnsidePrimeDegree（MerLean+Opus 4.7 以 32 节点分解 3h12m 解出，h1 十一次尝试共 $6,000、255 小时未果，但换 GPT-5.6 Sol 后 h1 解出）。FormalQualBench 上 Opus 4.8 让 h1 以 13 vs 10、$49.46 vs $118.35 反超 MerLean——下一代模型持续缩小差距，正是苦涩教训的机制。

开放问题战果（8 个）：Erdős 138/337 变体、3 个 OEIS 猜想（A108081/A211417/A022030）、AME(9,10) 量子态存在性（Open Quantum Problem 35）、Written on the Wall II 两猜想（100/314，均先修正表述后证明）。Misformalization 发现：系统通过给出短反证发现多个「形式化语句未表达原意」的缺陷，包括 Poincaré 猜想形式化缺 Hausdorff（T2）假设——非 Hausdorff 流形反例使原表述可证伪，已上游修复（PR #6008 等）。

消融：反思机制使 DeepSeek V4 Flash 从 554 升至 598 题；去掉全部工具 Putnam100 从 69 掉到 49；详细 prompt 单次尝试胜过简短 prompt 六次尝试；反思间隔 200 轮缓存 86% 但解题反降至 60/52（context rot）。

5.3 实验设计为何能证明论点

存在性主张 + 形式化验证 + 成本核算三者咬合：每个证明都被 SafeVerify 独立核验，不存在「分虚高」；匹配模型的对照把「架构贡献」与「模型进步」解耦；成本含失败题目，堵住了「只报成功成本」的口径漏洞。pass@1 曲线化则在开放问题上直接演示了「深度优于广度」的实例而非推断。

六、效果优势的根源解释

6.1 根源机制与证据链

因果链一：接口效率 → 小步行动与信息获取 → 成本与解题率

• 方法差异：targeted edit + 即时编译 + 预导入 Mathlib vs 整轮重写证明（AxProverBase 式）。【论文实验已支持】
• 机制变化：模型每一步行动后立即看到编译反馈，错误被局部化修正；无效 import 类失败从构造上不可能发生（AxProverBase 42.2% 失败编译卡于此）。【论文实验已支持：Figure 20、E.8 的 token 分解】
• 指标提升：Putnam100 同模型 69 vs 18；51 个 h1 独解题上，AxProverBase 平均每题输出 5.97M token、缓存复用 0.04%，h1 输出 0.628M、缓存 78.8%。典型题 putnam_1972_b4：AxProverBase $20.01/287 次构建，h1 $0.15/20 次局部编辑。【论文实验已支持】
• 深层解释：信息论视角——即时可验证反馈让每 token 推理都锚定在真实证明状态上，消除了「重新生成已验证内容」的熵浪费。重写式接口每轮都要模型凭记忆复现全文件，缓存全废，成本结构必然劣化。【阅读者推测：因果方向论文用 token 分解与调用计数支持，但论文自己声明未与其他设计差异完全解耦】

因果链二：循环掌握停止权 → 预算转化为持续进展 → 开放问题上的深度优势

• 方法差异：验证器拒绝强制触发新一轮（工作文件+反馈+反思摘要），模型无权自行终止；Claude Code 拿到同样工具仍可停止或被拒后放弃。【论文实验已支持：FATE-X 第 19 题 170 次重复提交 vs 17 次修改后解出】
• 机制变化：预算增长被系统性转化为「尝试-反馈-修正」循环的延长，而非浪费在重启或空转。详细 prompt 通过防放弃、防作弊条款维持循环的生产性。【论文实验已支持：Erdős 6 题上单次详细 prompt > 六次简短 prompt 尝试】
• 指标提升：开放 Erdős 问题 pass@1 82.5%@$121 帕累托支配 APN basic pass@3 与 full APN；极值统计（1,123 轮反思、95 小时、7,124 行）显示简单循环可承载远超直觉的工作跨度。【论文实验已支持】
• 深层解释：这是把 Sutton 意义上的「搜索」交给模型本身执行——工作流硬编码的分解结构是人类先验，模型自行决定何时换路、何时深挖，等于把搜索空间的结构学习内化给了模型。【阅读者推测：与新一代模型内化工作流策略的观察一致，但「内化程度」不可直接测量】

因果链三：上下文管理 → 缓存经济与 context rot 的平衡 → 同预算更多有效推理

• 方法差异：10–50 轮反思间隔 + 压缩重置， vs 每轮重置（缓存全废）或从不重置（rot）。【论文实验已支持】
• 机制变化：延续上下文使缓存复用达 74–94%（AxProverBase 至多 0.5%），输出 token 占成本从 89% 降至 34%；200 轮间隔缓存 86% 但解题反降，证明存在最优窗口。【论文实验已支持：Figure 29 与外部 context rot 研究（Chroma）一致】
• 指标提升：同等美元预算下换取更多轮有效推理；配合高推理努力（99 题@$5.34 vs 低努力 89 题@$20.63），「想得更深」优于「试得更多」。【论文实验已支持】

反事实检验：去掉反思 → 598 掉到 554；去掉工具 → 69 掉到 49；换成简短 prompt → 开放问题期望解数从 4.78 掉到 1.47；接口换回 shell 式（Humanfia）→ 同样 670 解成本 5 倍。每个组件的必要性都有量化反证。

6.2 相关工作检索与对照

围绕三条因果链，我对关键机制做了外部检索（检索时间 2026-11，来源以 arXiv 与官方页面为准）：

相反结论的检视：本次检索未发现「在匹配模型与预算下，专门工作流系统性优于简单循环」的受控反例。最接近的反向证据有两类：其一，Anthropic 多 agent 系统与 PTTS 显示在可并行/读密集任务上编排有真实增益——但这与 ATP 的写密集性质不同，构成适用边界而非反驳；其二，full APN 在 Erdős 125 上仍是唯一解出者、MerLean 曾以 32 节点分解在 BurnsidePrimeDegree 上胜出——说明极少数需要特殊结构或特殊工具（如 AlphaProof 的 RL 证明器）的题目上工作流仍有价值，与论文自己承认的「707 题中 2 题例外」一致。检索范围内未发现针对「反思间隔最优窗口」「循环掌握停止权」的独立反面研究。

6.3 综合判断与未决问题

多研究共同支持的机制：「验证器闭环 + 持续修复」的价值（h1、APN 消融、AxProverBase、Ralph loop、Kapoor 均指向同向）；「成本必须与准确率联合报告」（Kapoor 直接开创，h1 与 APN 的条件成本争议呼应）；「context rot 决定上下文必须定期重置」（Chroma 受控实验 + h1 消融）。这三条已接近「结构上必然」的地位。

仍属推测的机制：「新一代模型正在内化工作流策略」（论文从 Opus 4.7→4.8 反超 MerLean 等现象推断，无法直接观测训练数据）；「接口效率的因果贡献」（论文自述与同时变化的其他设计差异未完全解耦）。

适用条件：优势在「存在可靠机械验证器 + 任务写密集 + 单文件尺度」下成立。可能失效的场景：验证器不可靠或缺失的领域（开放式创作）；需要跨文件依赖管理的大尺度形式化（费马大定理、整本教科书——论文自己指出需要并行 agent 与代码库级验证）；需要专业计算工具的问题（数值模拟、网页检索）；以及对 wall-clock 时间敏感的场景（Numina 总耗时更短，h1 是串行搜索）。

未决问题（论文列出与检索发现的交集）：简单循环在万 agent 尺度（OpenAI Navier–Stokes 用了约 10,000 agent）下如何扩展；模型自建 harness（论文展望的「模型为自己部署接口」）；h1 自身的接口与工具仍是人设计的——苦涩教训是否会连这一层也吞掉；以及基准污染无法完全排除的评测学阴影。

七、必要知识反推

假设一位毫无背景的研究者要完成这项工作，最少需要掌握什么？

7.1 领域知识层

• Lean 4 证明助手与 Mathlib 的运作机制：不理解「编译即验证」「open goals」「import 环境」就无法设计 targeted edit + 即时编译的接口，更无法理解为何预导入能从构造上消灭一类失败；
• Lean 生态工具版图：REPL、LSP、Loogle/LeanExplore、SafeVerify/Comparator/AXLE 各验证器的差异——SafeVerify 的反证支持与沙箱模型正是被选中的原因；
• 形式化基准的分布与污染时间线：必须知道 PutnamBench/FATE-X/FC100 各测什么、哪些已饱和、模型发布与题目发布的先后（附录 E.10 的整张时间线图）才能设计出有区分度的实验。

7.2 方法论知识层

• 苦涩教训的原典与适用边界：不是口号式引用，而是把它转化为可检验假设——并意识到 Sutton 本人说明人机不必对立，从而把「人设计接口、算力花在推理」作为中间立场；
• 测试时扩展的既有理论（s1、Snell、Brown、Reflexion/Self-Refine）：h1 的反思机制直接站在 Reflexion 上，预算曲线视角则是对 pass@k 文献的补全；
• 评测方法论（Kapoor et al.）：成本-准确率联合优化、存在性主张的单次运行健全性、bootstrap 区间——这些决定了整篇论文的报告规范；
• 前序系统的第一手细节：必须实际运行/复现 AxProverBase、Claude Code、APN basic 才能做出「same-model rerun」的对照，光读论文不够。

7.3 工程知识层

• token 计费结构：缓存读/写、输出 token 的价差（至多 100 倍）是全部成本分析的底层；DeepSeek 本地服务无缓存计数器时需从 trace 重构估算；
• 沙箱与可信边界工程：不可变原始语句的隔离编译、提交流的网络隔离——防作弊的形式保证依赖这些工程细节；
• 失败处理的分布式系统直觉：API 瞬态重试、Lean 进程重启、从保存状态恢复——「确定性 Lean 失败连续三次计为未解」这类规则需要工程判断。

7.4 知识融合的关键节点

1. 洞察节点一：把 Sutton 的论断翻译成 harness 设计问题。需要同时理解苦涩教训、ATP 工作流现状与测试时扩展文献，三者在「模型已具备 agentic 能力，工作流是否还必要」这一点上交汇；
2. 洞察节点二：美元作为算力统一度量。需要评测方法论（Kapoor）+ 计费工程细节 + 对各前序系统 attempt 语义差异的考古，才能发现「pass@1 不可比」这个被全领域忽视的漏洞；
3. 洞察节点三：停止权外置。来自对 Claude Code 失败模式的第一手观察（模型会放弃、会重复提交），融合 agent 行为学与 SE 领域 Ralph loop 的实践智慧，才有了「循环而非模型决定停止」的设计；
4. 洞察节点四：反思 prompt 的证据纪律。把「反思摘要可能固化为错误神谕」当作对抗性文本生成问题处理（第三方归因、防放弃条款），是 LLM 行为学知识与数学工作流需求的化学反应。

八、论文中可以提取的通用性灵感

灵感一：先跑强基线，再谈架构

• 核心思想：在给系统加结构之前，先用真实预算评测「强模型 + 极简循环 + 机械验证器」的基线，避免把模型进步误认成架构贡献。
• 论文证据：Goedel-Architect 的 tool-integrated 基线 pass@32 仅 54.5%，而 h1 同模型 pass@1 达 89.0%——一个弱的简单基线足以让整个领域高估工作流必要性；Kapoor et al. 在通用 agent 基准上给出同向结论。
• 推广场景：任何有自动验证器的领域——编译通过的代码、通过测试的 CI、通过 schema 校验的数据管道、通过 linter 的文案系统、通过仿真验证的芯片设计；产品决策中的 build-vs-prompt 权衡；自动化流程设计（先问「一个强模型+检查器循环能做到哪」再画流程图）。

灵感二：验证器掌握停止权，而非模型

• 核心思想：长周期 agent 系统中，「何时停止」应由外部验证状态决定，模型只负责提议；被拒绝即强制进入下一轮。
• 论文证据：同模型同工具的 Claude Code 解 63 题而 h1 解 83 题，差异在循环控制；FATE-X 第 19 题 170 次重复提交 vs 17 次修改后解出。
• 推广场景：自动化运维（部署未通过健康检查就自动回滚重试而非报告完成）；法律/合规文档生成（校验规则不过即重写）；科学计算（数值结果不满足守恒律即继续迭代）；任何「模型自我评估不可靠但有客观检查器」的生产流程。

灵感三：把 pass@1 从常数变成曲线——深度与广度是预算分配问题

• 核心思想：单次尝试允许延长时，测试时算力的分配空间从「重复几次」扩展为「深度-广度权衡」，且深度常被低估。
• 论文证据：开放 Erdős 问题上 h1 pass@1 达 82.5%@$121，优于自身 pass@3（需 $202 达同率）与 APN basic pass@3；Gemini 3.1 Pro 高努力 99 题@$5.34 完胜低努力 89 题@$20.63。
• 推广场景：代码生成（一次深迭代 vs 多次并行采样+选择）；漏洞挖掘（一条路径深挖 vs 广撒网）；定理/证明助手调参；任何「单次成功率不低但重试成本高」的任务。

灵感四：缓存经济与 context rot 共同决定 agent 的成本结构

• 核心思想：长周期 agent 的最优上下文策略是「在一个上下文里工作到缓存收益吃满、在退化前压缩重置」，两个约束夹出最优窗口（论文中 10–50 轮）。
• 论文证据：h1 缓存复用 74–94% vs AxProverBase 0.5%，输出占成本 34% vs 89%；200 轮间隔缓存 86% 但解题从 72 掉到 60（rot），Chroma 的 18 模型研究提供机制解释。
• 推广场景：对话式产品的会话压缩时机；长文档分析流水线的分块策略；多轮代码 agent 的 checkpoint 设计；任何 token 成本敏感的 LLM 生产系统。

灵感五：防放弃、防作弊的 prompt 是循环生产性的前提

• 核心思想：让 agent 长时间持续工作的关键不是更聪明的规划，而是显式堵死「放弃」与「作弊」两条逃逸路径，并把已验证进展结构化地传递下去。
• 论文证据：详细 prompt 单次尝试胜过简短 prompt 六次尝试；反思 prompt 的证据纪律（第三方归因、不携带失败主义）防止错误信念固化；misformalization 的发现正来自「反证需具体反例」的规则设计。
• 推广场景：客服/运维机器人的升级机制设计；自动化研究中防止 agent 用捷径骗过评测；教育场景的坚持性训练设计；任何「过程漫长且中途诱惑多」的自动化任务。

灵感六：发现 misformalization 与解题同等重要——验证「问题本身」

• 核心思想：在形式化管道中，机器验证只保证「证明了对写下来的语句」，不保证「语句表达了原意」；系统性寻找表述缺陷是独立于解题的价值来源。
• 论文证据：Poincaré 猜想形式化缺 Hausdorff 假设等一批 misformalization 被短反证暴露并上游修复（PR #6008）；Written on the Wall II 两猜想是先修表述后证明。
• 推广场景：需求工程（实现之前先验证规格本身）；数据集质检（找 label 错误比刷分更有价值）；法规/合同的机器可执行化；任何「上游表述错误会污染下游一切验证」的系统。

灵感七：企业与高校的分工结构

• 核心思想：企业定义问题、提供算力与基础设施，驻场的高校力量攻坚研究问题——h1 的三一作标注 Work done at Meta 正是这种结构的实例。
• 论文证据：四机构署名 + 通信作者在 EPFL + †Work done at Meta 标注；论文附录 H 的全量可复现披露（工具/prompt/成本核算）。
• 推广场景：产学研合作的组织设计；初创公司与高校实验室的联合培养模式；企业研究院的开放研究规范。

本精读基于 arXiv:2610.35962v1 全文（含附录 A–H）撰写。文中所有实验数值均出自论文原文；第六部分外部文献信息来自公开检索，已在表中给出可核验链接。