核心问题：等价证明覆盖所有合法输入，为什么“优化后更快”仍然只是有条件的结论？
论文卡片
- 原题： Agentic Verified Optimization of Real-World Software
- 作者： Zhe Ye、Udaya Ghai、Zhizhen Qin、Dawn Song、Soonho Kong。
- 日期与版本： 2026-10-20 提交，arXiv v1；主分类 cs.SE，方法与实证研究预印本。
- 定位： Agent 程序优化、Lean 等价证明与性能评测。
- 入口： arXiv · 一手全文（v1） · PDF · alphaXiv
简短导读：同一次优化，两种保证
作者让既有程序充当规格：Agent 提出替代实现，并提交 Lean 内核可检查的等价证明。这样，优化可以改变算法和数据表示，却不能仅靠迎合测试来改变输出。搜索也因此同时包含两种困难：找到更快的实现，以及找到能证明它等价的论证。
这套方法有意把两件事分开。正确性由等价定理约束，性能由固定工作负载上的计时判断。 前者不能自动推出后者。即使一个改写对所有合法输入都返回相同结果，它也可能只在某些输入分布上更快。
附录 D 的一个例子很直观：为零指数增加提前返回分支，不改变任何输入的结果；但这个快路径能贡献多少加速，取决于测量中零指数出现的情况。证明保障分支不会算错，并不决定分支会被使用多少次。
证据与限制
§5 使用 Codex / GPT-5.6 Sol（xhigh）。评测工作负载对优化 Agent 隐藏，计时采用九组成对试验、交替运行顺序并取中位数。这支持对未见计时输入的改善，但不等于覆盖所有输入分布与硬件环境。
| 比较范围 | 基线与结果 | 如何理解 |
|---|---|---|
| 189 个 Verina 函数 | 156 个找到更快且获证的实现；几何平均加速 1.851×，中位数 1.117× | 汇总包含全部目标，每个目标选获证候选与原实现中的最快者；54 个初次未改善的目标获得一次重试 |
| 17 个迁移应用、51 个场景 | 优化后 Lean 相对迁移版 Lean：47/51 更快，几何平均 1.120× | 应用收益小于 92 个已接受函数改写的 1.864×；局部加速不必然成为同幅度的整体加速 |
| 同一批 51 个场景 | 优化后 Lean 相对原 C/C++/Go/Rust 程序：3/51 更快，几何平均比值 0.148× | “比迁移版更快”不能写成“普遍胜过原生程序”；比值为基线耗时除以被测耗时，低于 1 表示更慢 |
还有一条必须分清的链路。Aqueduct 把原程序迁到 Lean，这一步依靠差分测试等证据；形式化证明覆盖的是 Lean 参考实现到 Lean 优化实现，不是整个跨语言迁移过程。 证明仍信任编译器和运行时保持 Lean 语义；不透明 I/O 等行为也不在此次直接等价优化的范围内。
论文证明了这类优化可以被 Agent 找到，没有通过同预算的“有证明要求／无证明要求”对照，确定证明要求对搜索效率的净影响。作者在 §6 把这种比较，以及带成本模型的性能证明，列为后续研究。以上数字为论文报告，未独立复现。
重点阅读章节
- §3.1、§3.3： 对照等价义务、工作负载和加速指标的定义。
- §5.1–5.2、表 1–2： 留意原实现回退、重试和三种程序版本之间的基线关系。
- §6 的性能证明讨论、附录 A 与 D.3： 区分当前保证、信任前提和仍未实现的扩展。
思想启发：证明没有消灭评测
以下是导读者的延伸理解。
“经过验证的优化”容易被读成一个没有条件的结论，实际却包含两种不同范围的主张：行为等价是逻辑命题，运行更快是特定测量条件下的经验命题。证明使行为保持更可靠，也让性能比较中的剩余问题更清楚：快在哪里、相对谁、对哪些负载成立。
即便将来加入复杂度证明，也仍需要说明成本模型。减少抽象操作次数与减少真实机器时间之间，还有常数、内存访问和运行时开销。逻辑证据与实验证据可以互相约束，但不能互相代替。
三个开放性思考问题
1. 所有输入都保持正确、但只让常见输入更快的改写，应该算怎样的优化成功？
参考思路
平均耗时、尾部延迟和最坏情况可能指向不同判断。等价证明排除了输出变化，却不排除性能在输入之间重新分配。若“常见”的分布发生变化，成功结论也可能改变；这不否定证明，而是说明优化目标还需要独立定义。
2. 为每个目标保留原实现作为回退，会让汇总加速比遗漏哪些失败？
参考思路
回退合理地描述了最终能保留的最佳程序，却会把无改善、证明未完成和候选变慢都压到同一个性能下界。成功比例提供补充信息，但搜索时间、重试成本与证明难度仍不在加速比中。最终产物的质量与找到它的效率，是相关而不同的对象。
3. 如果容易证明的改写并非最有性能潜力的改写，证明要求是在帮助搜索，还是限制搜索？
参考思路
它可能排除错误候选、鼓励重用可靠算法，也可能使 Agent 提前放弃难以建立不变量的变换。两种作用可以同时存在。论文给出了可行性证据，但尚不能区分收益来自搜索引导、现成证明知识，还是更大的尝试成本；作者提出的同预算对照正对应这一未决矛盾。