编码智能体可以把程序改快，但怎么确认改完之后对所有输入都返回同样的结果？Berkeley RDI 与 AWS 的研究者（Zhe Ye、Udaya Ghai、Zhizhen Qin、Dawn Song、Soonho Kong）在 2026 年 11 月发布的工作 Aqueduct 给出的答案是：让智能体在 Lean 4 里顺带证明这一点。论文为 arXiv:2610.30188。
他们的做法绕开了一个长期瓶颈——写规格。形式化验证通常需要先用形式语言写出「程序应该做什么」，而规格本身很难写对；Aqueduct 直接拿现有实现当规格，把待证命题固定为 f = f′：原函数 f 与改写后的 f′ 在所有输入上相等。智能体的任务据此变成「改写并证明」，而不是「猜一个规格再证明」。
为什么测试不够
文章先解释了动机。以测试作为正确性检查，只能证明程序错了，不能证明它对；当测试同时决定智能体的奖励时，它可以通过测试却没有保持行为。文中引用了两个例子：一份报告里看似 6 倍的加速，来自「重新生成测试值而不是存储它们」；另一次审计发现，某个优化框架接受的 GPU kernel 里有 39.5% 存在正确性失败。
等价性证明覆盖每一个输入。已有的验证编译器与超优化器也提供这种保证，但它们只能使用预先证明正确的变换、或只作用于很短的指令序列，因此只能发现这些变换能表达的东西。智能体不受固定变换集合的限制，可以提出新算法与新的数据表示；有了证明作为检查，改动的自由度与正确性要求就可以同时保留。
现成代码就是规格
验证能力近年提升很快，用强化学习训练的证明器已能达到奥赛水平，但「把意图翻译成正确的形式化陈述」仍是瓶颈。程序规格难写，即便是精心整理的规格也有错误——Vero 的审计就发现了这一点。
Aqueduct 省掉了这一步：命题 f = f′ 在智能体开始工作之前就已固定，原实现就是规格。
任务在 Lean 4 中表述。Lean 4 既是证明助手也是通用编程语言，同一份定义可以编译执行，也可以出现在证明里。智能体根据 Lean 的报错与证明目标反复修订 f′ 和证明，最终由 Lean 内核针对未改动的 f 检查证明。加速只有在等价证明成立时才算数，弱测试、或漏掉部分预期行为的书面规格，都无法被利用。作者认为这让任务对奖励作弊有抵抗力；又因为正确性固定、加速比是连续指标而非通过率，任务不会随着智能体变强而饱和，而且代码库里的每个函数都是一个规格现成的新实例。
Verina：156/189，几何平均 1.85×
在 Verina 基准的 189 个小程序上，智能体为其中 156 个产出了更快的、带证明的改写，几何平均加速 1.85 倍。最长递增子序列是个典型例子：原实现枚举 2ⁿ 条分支，智能体换成动态规划、证明两者相等，函数快了 4,468 倍。最大的加速达到 128,292 倍，做法是把迭代求和换成闭式多项式。
Aqueduct：把 C、C++、Go、Rust 迁进 Lean
Lean 是通用语言，但真实世界的应用很少用 Lean 写，而仓库级优化需要带调用方与负载的真实程序。Aqueduct 因此先把 C、C++、Go、Rust 程序迁移成原生 Lean，再用差分测试对照原程序检查每个移植版本。
在 ProgramBench 的 40 个仓库上，Aqueduct 的移植版本通过了原程序也能通过的隐藏测试中的 87.7%，而单个迁移智能体的这一数字是 68.2%。移植对象包括 Ninja 构建系统、pigz 压缩器、Doxygen 文档生成器，以及约 25.3 万行源码的 7zip。
流程分四步：三种策略（广度优先、夹具优先、账本引导）分别产出候选移植，目的让它们的错误各不相同；测试设计智能体以原程序为预言机构建共享测试集，做差分、覆盖率、模糊与变异测试；控制器按测试一致度选出最佳候选并修复失败项，只有在不破坏任何已通过测试时才保留修复；最后审计移植是否调用原程序、是否硬编码答案，然后在隐藏测试上评估一次。
需要区分的是：移植本身靠差分测试把关，证明覆盖的是被改写的函数，两者不是同一件事。
函数快了，应用只快 1.12 倍
在 17 个已迁移应用上，由智能体自己挑选要改写的函数。92 个带证明的改写在其微基准上全部更快，几何平均 1.86 倍；合起来让 51 个应用场景中的 47 个变快。但应用层面的收益只有 1.12 倍。
原因很直接：一个函数的加速只对它占用的那部分运行时间有效，所以「挑哪些函数来优化」本身是个重要问题。作者也给出一个积极信号：在这 92 个函数里，有 15 个优化后的 Lean 代码已经比原程序里对应的原生操作更快。
下一步
作者指出，义务 f = f′ 不依赖于 f′ 写在什么层次上：改写可以直接针对显式内存布局或向量指令，只要证明编译后的代码实现了 f。把文件与网络 I/O 建模成原语接口，也能把应用中的 I/O 路径纳入范围。
核心总结
- Aqueduct 把优化任务定义为「改写函数并在 Lean 4 中证明与原函数等价」，用现有实现充当规格，避开形式化规格难写、易出错的瓶颈
- Verina 189 个小程序中 156 个拿到带证明的加速，几何平均 1.85 倍，最长递增子序列一项快 4,468 倍
- 迁移框架把 C、C++、Go、Rust 程序转成原生 Lean，40 个 ProgramBench 仓库上移植通过 87.7% 的隐藏测试，单智能体基线为 68.2%
- 17 个应用中 92 个改写全部变快（微基准几何平均 1.86 倍），但应用级只有 1.12 倍，说明选择优化目标与改得快同样重要
- 值得注意的边界：移植靠差分测试而非证明；应用级收益受函数占用时间限制；Verina 以小型程序为主
原文：Agentic Verified Optimization of Real-World Software（Berkeley RDI，2026 年 11 月）｜论文：arXiv:2610.30188
