论文智能体 · Skill · MCP程序优化形式验证Lean 4coding agent

Agentic Verified Optimization of Real-World Software

AI 解读已生成 · AI 生成，数字以原文为准

AI 全文总结值得深入基于论文全文 5.6 万字 · 完整阅读

智能体在 Lean 4 为 156/189 函数产出带等价证明的更快重写，应用级仅 1.120×

智能体验证优化要求智能体生成更快实现 $f^{'}$ 并给出 Lean 4 内核检查的等价证明 $π : f = f^{'}$ ，以现有实现为规范，规避验证代码生成的规格书写瓶颈。由于真实软件极少用 Lean，作者构建 Aqueduct 将 C、C++、Go、Rust 程序迁移为原生 Lean，并以差分测试、覆盖率引导模糊和突变分析验证端口。在 Verina 的 189 个参考实现上，智能体为 156 个生成更快且经验证的重写，函数级几何平均 1.851×；迁移应用中的 92 个重写全部在函数级更快，应用级几何平均仅 1.120×，收益明显低于函数级，说明目标选择成为关键。重写包括把指数递归改为动态规划、复用 Mathlib 的 Nat.sqrt、用哈希集去重、数组替换列表及提前返回。局限是 Lean 不定义 IO 等不透明效果，须先建模才能扩展到生产 I/O 路径。

1156/189 Verina 函数获得 Lean 等价证明加速（82.5%）
2Aqueduct 迁移恢复 87.68%，超单智能体 19.50 个百分点
3应用级仅 1.120×，47/51 场景；函数级 1.864×

为什么重要　代码优化不再只跑测试：Lean 等价证明可防奖励黑客；Aqueduct 迁移链路给多语言工程落地一个可复现基线适合　研究 LLM 代码优化、定理证明、程序语言工程或需要形式化保证的工程师

来源: arxiv.org
发布: 2026/10/23

中文（AI 翻译）

程序优化旨在在保持行为的同时提升性能。编码智能体已经可以通过更改算法、数据结构和执行策略使程序更快。然而，现有的等价性检查大多依赖测试，而智能体已被证明会利用这些测试，在不保持预期行为的情况下通过测试。我们提出 agentic verified optimization，其中智能体生成一个更快的实现，并附有与现有实现等价的机器可检查证明。由于现有实现充当规范，该任务避免了验证代码生成中的规范编写瓶颈，并且定理证明的最新进展使这些证明变得可实现。

我们在 Lean 4 中在函数级和仓库级制定该任务，在 Lean 4 中程序既可以执行也可以进行推理。由于很少现实应用是用 Lean 写的，我们开发了 Aqueduct，一个智能体框架，将 C、C++、Go 和 Rust 程序迁移到原生 Lean，并通过与其原始程序进行差分测试来验证每个移植。在 Verina 的 189 个参考实现中，智能体为 156 个生成了更快的已证明重写，包括算法更改，例如用动态规划替代指数递归。

在 17 个迁移应用上，其 92 个已证明重写加速了 51 个应用场景中的 47 个。这些应用级收益小于函数级收益，使得选择要优化的函数成为一个重要问题。当前的智能体已经可以在独立函数和从真实程序迁移的应用上执行验证式优化。我们讨论了剩余挑战以及在生产中实现验证式优化的步骤。

原文

Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution strategies.

However, existing equivalence checks mostly rely on tests, which agents have been shown to exploit, passing the tests without preserving the intended behavior.

We propose agentic verified optimization, in which an agent produces a faster implementation together with a machine-checked proof of equivalence to the existing one.

Because the existing implementation serves as the specification, the task avoids the specification-writing bottleneck of verified code generation, and recent advances in theorem proving make the proofs attainable.

We formulate the task at the function and repository levels in Lean 4, where programs can be both executed and reasoned about.

Few real-world applications are written in Lean, so we develop Aqueduct, an agentic framework that migrates C, C++, Go, and Rust programs into native Lean, validates each port by differential testing against its original.

On the 189 reference implementations in Verina, agents produce faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming.

On 17 migrated applications, their 92 proved rewrites speed up 47 of 51 application scenarios.

These application-level gains are smaller than the function-level ones, making the choice of functions to optimize an important problem.

Current agents can thus already carry out verified optimization on both standalone functions and applications migrated from real programs.

We discuss the remaining challenges and the steps toward verified optimization in production.

Basic
1.959
Advanced
1.716
All
1.851

注释 · 中位 1.117×；71 个超 1.25×，38 个超 2×出自表 1 图 4

16,345/18,642

通过

12,709/18,642

基线通过

87.68%

恢复率

68.17%

基线恢复率

注释 · 40 个仓库，原版通过 18,642 个测试出自 §5.2

目标语言: Lean 4
源语言: C/C++/Go/Rust
优化模型: Codex GPT-5.6 Sol xhigh
运行时: Lean 4.18.0
硬件: AMD EPYC 9654

深度总结

1 / 7

92/92

函数级与应用级增益对比· 表格

92/92 个重写全快于迁移参考，应用级仅 1.120×

对比	F 更快	F 几何均值	A 更快	A 几何均值
优化 Lean vs 迁移 Lean	92/92	1.864×	47/51	1.120×
优化 Lean vs 原版	15/92	0.235×	3/51	0.148×
迁移 Lean vs 原版	12/92	0.126×	3/51	0.132×

注释 · 函数级中位数 1.402×，应用级中位数 1.077×，最大单点 18.53×出自表 2

智能体在 Lean 4 为 156/189 函数产出带等价证明的更快重写，应用级仅 1.120×

智能体验证优化要求智能体生成更快实现

f^{'}

并给出 Lean 4 内核检查的等价证明

π : f = f^{'}

，以现有实现为规范，规避验证代码生成的规格书写瓶颈。由于真实软件极少用 Lean，作者构建 Aqueduct 将 C、C++、Go、Rust 程序迁移为原生 Lean，并以差分测试、覆盖率引导模糊和突变分析验证端口。在 Verina 的 189 个参考实现上，智能体为 156 个生成更快且经验证的重写，函数级几何平均 1.851×；迁移应用中的 92 个重写全部在函数级更快，应用级几何平均仅 1.120×，收益明显低于函数级，说明目标选择成为关键。重写包括把指数递归改为动态规划、复用 Mathlib 的 Nat.sqrt、用哈希集去重、数组替换列表及提前返回。局限是 Lean 不定义 IO 等不透明效果，须先建模才能扩展到生产 I/O 路径。

1156/189 Verina 函数获得 Lean 等价证明加速（82.5%）

2Aqueduct 迁移恢复 87.68%，超单智能体 19.50 个百分点

3应用级仅 1.120×，47/51 场景；函数级 1.864×

来源

arxiv.org

发布

2026/10/23