论文链接：ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving (arXiv:2608.26334) 发表时间：2026年8月 机构：University of Virginia、Meta AI——企业与高校合作（两位共同核心贡献者中，Wenqian Ye 为 UVA 博士生、Ziwei Guan 来自 Meta AI，Henry Kautz 与 Aidong Zhang 为 UVA 教授） 领域标签：cs.AI，形式定理证明 / 神经符号进化
一、论文背景
1.1 什么是形式化定理证明与 Lean 4
形式化定理证明指的是把数学定理和证明写进一个计算机可以逐行检查的语言里。Lean 4 是当前最主流的此类语言之一（另一个常见选择是 Isabelle），配套的数学库 Mathlib 收录了数十万行已验证的数学结果。在 Lean 里，每一个证明步骤都要通过 内核（kernel） 的类型检查——内核是极小的可信计算基，它不关心你的证明写得多漂亮，只检查每一步是否逻辑上无懈可击。通过内核检查的证明，正确性等同于数学意义上的确定。
这带来一个关键性质：反馈是二值的——Lean 要么接受一个证明步骤，要么拒绝。这既是形式化的最大优点（零假阳性），也是机器搜索的最大障碍（没有部分分）。
pass@16 是评估这类系统的常见指标：让模型对同一道题独立采样 16 次，只要有一次通过验证就算解决。它衡量的是模型「裸推理」能碰对多少题。
1.2 神经定理证明器的两条路线
用大模型做定理证明，现有工作分两条路线：
- 训练式：GPT-f、AlphaProof、DeepSeek-Prover-V2、Goedel-Prover-V2 等，把证明经验通过微调或强化学习写进模型参数。问题在于新经验要影响后续问题，必须再跑一轮训练，成本高、周期长。
- 智能体式：Draft-Sketch-Prove、Hilbert、LEAP 等，推理时用多智能体协作做分解、检索、修复。信息复用基本限于当前这道题内部。
1.3 核心痛点：递归自我改进结构的丢失
论文开篇点出一个漂亮的观察：一个证明的价值远超它的结论本身。数学史上，试图推导欧几里得第五公设的失败尝试直接催生了非欧几何；希尔伯特的判定性问题（Entscheidungsproblem）未解，但图灵对它的分析诞生了图灵机。失败与部分的证明，会留下可复用的知识。
而现有系统恰恰把这一点丢掉了：
- 经验不持久——训练式方法把经验存进参数（需再训练），智能体方法只在当前问题内复用。上一道题证出的引理，下一道题看不见。
- 反馈太稀疏——严重依赖「整道题证没证出来」的二值信号。一个证到 90% 的尝试与一个完全跑偏的尝试，在根目标的 pass/fail 判定下同样都是 0 分，已验证的 90% 进度被直接丢弃。
- 小改即废——形式证明中一个小的文本改动就可能让整份证明失效，即使大部分已验证的论证仍然正确。这让「在完整证明文本上做变异」的朴素进化方法几乎不可行。
进化搜索的前提恰恰相反：有用的结构要能从失败的候选中幸存下来、传给下一代。这就是 ProofEvolve 要解决的问题。
二、论文定位和关联工作
2.1 神经定理证明器谱系（训练式）
| 工作 | 核心思想 | 与 ProofEvolve 的关键区别 |
|---|---|---|
| GPT-f / PACT | 语言模型生成 tactic | 开创性，但经验靠再训练积累 |
| AlphaProof | 大规模内核检查的自产经验 + 强化学习，IMO 银牌级 | 经验在参数里，训练后固定 |
| DeepSeek-Prover-V2 / Goedel-Prover-V2 | 子目标分解数据合成 + RL | 同上，ProofEvolve 模型全程冻结 |
2.2 智能体证明器谱系（推理时）
| 工作 | 核心思想 | 与 ProofEvolve 的关键区别 |
|---|---|---|
| Draft-Sketch-Prove | 非正式草稿引导形式化 | 单问题内，无跨问题记忆 |
| Hilbert | 递归分解难题 + 修复失败证明 | 同上 |
| LEAP（最强基线） | AND-OR 证明 DAG，分支间共享中间引理 | 记忆绑定当前目标，题一换就清零 |
| COPRA / Aristotle / ReAct | 多智能体 tactic 执行 / IMO 级证明 / 通用推理循环 | 均为问题内搜索 |
2.3 符号知识进化谱系
FunSearch 与 AlphaEvolve 用「LLM 生成 + 自动评估 + 选择」进化程序；MAP-Elites（质量多样性优化）用行为索引存档保留多样高质量候选；LEGO-Prover 尝试增长引理库，但有研究指出存储本身不保证复用；DreamProver 是最接近的先行者——固定模型、通过 wake-sleep 抽象构建可迁移 Lean 库。形式证明上的进化此前很难做通，核心原因正是 1.3 节所述：验证二值、小改即废。
2.4 定位结论
ProofEvolve 站在三条谱系的交点上：它像智能体系统一样在推理时搜索、模型权重全程冻结；又像 FunSearch/AlphaEvolve 一样做进化选择；但把进化的对象从「完整证明文本」换成「内核验证过的证明子结构」。按 Kautz 的神经符号分类，它是 Neuro[Symbolic] 系统——符号内核与验证算子嵌入神经生成过程内部。两个独有贡献：verified closure（把二值判定变成分级适应度）与类型化 schema 重组（跨问题继承验证成果）。
三、问题定义
3.1 从具体到抽象
具体问题：怎么让定理证明器越用越强？抽象洞察：定理证明在结构上就是一场进化搜索——候选（证明尝试）经过变异（LLM 提议修改）和环境选择（Lean 内核验证）存活下来，存活的候选应该把基因（已验证子结构）传给后续搜索。
| 生物进化 / 遗传算法 | ProofEvolve 对应 |
|---|---|
| 个体基因组 | AND-OR 证明 DAG（部分证明） |
| 基因（可继承片段） | 内核验证过的闭子 DAG（定理 schema） |
| 变异算子 | 分解 / 修复 / schema 重组 |
| 环境选择压力 | Lean 4 内核的接受 / 拒绝 |
| 适应度 | verified closure ρ（分级，0 到 1） |
| 种群存档 | MAP-Elites 行为索引存档（问题内） |
| 种系基因库（跨代） | schema 库（跨问题持久） |
3.2 形式化定义
给定：固定 Lean 4 环境 $E$（含 Mathlib）、冻结的策略模型 $\pi$、目标队列 $Q$。
求：对每个良构目标 $T$，产出通过内核验证的证明项 $p$（即 $E; \Gamma_0 \vdash_K p : T$），同时让搜索积累的知识跨问题复用。
核心数据结构：AND-OR 证明 DAG $D=(V,E,r)$，根节点是原始目标，每个节点是一个 tactic 状态（待证子目标）。一条被内核接受的超边 $e=(s;s_1,\dots,s_k)$ 是一个已检查的证明构造器——父目标 $s$ 的证明归约为 $k$ 个子目标的证明（AND 关系：全部子目标要证完）；同一节点可以有多条出边（OR 关系：任选一条走通即可）。
闭合（Closed）：一个节点闭合当且仅当它存在一条出边，其所有子节点都闭合。边界是尚未闭合且无出边的节点，即待扩展的搜索前沿。
关键洞察（Eq. 5 的含义）：一个闭合的内部子 DAG 本身就是一个可复用的类型化结果——哪怕整道题的根目标还没证出来。这是后续一切积累与迁移的基石。
四、问题解法
4.1 总体架构：神经提案，符号裁决
每一步迭代中，LLM 策略 $\pi$ 提议对某个边界状态的一次编辑 $\delta$，内核通过信任转移算子裁决：
- 接受：$D' = \text{step}_K(D,\delta)$，是 $D$ 的无环扩展，新边带已检查的 realizer；
- 拒绝：返回 $\bot$，证明存档与 schema 库原封不动。
系统状态 $S_t = (Q_t, \{M_{T,t}\}, L_t, H_t)$：目标队列、每目标的 DAG 存档 $M_T$（问题内局部）、持久 schema 库 $L$（跨问题全局）、被拒提案与 Lean 错误存储 $H$（修复的原料）。只有内核验证过的转移才能改动可信部分。
4.2 三类变异算子
| 算子 | 输入 | 做法 | 输出 |
|---|---|---|---|
| 分解 decompose | 边界状态 $s$ | 模型提出一个 checked closing term，或一个带类型化中间义务的证明构造器（proposal-time 的洞必须显式变成子状态才能被接受） | 新的 AND 超边 |
| 修复 repair | 同一状态上先前被拒的提案 | 模型看到原提案、检索上下文与 Lean 错误信息，重写出错分支 | 修正后的边，仍需过同一 stepK 检查 |
| schema 重组 recombine | 边界状态 $s$ + 库中 schema | 见 4.5 节 | 单条内核检查的超边 |
4.3 verified closure：把二值判定变成分级适应度
这是论文最核心的机制创新。根验证是二值的，但一个已接受的 DAG 记录了哪些内部义务已经证明。verified closure ρ 从叶到根按反拓扑序递归计算：
- OR 节点（状态 $s$）：$\rho_D(s) = \max_{e} \rho_D(e)$（多条备选边取最大）；
- AND 边（边 $e$）：$\rho_D(e) = \sum_{s'} w_e(s')\rho_D(s')$（合取义务加权求和，权重和为 1）；
- 闭合节点 $\rho=1$，无出边的开节点 $\rho=0$。
三条关键性质：
- $\rho(D)=1 \iff$ 根闭合（Eq. 10）：ρ 到 1 等价于整题证完，不会出现假满分；
- 单调性：$D \preceq D'$ 则 $\rho(D') \geq \rho(D)$——扩展只会加分不会扣分，已验证进度永不丢失；
- 完全内核接地：ρ 只从内核接受过的子目标算出，没有任何模型自评的成分。
直观理解：ρ 是「这道题已经证明了多少」的精确度量。证到 90% 的尝试 ρ≈0.9，完全跑偏的尝试 ρ≈0.1，选择压力第一次作用在分级进度上。
4.4 MAP-Elites 存档：保结构多样性
只有适应度还不够——进化搜索容易陷入单一策略的局部最优。ProofEvolve 用 MAP-Elites 质量多样性算法维护行为索引存档：行为描述子 $b(D)$ 记录分箱的证明深度、主导 tactic 族、使用的 schema 区域；每个格子里只留一个 DAG，挑战者 ρ 更高才替换（平局卫冕者胜）。父代按 $\rho/\tau$ 的 softmax 采样。
一个例子（图 1）：个体 A 证完了「⊇」方向（ρ=0.5），个体 B 证完了「⊆」方向（ρ=0.5），个体 C 两个方向都没进展（ρ=0，被淘汰）。C 的格子被更优者占据，A、B 存活。
4.5 schema 提取与类型化重组：跨问题继承
问题内的存档随题目结束就失效了，进化要成立还需要跨问题的基因库。
schema 提取：一个闭合状态可能依赖局部变量和假设。内核检查的提取把它抽象成前束范式的一般定理——量词化自由变量、把用到的假设显式化为前提：
$$\ell: \forall x, A_1 \to \cdots \to A_m \to C, \quad E \vdash_K \pi_\ell : \ell$$任何一步抽象或核验失败就不返回 schema——库里只有真货。
类型化重组：在后续某道题的开状态 $s=(\Gamma \vdash g)$ 上，若一个类型化替换 $\sigma$ 使 schema 结论与目标定义相等，该 schema 可用。Lean 先找局部见证，找不到见证的每个前提显式暴露为新的子目标，实例化后的 schema 应用作为一条完整超边 realizer 整体过内核检查。
回到 4.4 的例子：个体 A 的「⊇」子证明与 B 的「⊆」子证明分别被提取为 schema 后，在新问题里重组——合并 A 的已验证 ⊇ 与 B 的已验证 ⊆，通过反证对称（antisymmetry）一步合成子代 D，ρ=1，整题证完。已验证成果从此前的问题流进后续问题，扩大了后者的可达搜索空间。
4.6 理论保证：不削弱形式可靠性
Theorem 1（内核接地状态不变式）：任何有限执行中，每个接受边都有 checked realizer、每个闭合节点的装配证明在 $\text{Prf}_E(s)$ 中、每个库项满足 $E \vdash_K \pi_\ell : \ell$；库单调增长；被拒提案不改变可信状态。Corollary 1：ProofEvolve 返回的每个证明都通过内核类型检查。
一句话：神经网络只决定尝试什么，内核决定什么被接受。引入进化与重组没有换取任何可靠性折扣。
五、评估指标与实验证据
5.1 指标与设定
主指标是 solve rate：基准中通过 Lean 4 内核验证的定理比例。判定「已解决」的门槛严格：最终证明须与基准 ground truth 匹配、无未解析元变量、不依赖 native_decide（其代码生成路径引入内核外的公理）、并通过受限 #print axioms 检查。三个竞赛级基准：PutnamBench（纯证明子集）、IMO-LeanProofBench（奥赛级）、CombiBench（组合数学）。所有智能体基线统一用 Claude Opus 4.8 做基座、匹配每目标预算，三次独立运行取均值——比较的是搜索方法本身而非模型。
5.2 主结果：平均解决率第一
| 方法 | Putnam (%) | IMO-Lean (%) | Combi (%) | 平均 (%) |
|---|---|---|---|---|
| Claude Opus 4.8（pass@16） | 0.0 | 0.0 | 10.0 | 3.3 |
| GPT-5.5（pass@16 最强推理模型） | 10.0 | 5.0 | 13.0 | 9.3 |
| ReAct | 35.0 | 15.0 | 27.0 | 25.7 |
| Aristotle | 45.0 | 13.3 | 40.0 | 32.8 |
| AxProver | 54.3 | 10.0 | 47.0 | 37.1 |
| Hilbert | 55.5 | 33.3 | 49.0 | 45.9 |
| LEAP | 64.7 | 36.7 | 50.0 | 50.5 |
| ProofEvolve | 71.2 | 53.3 | 49.0 | 57.8 |
三个值得注意的细节：
- PutnamBench 71.2%，超 LEAP 6.5 个点；
- IMO-LeanProofBench 提升最大：53.3% vs 36.7%，+16.6 个点——这批题最需要多引理组装；
- CombiBench 略落后 LEAP 1 个点（49.0% vs 50.0%）——组合题常靠单个显式构造/计数解决，多引理组装的用武之地小。
5.3 消融：三个变异算子缺一不可
IMO-LeanProofBench 60 题、同基座同预算、5 个随机种子：
| 配置 | 解决数（/60） | Basic | Advanced |
|---|---|---|---|
| 完整系统 | 32 | 22/30 | 10/30 |
| 去分解 | 11 | 9 | 2 |
| 去重组 | 14 | 11 | 3 |
| 去修复 | 9 | 7 | 2 |
每个算子拿掉都掉一半以上，且 Advanced 难度块降幅更大。去修复掉得最狠（32→9）：Lean 错误信息是最宝贵的学习信号，没有修复循环，一次拒绝就断了一条路。
5.4 库贡献的隔离测量
受控组合族：每个后续目标由前面目标建立的引理构成（依赖结构已知）。库增长模式解决 19.8%，每题前重置库只解决 7.3%——增长库解决 2.7 倍的目标，其余组件全部固定。这个实验干净地隔离了跨问题继承这一个机制。
真实定理（Lean Workbook）：库 = Qwen3.5-397B-A17B-FP8 在 9,968 条源流定理上自产的 5,546 条内核接受证明；评估集 = 与库完全不相交、经五个 LLM judge 屏检的 744 条定理。检索进上下文后单次整证明尝试（关闭 DAG 存档、分解、修复与 ρ 选择，纯测库本身的贡献）：
| 条件 | solve rate | 提升 |
|---|---|---|
| zero-shot | 49.5% | — |
| 相关检索 K=8 | 53.4% | +3.9pt |
| 同库随机检索 K=8 | 49.6% | +0.1pt |
| 相关检索 K=64 | — | +5.3pt |
随机检索对照是点睛之笔：收益来自「选中有用的验证工作」，而不是往 prompt 里塞示例。另一个数字：相关检索新关掉的 351 个定理实例中，91.7% 的接受证明不逐字复现任何所示证明——库提供的是可复用证明结构，不是答案目录。
5.5 测试时预算扩展
8 个开源模型配置（Qwen3.5-397B/3.6-35B 各两种模式、GLM-5.1、Kimi-K2.6、gpt-oss-120b 两档推理力度），预算从 0.25×（3 次模型调用/15 次 Lean 调用/100K token/450 秒）扩到 2×（24/120/800K/3600 秒）：7/8 配置的内核验证转换数单调增加（唯一例外是低推理力度的 gpt-oss-120b，全程持平——说明趋势不只是多发几次调用）；解决目标并集从 2 增至 10。
5.6 可靠性
400+ 次独立复验（冻结 Lean 4.29.1 + 匹配 Mathlib commit，#print axioms 逐一枚举公理依赖），0 假阳性。所有证明只依赖标准三公理（propext、Classical.choice、Quot.sound）。开源模型跑出的 158 条自建引理库在复验时整体内联检查，公理足迹与直接用 Mathlib 相同。
六、效果优势的根源解释
6.1 baseline 为什么有效，以及它的根本局限
LEAP 是最强基线不是偶然：AND-OR 证明 DAG + 分支间共享中间引理，已经是问题内搜索的很强形态。但两个局限从机制上锁死了它的上限：
- 反馈层面：LEAP 的记忆绑定在当前目标的 DAG 分支上，选择信号本质上仍是根目标的 pass/fail。一个「已证完 3/4 个关键引理」的失败尝试与「全无进展」的失败尝试在二值判定下等价，选择压力无法区分它们——进化算法最需要的梯度信息在根目标证出前一直是零。
- 记忆层面：题目一换，前一道题验证过的所有结构清零。每道题的可达搜索空间都从 Mathlib 的原始边界起步，系统没有越用越强的通道。
6.2 因果链一：verified closure 让选择压力作用于分级进度
方法差异：ρ 把内核对每个子目标的逐条接受记录，沿 DAG 聚合成连续适应度。机制变化：两个未完成的尝试现在可以排序——ρ=0.9 的候选优先成为父代、其格子优先保留。瓶颈缓解：进化选择不再等整题证完才获得信号，而是在每一次内核接受后就获得部分信用。指标体现：论文图 2 的 ρ 轨迹显示，解出的运行阶梯式升至 1（每次引理被内核认证就上一个台阶），失败的运行在 1 以下平台化，而二值信号在证出前始终为 0——分级与二值的信息差全程存在。单调性保证（扩展不扣分）进一步意味着中间进度一旦验证就永久保值，进化只有前进方向。
6.3 因果链二：schema 库让早期成果扩大后期搜索空间
方法差异：闭合子 DAG 经内核检查的抽象进入持久库，类型化重组把它作为单条超边接入后续证明。机制变化：后期问题的搜索不再从零开始——一个此前验证过的结果在新目标处匹配成功，就是一步内核检查的扩展，等价于直接跳到前人（包括此前的自己）停下的地方。瓶颈缓解：LEAP 每题重置的搜索空间边界，在 ProofEvolve 里随库单调外推。指标体现：受控组合族 19.8% vs 7.3%（2.7 倍）直接量化了这个机制；类型化重组整体过检的设计还保证迁移不削弱可靠性——检索错了顶多匹配失败，不会污染可信状态。
6.4 两条链汇合：为什么 IMO 基准提升最大
IMO 级证明通常需要从多个引理组装（论文正文的示例就是 4 个引理 L1–L4 逐个被内核认证、ρ 逐级上升至 1 的过程）。这种结构同时最大化两个机制的收益：分级选择在多引理的部分进度上信息最丰富（每个引理都是一个台阶）；schema 复用在多引理组装时复用机会最多。Putnam 题（+6.5pt）引理组装需求居中；CombiBench 常靠单个显式构造（例表里多个证明只有 1–4 次转换），两个机制的用武之地都小，所以落后 LEAP 1 个点。提升幅度随问题可分解度的排序，与机制的预测完全一致——这不是凑巧好，是结构上必然好。
6.5 反事实证据
消融给出直接反证：去重组 32→14（跨问题继承砍掉一半多成绩）、去分解 32→11（没有分解就没有可积累的子结构）、去修复 32→9（错误信号不通，搜索极其脆弱）。库研究里随机检索 +0.1pt vs 相关检索 +3.9pt，反证收益来自「选中有用验证工作」这一步本身。CombiBench 上不占优则诚实地划出了方法的适用边界：单构造类问题里分级进度与复用的杠杆都短。
七、必要知识反推
假设找一个没有任何背景的人重做这项工作，他最少需要知道什么？
7.1 领域知识层
- Lean 4 / Mathlib 的运作机制：tactic 状态、元变量、elaboration 错误、内核类型检查、#print axioms——不理解这些就无法定义 stepK 转移算子，也无法把「闭子 DAG 是可复用结果」（Eq. 5）这个关键洞察落到实处；
- 证明的结构性质：AND/OR 分解关系、反证对称等组装模式——这决定了行为描述子和重组算子的设计空间。
7.2 方法论知识层
- 进化算法与 MAP-Elites：变异-选择循环、质量多样性、行为索引存档——没有这套词汇就不会想到用「格子保留最优」来防策略坍缩；
- 神经定理证明研究脉络：训练式与智能体式各自的记忆存放位置（参数 vs 当前问题）、LEAP 的分支共享边界——精确定位「验证进度不跨问题存活」这个缺口，是提出问题的前提；
- 神经符号分类（Kautz taxonomy）：知道 Neuro[Symbolic] 的含义，才能把方法放进正确的理论坐标系。
7.3 工程知识层
- 大规模验证基础设施：Lean 4.29.1 冻结环境、pantograph 交互、B200 集群（最多 224 块 GPU 并发）上 vLLM/SGLang 部署多种开源模型——没有这层，预算扩展实验无从谈起；
- 严格评估设计：native_decide 排除、公理白名单、400+ 独立复验、屏检防泄漏、随机检索对照——形式领域的论文，评估 rigour 直接决定可信度。
7.4 知识融合的关键节点
三个化学反应点：(1) 进化生物学 × 形式验证——意识到「部分验证的证明 = 可存活的基因」，把欧几里得/图灵的历史叙事变成 Eq. 5 的数学表述；(2) 质量多样性 × DAG 结构——把 MAP-Elites 的行为空间落到证明深度/tactic 族上，多样性第一次在形式证明里有了操作定义；(3) 遗传算子 × Lean 类型系统——schema 的前束抽象 + 类型化替换 + 残留前提暴露为子目标，让「杂交」变成一条内核可检查的超边。三处融合的共同约束是：任何一步都不能绕过内核。
八、论文中可以提取的通用性灵感
灵感一：把二值反馈改造成分级适应度
核心思想：当环境只给 pass/fail 时，检查环境判定过程中留下的中间产物，往往能重构出有方向的梯度信号。论文证据：ρ 从内核逐子目标的接受记录聚合而来，解出运行阶梯升至 1、失败运行平台化，二值信号全程为 0；消融中去掉依赖此信号的分解/修复掉到 11/9。推广场景：代码生成（编译通过的函数比例作为部分分）、智能体任务（完成的子目标数）、硬件设计（通过的部分规格约束比例）、法律文书审查（已核验的条款占比）、科学实验（复现成功的子流程计数）。
灵感二：验证子结构，而不是验证完整工件
核心思想：大工件的小改动会整体作废，但已验证的子结构可以幸存并被重组——把进化单位从「整件」缩小到「可独立验证的构件」。论文证据：「小改即废」正是此前形式证明进化做不通的原因；ProofEvolve 证明 91.7% 的新解不逐字复现所示证明，库提供的是结构不是答案。推广场景：软件工程（接口验证过的模块跨项目复用）、产品设计（通过测试的子装配跨产品线继承）、自动化流水线（各 stage 的验证产物持久化）、论文写作（已核实的数据段落跨稿件重组）、法规合规（已认证的子组件拼装新产品）。
灵感三：显式外部库优于参数记忆，用于零训练的持续学习
核心思想：把学到的东西放进可检索、可审计的外部结构（schema 库）而不是模型参数，能让冻结的模型也具备越用越强的能力，且每一条知识都可独立验证。论文证据：模型权重全程冻结，库增长解决 19.8% vs 重置 7.3%（2.7 倍）；744 条不相交定理上自产库 +3.9pt 而随机检索 +0.1pt。推广场景：企业知识管理（验证过的事实库替代微调）、代码助手（项目私有的已测试函数库）、医疗诊断（循证结论库按适应症检索复用）、机器人技能（验证过的运动原语库）、情报分析（溯源核实过的论断库）。
灵感四：神经提案 + 符号裁决的关注点分离
核心思想：让神经网络负责发散（提议做什么），让形式化组件负责收敛（裁决能否接受），创造力的上限来自模型，可靠性的下限来自符号系统。论文证据：Theorem 1 / Corollary 1 保证任何被拒提案不污染可信状态、返回的证明全部通过内核；400+ 复验 0 假阳性。推广场景：AI 编程（LLM 写、类型系统/测试裁决）、金融决策（模型建议、风控规则裁决）、数据库（LLM 生成查询、schema 校验执行）、自动驾驶（学习规划、安全控制器过滤）、内容审核（模型初筛、政策规则终审）。
灵感五：失败尝试是资产，不是垃圾
核心思想：一个没达到最终目标的尝试，其已验证的中间成果仍有正价值；系统设计应让这些成果自动沉淀而不是随尝试丢弃。论文证据：这直接呼应论文开篇非欧几何与图灵机的历史论证；技术上体现为闭子 DAG 的提取入科（Eq. 5→Eq. 14）与错误存储 $H$ 驱动的修复算子（去修复 32→9）。推广场景：研发管理（失败项目的可复用中间件入科）、强化学习（失败轨迹中的成功子段做奖励塑形）、创业复盘（失败业务验证过的渠道/技术归档）、教育（错误答案中的正确步骤应被评分）、运筹优化（不可行解中满足的约束子集作为剪枝知识）。
灵感六：用「同库随机检索」对照来隔离机制归因
核心思想：证明收益来自机制 X 而非泛泛的「多了些上下文」，最干净的办法是保留一切、只把 X 换成随机版本。论文证据：随机检索 +0.1pt vs 相关检索 +3.9pt，一举排除「prompt 里加例子就有提升」的替代解释。推广场景：RAG 系统评估（随机检索对照分离检索质量与生成能力）、推荐系统（随机曝光对照分离推荐算法与物品本身热度）、A/B 测试设计、数据增强归因、课程设计的有效性检验。