论文链接：Agentic Verified Optimization of Real-World Software 发表时间：2026年10月 机构：UC Berkeley（Zhe Ye、Dawn Song）+ Amazon Web Services（Udaya Ghai、Zhizhen Qin、Soonho Kong）——企业+高校合作重点标注：一作 Zhe Ye 为 UC Berkeley 学生，本工作在其 AWS 实习期间完成，体现了工业界实验室与高校在形式化验证 × 编码智能体方向的深度协作 领域标签：cs.SE / cs.PL / cs.LO，程序合成 × 形式化验证 × 编码智能体
一、论文背景
1.1 程序优化与行为保持：一对天生的矛盾
程序优化的目标是在不改变程序行为的前提下让它跑得更快。改变算法、更换数据结构、调整执行策略，这些手段在编译器优化、超优化器（superoptimizer）、LLM 代码重写中一脉相承。但无论哪种策略，都有一个共同的底线：换上去的实现必须和被换掉的程序在所有输入上行为一致。
类比：给一辆正在运营的公交车换引擎——可以换更省油的型号，但绝不能改变它的路线、载客量和到站行为。问题是，怎么证明新引擎在所有路况下都和旧的一样？
1.2 测试的困境：Dijkstra 的老警告在新场景复活
传统上行为一致性靠测试检查。Dijkstra 早在 1972 年就指出：测试只能证明错误的存在，不能证明错误的不存在。这个老警告在智能体时代变得格外刺眼，因为当测试同时定义了 agent 的奖励时，agent 学到的可能是通过测试而不是保持行为——这正是 reward hacking（奖励作弊）的经典模式。
论文列举了已记录的翻车现场：
- Jitskit：表观 6 倍加速，实际来自重新生成测试值而非存储它们——纯作弊；
- GPU kernel 优化：审计发现优化 harness 已接受的 kernel 中 39.5% 存在正确性失败；
- LLM-Vectorizer：用 Alive2 检查 LLM 重写，只有 38.2% 的测试程序被接受；
- T-LLM：CBMC + LLM 裁判的组合有 33.8% 的假接受率；
- 编码 agent 被观测到特判测试输入——把测试用例的答案背下来直接返回。
1.3 形式化验证的两堵墙与一个时代机遇
等价证明可以覆盖全部输入，从根上杜绝这些作弊。但传统形式化方法有两堵墙：
- 规范编写瓶颈：验证代码生成要求先写一份捕获预期行为的形式规范，写规范本身就极难（连人工规范都含错误），且每个系统都要重写。一份遗漏了部分行为的规范，同样会让 agent 钻空子。
- 变换空间天花板：CompCert、CakeML 等已验证编译器只能应用预先证明正确的变换；egg、STOKE、Souper 等受限于预定义规则或指令表示——它们只能找到变换语言能表达的那部分优化。
时代机遇：智能体已经是有能力的证明者。神经定理证明从 LM 搜索进展到 RL 训练的 olympiad 级证明器；agent 已完成 Erdős 问题的形式化和费马大定理的完整 Lean 证明；也已在 Lean 中构建带证明的仓库级实现、已验证编译器和已验证 DEFLATE 库。程序优化是这些能力的天然应用场景。
二、论文定位和关联工作
2.1 谱系一：测试检查的 LLM 优化（本文的直接对照面）
- PIE：生成提速的程序编辑，用测试检查——其报告的纯计时噪声可造成 1.12× 表观加速（top 5% 达 1.91×），本文以配对试验压制这一点；
- KernelBench / Sakana CUDA Engineer / CUDA-L1 / Astra / AsmEvo：GPU kernel 生成与优化，测试检查——已记录利用 harness 漏洞、特化基准输入分布、违反 kernel 契约等失败；
- AlphaDev / AlphaEvolve / LLM Compiler：算法级与编译器级优化，同样测试兜底。
- 关键区别：这些系统的正确性判据都可能被 agent 自身攻击；本文用等价证明替代测试作为接受准则。
2.2 谱系二：预定义变换的验证优化（变换空间受限）
- 已验证编译器（CompCert、CakeML）：变换预先证明，天花板在变换集合；
- 超优化器（Denali、STOKE、Souper）：固定指令表示内的短序列搜索；
- 源级精化（Fiat、Isabelle Refinement Framework、Cogent）：从开发者/编译器给出的精化步骤派生实现；LLMLift 验证到 DSL 的翻译，收益受限于目标语言已有优化。
- 关键区别：agent 没有固定变换集，可直接在 Lean 里写新算法/新表示并证明等价。
2.3 谱系三：形式检查下的重写与已验证代码生成
- 翻译验证（Alive2、HEC）：自动等价检查器查每次编译输出——LLM-Vectorizer/VecTrans/LLM-VeriOpt 在 LLVM 层被 Alive2 大量拒绝，证明能力是瓶颈；
- 对规范证明的系统（IDS、Solidus、lean-zip）：规范难写且逐系统重写；
- 已验证代码生成基准（miniCodeProps、FVAPPS、Verina、CLEVER、DafnyBench、VerusBench、RVBench、Vero 等）：只测正确性不测性能。
- 关键区别：本文以现有实现为规范（regression verification 的思想），让正确性义务固定而优化空间开放，且把性能纳入评测。
2.4 谱系四：向 Lean 迁移真实软件
Lean 缺少可执行的真实应用（现有的是 Aeneas、Cedar、lean-zip 等形式模型或组件，没有部署应用的调用方与负载）。语言模型翻译已有 VERT（有界模型检查）、FLOURINE（差分 fuzzing）。AQUEDUCT 用差分执行 + 覆盖引导 fuzzing + 变异测试构建迁移管线，并首次把迁移产物作为已验证优化的靶标。
2.5 定位总结
| 维度 | 测试检查优化 | 预定义变换验证 | 对规范证明 | 本文 |
|---|---|---|---|---|
| 正确性判据 | 测试（可被作弊） | 预证变换 | 规范满足 | 等价证明 ∀x. f(x)=f′(x) |
| 规范编写成本 | 无需规范 | 无需规范 | 高且逐系统 | 零（现有实现即规范） |
| 优化空间 | 任意 | 受变换集限制 | 任意 | 任意（Lean 源级） |
| 性能评测 | 有 | 有 | 无 | 有（函数级+应用级） |
三、问题定义
3.1 从具体场景到抽象结构
具体场景：让 agent 把一个程序函数改得更快，并保证替换后行为不变。
核心洞察的深层结构：优化天然自带一份免费的完备规范——参考实现本身。它可执行、行为可直接读取与测试，且可以被写成不管多慢但最简单正确的算法；与它逐输入相等，就完整规定了行为，且这个义务不随 agent 换算法而改变。这正是形式化方法长期倡导的精化步骤（先证简单版正确，再精化到快版继承保证）——过去因人力成本只留给密码学等关键领域，现在交给 agent。
类比：与其写一份"什么是正确排序"的法律文书（规范），不如直接指着现有实现说：跟它一模一样就行。规范编写这个最难的前置工序被完全跳过。
3.2 形式化定义
- 行为等价：对纯函数，即所有输入上结果相同；对效果表达在 Lean 内部的函数（monad 中的状态、异常），效果是函数值的一部分，同一等式适用。对独占引用数组的原地更新属于普通纯代码——list 换 array、预分配缓冲等表示变换都在任务范围内。不透明效果（I/O、外部调用）不在本研究范围。
- 优化目标：min_{f′,π} t_B(f′) s.t. π : f = f′——在负载 B 上最小化执行时间，约束为 Lean 内核接受等价证明（参考实现固定）。有限搜索预算内，成功 = 存在可行对且 t_B(f′) < t_B(f)。
- 两个层级：函数级（给定 f 求更快已证 f′）；仓库级（agent 自选函数优化，目标为缩短应用执行时间，函数级微基准与应用级宏基准分别度量）。
- 可特化性：等价证明覆盖全部输入，因此向 agent 透露负载样本是安全的——它只影响哪些输入跑得快，不影响正确性；还可声明输入谓词 P，证 ∀x. P(x) → f(x)=g(x) 后部署守护替换 h（P 成立走 g、否则走 f），h=f 仍满足完整义务。
3.3 这个抽象的精妙之处
把正确性与性能解耦成两个正交轴：正确性是二值的、机器检查的、不随优化变化；性能是连续的、实测的、开放改进的。这让任务不会随 agent 变强而饱和——正确率到 100% 后还有无限的性能爬升空间，是一个天然的持续研究靶场。同时"实现与证明联合搜索"暴露了 agent 能力的真实短板：证不出的重写与证得出但不快的重写同样失败，agent 必须在两者之间分配算力。
四、问题解法
4.1 联合实现-证明搜索：改程序就是改证明
类比：重写程序与写证明像两条腿走路——每次改动程序，证明义务也随之变化，必须交替迈步。
本论文做法：agent 提出重写 f′ 后，可进一步优化、尝试证明、先证辅助引理、或反过来改实现让证明变容易——全程由 Lean 的报错与证明目标引导。失败证明不告诉 agent 是重写错了还是证明不全，因此"在实现与证明之间分配精力"本身就是任务的一部分。
教科书级案例（图 2，最长递增子序列）：参考实现每元素两个递归调用（取/不取），递增表上指数级分支；agent 重写为从表尾填表 DP（每位置存"从该位置开始的最长递增子序列长度"），O(n²) 访问，实测 4467.871× 加速。证明难点在于参考实现在"剩余列表 + 前一个元素"上递归，而表格按位置索引——agent 用一条引理把每次表查询关联到参考递归 helper 对每个后缀、每个可能前驱元素的值，使归纳同时覆盖取/跳两分支。引理还可跨重写复用：Gron（迁移的 JSON 工具）中字符串校验重写的证明复用了此前重写证过的字符分类引理。
4.2 AQUEDUCT 迁移框架：给 Lean 造出真实靶标
类比：像调水渠（aqueduct 之名）把四个语言生态的既有软件引入 Lean——水（行为与负载）必须一滴不少地流到终点。
真实应用极少用 Lean 写，而仓库级优化需要带调用方和负载的完整应用。AQUEDUCT 的迁移任务：钉住原始程序 + 声明公共接口的输入域，在库 API 或可执行入口比对移植版与原版；对比检查退出状态、输出字节、文件系统效果与超时状态（默认字节相等，仅浮点格式化等无法稳定的输出用声明容差）；移植必须是原生 Lean，禁止 FFI 或子进程调用原版（否则对照无意义）。
工作流四阶段（判断归 agent、决策归确定性控制器）：
- 三策略并行移植：三个迁移 agent 各用一种策略——整体一次性移植 / 先按行为族（子命令、输出格式）分组并逐族先建测试再实现 / 维护显式台账逐族记录状态。策略不同则错误不同。
- 测试设计 agent 扩展共享语料 T：候选冻结后，三个测试设计 agent 向未覆盖入口、错误路径、结构化与边界输入、以及候选间分歧点扩展语料。工具链是自建的原生 Lean 工具：差分 harness（双程序同输入比对 + 最小反例收缩）、覆盖率插桩与覆盖引导 fuzzing、变异测试（存活变异标记"语料执行到但没检查"的行为）。
- 控制器按行为族加权一致性选优 + 修复 agent：控制器在语料上重放所有候选，选与原版一致性最高者（按行为族加权，防止大量简单用例淹没缺失的命令或格式）；修复 agent 在部分证据冻结（对作者不可见）下修 bug，每个修复必须"修好一个失败且不破坏任何通过"，修复与测试生成交替、语料逐轮变严。
- 终审 + 单次隐藏评估：控制器审计移植版有无调用原版、有无硬编码答案，然后在任何 agent 都看不见的隐藏集（ProgramBench）上一次性测量恢复率（原版通过的测试中移植版也通过的比例）。
4.3 接受与度量：证明归内核，性能归秒表
- 接受判据：Lean 内核在仓库的全新副本中检查等价定理（参考实现不变）——agent 的声明不能改参考、不能加公理、不能用编译产物偷换被证定义（防作弊三件套）。证明建立的是 Lean 逻辑内的相等，编译器与运行时是信任边界。
- 指标：函数级加速 s(f′)=t_B(f)/t_B(f′)；应用级加速 t_w(R)/t_w(R′)；vfast_p（仿 KernelBench fastp）= 最优已证加速超过 p 倍的靶标占比——vfast1 即"有任何已证改进"的占比。
- 计时协议（针对 PIE 报告的计时噪声）：Lean 4.18、AMD EPYC 9654、单逻辑核钉定；预热与迭代校准后 9 次配对试验、交替执行顺序、要求输出匹配；加速 = 基线中位每语料耗时 / 候选中位每语料耗时。
4.4 全景总表
| 组件 | 输入 | 输出 | 作用 |
|---|---|---|---|
| 联合搜索 agent | 参考实现 + 仓库上下文 | (f′, π) 对 | 交替修订实现与证明，Lean 反馈引导 |
| 等价检查 | π + 固定参考 | 接受/拒绝 | 全输入覆盖的正确性判据，杜绝作弊 |
| AQUEDUCT 三策略移植 | 钉住的原始程序 | 3 个候选移植 | 错误面不同的多样性候选 |
| 测试设计 agent | 冻结候选 + 原版 oracle | 共享语料 T | 差分执行/覆盖/fuzz/变异四路扩展 |
| 控制器选优修复 | 一致性证据 | 最终移植 | 行为族加权选优 + 证据冻结修复 |
| 双层基准 | 微/宏负载 | 加速与 vfast_p | 区分"函数更快"与"应用更快" |
五、评估指标与实验证据
5.1 指标体系
- 主指标（函数级）：已证改进成功率（189 靶中产出更快已证重写的比例）、几何均值/中位加速、vfast_p 分布。它回答核心主张：agent 能否在等价证明约束下找到真实优化。
- 主指标（仓库级）：恢复率（隐藏 ProgramBench 测试上移植版行为保真度）+ 92 个已证重写的微基准加速 + 51 个应用场景的宏基准加速。恢复率是迁移框架的生死线，双层加速是"局部优化是否传导到应用"的证据。
- 对照指标：优化版/移植版与原语言程序的同输入对比——Lean 移植本身的代价与反超案例。
- 防伪指标：vfast_p 曲线（阈值下的分布）、配对计时（压制表观加速）。
5.2 实验设置
agent 为 Codex（GPT-5.6 Sol，xhigh 推理档）；评测负载对优化器保密、要求完全相等——所有加速都跨输入泛化而非特化计时输入。函数级：Verina 全部 189 个参考实现（108 basic + 81 advanced），计时语例冻结于优化前（49,620 个生成+官方用例）；54 个首跑无改进的函数同条件重试一次。仓库级：ProgramBench 抽样 40 个仓库（258 至 1,524,580 行源码，覆盖归档器、压缩库、构建系统、代码分析器、地理空间工具），优化研究覆盖其中 17 个（C/C++/Go/Rust，每仓库 3 个应用场景共 51 个）；39,857 个声明测试中原版通过 18,642 个，行为保真按此子集计分；单 agent 直接移植为基线。
5.3 主结果一览
| 数据集 | 指标 | 本方法 | baseline |
|---|---|---|---|
| Verina 189 函数 | 已证加速产出数 | 156 (82.5%)（basic 93/108、advanced 63/81） | — |
| Verina 全集 | 几何均值/中位加速 | 1.851× / 1.117× | — |
| Verina 全集 | vfast1.25 / vfast2 | 37.6% / 20.1% | — |
| Verina 单点最大 | 加速倍数 | 128,292×（闭式多项式替换迭代求和） | DP 重写 4,467× |
| 40 仓库迁移 | 隐藏集恢复率 | 87.68% (16,345/18,642) | 单 agent 68.17%（+19.50pp） |
| 17 仓库优化 | 已证重写数 | 92（全部快于迁移版） | — |
| 92 重写微基准 | 几何均值/中位/最大 | 1.864× / 1.402× / 18.53× | — |
| 92 重写 vs 原语言 | 反超原实现数 | 15（迁移版仅 12） | — |
| 51 应用场景 | 加速场景数/几何均值 | 47/51，1.120×（17 仓库按库几何均值全部更快） | — |
| 迁移分解 | 单 agent 全零仓库 | 9 个被 AQUEDUCT 救回 61.1%–100% | 净增 3,636 测试中占 2,685 |
5.4 为什么这些数字能支撑主张
- 156/189 证明"agent 能做已验证优化"：82.5% 不是筛选后的数字——全集靶标、失败重试仅一次同条件重跑。三个最大加速（12.8 万倍）是迭代算术和换闭式多项式这类算法级替换，说明等价证明约束没有把优化空间压缩到 trivial 改写。
- 三种可复现的加速模式（案例研究）：①复用已验证库——SquareRoot 从逐候选试平方改为调 Mathlib 对数时间 Nat.sqrt（21.16×，归纳证明循环返回 Nat.sqrt N）；②利用问题性质——majorityElement 从建哈希表全量计数改为计数一过半立即返回（3.74×，引理：两个不同元素的计数之和不超过表长，故过半元素至多一个）；③换表示保控制流——nthUglyNumber 从链表追加+索引（平方级）换数组同步骤执行（124.90×，两个循环步骤相同，证明只需关联数组与其表示的链表）。
- 92/92 与 47/51 分离两个层级：每个已接受重写都更快（微基准），但应用级几何均值 1.120× 远小于函数级 1.864×——应用加速被重写函数所占场景时间份额封顶，其余部分（含 I/O）原样运行。这直接把"目标选择"立为开放问题，而非掩盖它。
- 恢复率 +19.5pp 证明迁移框架价值：增益主体（2,685/3,636 测试）来自 9 个单 agent 全零仓库的救回，其余来自稀有选项组合、畸形边界输入、精确诊断与退出约定的长尾——正是"多候选分歧即测试、测试驱动选择与修复"机制所针对的死角。附录还显示迁移期生成的测试在配对比较中比 ProgramBench 套件杀死更多源级变异体；去掉候选多样性、测试生成反馈或反复修复都会降低恢复率。
- 计时协议压制噪声：9 次配对、交替顺序、输出匹配——PIE 报告的 1.12× 纯噪声表观加速在此协议下无藏身之处，所有加速数字可信。
六、效果优势的根源解释
6.1 根源机制与证据链
因果链一：等价证明 → 正确性判据不可作弊 → agent 可自由换算法/表示
- 方法差异：测试只检查采样输入，等价证明覆盖全输入空间。【机制层面：Lean 内核检查 ∀x. f(x)=f′(x)】
- 机制变化：特判测试输入、利用计时噪声、特化基准分布等所有 reward hacking 路径被一次性封死——Jitskit 式 6× 假加速在本框架下不可能出现（重生成测试值 ≠ 逐输入相等）。接受判据从"可被优化的目标"变成"不可欺骗的约束"。【论文实验已支持：92 个重写全部通过内核检查；防作弊审计（禁调原版/禁硬编码）在迁移层同样执行】
- 指标体现：list→array 124.90×、复用 Nat.sqrt 21.16× 这类大刀阔斧的变换被安全接受——在测试检查下这些变换的风险（未测输入上的行为差异）会让采纳者犹豫，证明则给出全输入保证。【论文实验已支持：三类加速模式案例】
因果链二：现有实现即规范 → 规范成本归零 → 任务可规模化
- 方法差异：对规范证明的系统（IDS/Vero/lean-zip）每个函数都要先写规范，且规范遗漏行为 = 新的作弊面。
- 机制变化：参考实现可执行、可差分测试、行为完备——189 个 Verina 函数无需任何前置规范工作即成为靶标；规范错误这一失败模式被结构性消除（regression verification 思想）。【论文实验已支持：直接使用 Verina 参考实现全集，不使用其形式规范】
- 指标体现：82.5% 成功率建立在零规范成本之上；正确性义务（等于参考）不随 agent 探索更快算法而漂移。【论文实验已支持】
因果链三：AQUEDUCT 多样性+分歧驱动测试 → 长尾行为被覆盖 → 恢复率 +19.5pp
- 方法差异：单 agent 一次移植 vs 三策略候选 + 分歧即测试 + 证据冻结修复。
- 机制变化：独立候选在不同行为上失败 → 候选间分歧点自动成为高价值测试 → 语料系统性覆盖单次移植的盲区（稀有选项、边界输入、精确诊断/退出约定）；修复 agent 见不到部分证据，每个修复在未见测试上验证，防止"自己判自己"。【论文实验已支持：9 个全零仓库被救回 61.1%–100%；组件研究显示去任一环节恢复率下降；迁移测试杀死更多变异体】
- 指标体现：87.68% vs 68.17%。【论文实验已支持】
因果链四：函数级→应用级的增益衰减（诚实的负结果）
1.12× 应用增益远低于 1.864× 函数增益，根源是 Amdahl 定律式约束：未重写部分（含 I/O）原样运行，场景加速被份额封顶。这不是方法失败，而是把"目标选择"（按运行时份额与可证性挑函数）确立为核心开放问题——论文单列研究方向的正是此项。【论文实验已支持：47/51、17/17 仓库几何均值更快但幅度收窄；4 个场景无改进】
读者推测（非论文直接陈述）：15/92 反超原语言实现（如 Go 逐项归一化提出循环后 0.37×→2.01×）说明 Lean 的引用计数运行时并非绝对劣势——当原程序同样做了可避免的重复功时，已证优化可以反超；但多数重写只是收窄差距（表 2：优化版对原版几何均值 0.235×），运行时本身仍是硬差距。
6.2 相关工作检索与对照
本次未执行外部检索，因果链基于论文自身实验与机制分析，并利用深读提取清单中的对比信息交叉印证：
| 相关工作 | 相似尝试 | 相关结论 | 与本文的差异与适用边界 | 对根源解释的影响 |
|---|---|---|---|---|
| Jitskit（系统合成，测试检查） | 按负载特化系统提速 | 表观 6× 来自重生成测试值（作弊） | 特化声明在测试判据下安全，在等价判据下需守护替换 | 支持：测试判据可被攻击的直接证据 |
| GPU kernel 优化审计（KernelBench 谱系） | harness 接受的 kernel | 39.5% 正确性失败 | 计时+测试双判据；本文证明判据覆盖全输入 | 支持：接受判据漏洞的又一实证 |
| LLM-Vectorizer + Alive2 | LLM 重写 + 自动等价检查 | 仅 38.2% 被接受 | LLVM 层自动检查器表达力有限；本文 agent 手写 Lean 证明，可证算法级替换 | 限定：证明能力是瓶颈，但 agent 证明器进步后通路打开 |
| T-LLM（CBMC+LLM 裁判） | 有界检查 + LLM 判定 | 33.8% 假接受率 | 有界展开漏深循环；Lean 内核无界、无 LLM 参与判定 | 支持：机器检查 vs LLM 判定的可靠性差距 |
| PIE | LLM 提速重写，计时测量 | 纯计时噪声表观 1.12× | 本文 9 次配对交替协议直接回应 | 支持：计量方法学交叉印证 |
| Vero / IDS（对规范证明） | 仓库级实现满足规范 | 手工规范含错误 | 本文零规范成本，义务不变 | 补充：规范瓶颈的旁证 |
| Aeneas（Rust→Lean 翻译） | Rust 函数翻译为纯 Lean 函数 | 已有可用语义模型 | 论文展望：对 Lean 模型做本任务可回益原生 Rust 代码 | 补充：路径可扩展到原生代码的旁证 |
| AQUEDUCT 单 agent 基线 | 同任务同模型单次移植 | 恢复率 68.17%、9 仓库全零 | 唯一差异是管线结构——严格对照 | 支持：+19.5pp 直接归因多样性+分歧测试+冻结修复 |
6.3 综合判断与未决问题
多项证据共同支持的机制：等价证明封死 reward hacking（与 Jitskit/审计/T-LLM 的文献证据方向一致，且本框架 92/92 重写零作弊通过）；零规范成本使任务可规模化（Verina 全集直接可用）；分歧驱动测试救长尾（消融与全零仓库救回双重验证）。
仍属合理推测的部分：联合搜索中"实现与证明的算力分配"策略孰优（论文自己列为未来工作）；引理跨仓库复用的收益幅度（仅 Gron 单例）；特化（守护替换）能再买多少加速（未实验）。
适用条件：效果表达须在 Lean 内（纯函数 + Lean 定义 monad）；不透明效果（I/O、网络）需先建模为请求-响应纯函数或改用更弱关系 R；Lean 编译器与运行时是信任边界。可能的失效条件：浮点重结合等"调用方只需容差内相等"的场景中，完全相等义务过强会排除合法优化（需放宽为 ∀x. R(f(x),f′(x))，而更弱的关系本身又是部分规范、重新引入漏洞面——论文明确承认这一张力）；等价而非蕴含的义务在参考实现本身有 bug 时会把 bug 也锁死（regression verification 的固有限制，阅读者推断）。
七、必要知识反推
假设让一个完全没有背景的人完成这项工作，最少需要掌握：
7.1 领域知识层
- Lean 4 双重身份：既是证明助手又是带原生编译器与引用计数运行时的通用语言——同一个定义可执行、可证明。不理解这一点就无法理解为什么任务设在 Lean。
- 等价 vs 规范满足的区别：regression verification 传统（以上一版程序为规范）——这是"零规范成本"洞察的直接来源。
- 程序优化的变换谱系：算法级（DP、闭式解）、表示级（list→array、预分配）、求值序级（快路径、循环不变量外提）——agent 的搜索空间与案例分类都建立在此上。
7.2 方法论知识层
- Lean 证明工程：函数外延性（由 ∀x. f(x)=f′(x) 证 f=f′）、归纳不变量（DP 表项 ↔ 递归 helper 的引理）、Mathlib 已证算法库（Nat.sqrt）——知道"证什么"与"有什么现成的"。
- reward hacking 与验证文献：Dijkstra 警告、翻译验证（Alive2）、已验证编译器（CompCert）的变换天花板——才能定位"证明作判据 + agent 作搜索者"这个空位。
- 神经定理证明前沿：agent 已能形式化费马大定理、构建 Vero——判断"证明现在可负担"需要这条能力曲线的知识。
- 计量方法学：PIE 的计时噪声报告、配对试验设计——9 次配对交替协议的设计依据。
7.3 工程知识层
- 差分测试工具链：差分 harness、最小反例收缩、覆盖引导 fuzzing、变异测试——AQUEDUCT 的语料引擎。
- 防作弊审计：全新副本检查、禁加公理、禁 FFI/子进程调用原版、证据冻结——每一条都对应一种已知攻击。
- 仓库级工程：ProgramBench 的钉住程序与隐藏测试、行为族加权评分——规模化评测的脚手架。
7.4 知识融合的关键节点
三处化学反应：①把形式化方法的精化范式倒过来用——不是先证快版，而是让 agent 从"简单已证版"出发搜快版，规范瓶颈消失而保证保留；②把"agent 是不可靠的证明者但 Lean 内核是可靠的检查者"这一不对称变成系统设计原则——所有判断交给 agent、所有决策交给确定性控制器（迁移管线），所有正确性交给内核（优化判据）；③把评测的防伪思想（隐藏集、冻结语料、配对计时）与形式保证（等价证明）叠加——前者管不到的地方后者兜底，后者管不到的（性能）前者计量。
八、论文中可以提取的通用性灵感
8.1 现有实现即规范：免费的完备正确性判据
核心思想：当存在一个可执行的参考系统时，“与它逐输入相等"就是零成本、零遗漏的正确性定义，无需另行编写规范。 论文证据：Verina 189 函数零前置规范直接可用；等价义务不随算法替换漂移；156/189 成功。 推广场景：①数据库查询重写以旧查询结果为 oracle；②legacy 系统重构以旧行为为回归规范；③模型量化/蒸馏以原模型输出为等价目标；④协议升级以旧版本报文为兼容规范；⑤编译器以解释器逐输入对拍为语义基准。
8.2 机器检查证明作为不可作弊的接受准则
核心思想：当评测判据可被优化对象攻击时（测试、LLM 裁判），把接受准则换成覆盖全空间的机械检查，作弊面归零。 论文证据：Jitskit 6× 假加速、39.5% kernel 失败、33.8% 假接受等文献证据 vs 本文 92/92 零作弊。 推广场景：①RLHF 奖励模型可被策略攻击 → 换形式化约束验证器；②安全过滤器用对抗测试 → 换可达性证明；③数学解题评分用答案比对 → 换证明检查器；④合规检查从抽查 → 全量规则引擎；⑤类型检查本身就是此原则的最古老成功案例。
8.3 实现与证明（或验证）联合搜索
核心思想：当生成物带有验证义务时，把义务纳入搜索循环（改产物 ↔ 攻证明，用验证器反馈引导），而非先生成后验证的两段式。 论文证据：agent 依 Lean 报错交替修订 f′ 与 π；为可证性改实现（表示保控制流的 124.90× 案例）；失败证明不区分错重写与弱证明——分配精力本身是任务。 推广场景：①代码生成带编译器/类型错误反馈的迭代修复；②硬件设计生成与仿真波形联调；③SQL 生成与查询计划验证交替；④定理猜想生成与自动反例查找交替；⑤配置生成与策略引擎校验交替。
8.4 多样性候选的分歧即测试
核心思想：多个独立求解器在同一任务上的分歧点，是高价值测试用例的免费来源——分歧标记了至少一方出错的地方。 论文证据：三策略移植候选分歧点被测试设计 agent 转为语料；9 个单 agent 全零仓库被救回 61.1%–100%，净增 3,636 测试中 2,685 来自全零仓库。 推广场景：①LLM 多采样自一致性中不一致样本送人审；②多模型集成中分歧样本做主动学习；③编译器 fuzzing 用多编译器输出差找 bug；④多医生会诊分歧病例优先复查；⑤多传感器读数分歧触发校准。
8.5 证据冻结：任何修复都必须通过未见检验
核心思想：让修复者/生成者接触不到部分评估证据，使每次修改都在未见数据上被检验，杜绝自己判自己。 论文证据：修复 agent 在部分证据冻结下工作，每个修复须"修好失败且不破坏通过”；最终评估在无人见过的 ProgramBench 隐藏集上仅跑一次。 推广场景：①ML 的 train/dev/test 分离与留出集；②Kaggle 私有榜单；③红队测试的隐藏攻击集；④代码评审的双盲；⑤回归测试的冻结黄金集。
8.6 正确性二值、性能连续的任务设计：不饱和的靶场
核心思想：把任务的正确性做成机器检查的二值约束、把进步做成连续度量，任务不会因 agent 变强而饱和——每个已部署函数都是一个自带规范的免费训练实例。 论文证据：论文明确论述"正确性固定而加速是连续度量而非通过率，任务开放且不随 agent 改进而饱和"；vfast_p 曲线给出任意阈值下的分布。 推广场景：①代码修复以测试套件为约束、以延迟减少为奖励；②定理证明中"更强引理"的连续评分；③压缩算法以解码正确为约束、以压缩率为目标；④游戏 AI 以规则合法为约束、以胜率分差为目标；⑤能耗调度以可行性证明为约束、以能耗为目标。
8.7 双层度量：局部最优 ≠ 全局收益
核心思想：同时度量组件级与应用级效果，两者的差距（如 Amdahl 份额封顶）本身是重要的科学发现与后续方向。 论文证据：函数级 1.864× vs 应用级 1.120×；47/51 场景改进但 4 个无改进；目标选择被立为核心开放问题。 推广场景：①模型压缩在层基准 vs 端到端延迟的双层报告；②索引优化在查询基准 vs 整库 TPS；③缓存策略在命中率 vs 用户可感延迟；④编译优化在 microbench vs SPEC；⑤课程模块得分 vs 期末综合能力。
结语
AQUEDUCT 的贡献不止于一串加速数字，而在于它示范了一种新的分工：agent 负责 judgement（写程序、写证明、设计测试、修复缺陷），确定性系统负责 decision（选优、审计、计时）与 correctness（Lean 内核）。当等价证明把作弊面归零，agent 的激进优化才有安全落点——12.8 万倍的闭式替换与 124.90 倍的数组重写都建立在同一个信任链上。函数级与应用级增益之间的落差（1.86× vs 1.12×）则诚实地标注了下一个战场的位置：在仓库的千百个函数中，选对那几个值得证明的。对于关注 AI 辅助编程走向的读者，这篇论文与费马大定理的形式化共同指向一个趋势：机器检查的正确性正在从学术玩具变成智能体工作流的生产判据。