智能体实现可验证的程序优化

智能体可在 Lean 4 中为真实程序生成带等价性证明的加速重写。

资讯摘要

论文提出“智能体可验证优化”：让编码智能体在给出更快实现的同时，产出机器可检验的等价性证明，并以原实现作为规范，从而绕开验证式代码生成的规范编写瓶颈。作者在 Lean 4 中定义函数级与仓库级任务，并开发 Aqueduct 框架，将 C、C++、Go、Rust 程序迁移为原生 Lean 并用差分测试校验。在 Verina 的 189 个参考实现中，智能体为 156 个给出更快的已证明重写。

要点速读

1. 论文提出智能体可验证优化：智能体同时输出更快的实现与机器可检验的等价性证明，原实现即作为规范。
2. 作者开发 Aqueduct 框架，将 C、C++、Go、Rust 程序迁移为原生 Lean，并用差分测试对照原程序校验。
3. 在 Verina 的 189 个参考实现上，智能体为 156 个产出更快的已证明重写，包括用动态规划替换指数递归等算法改动；在 17 个迁移应用上，92 个已证明重写使 51 个应用场景中的 47 个加速。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/24 08:00:37（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。