现实世界软件的智能体式经验证优化

arXiv:2610.30188v1 公告类型：交叉发布 摘要：程序优化旨在提升性能，同时保持行为不变。编程智能体已经能够通过改变算法、数据结构和执行策略来加快程序运行。然而，现有的等价性检查大多依赖测试，而已有研究表明，智能体会利用测试的漏洞，在未保持预期行为的情况下通过测试。我们提出智能体式经验证优化：智能体生成运行更快的实现，同时提供经机器核验的证明，证明该实现与现有实现等价。由于现有实现充当了规约，这项任务避开了经验证代码生成中的规约编写瓶颈，而定理证明领域的最新进展也使这些证明变得可行。我们在 Lean 4 中从函数和代码仓库两个层面形式化定义了这项任务；在 Lean 4 中，程序既可以执行，也可以进行推理。由于很少有现实世界应用使用 Lean 编写，我们开发了 Aqueduct，这是一个智能体式框架，可将 C、C++、Go 和 Rust 程序迁移为原生 Lean 程序，并通过与原始程序进行差分测试来验证每个移植版本。在 Verina 的 189 个参考实现中，智能体为其中 156 个生成了速度更快且经过证明的改写版本，其中包括将指数级递归替换为动态规划等算法改动。在 17 个迁移后的应用中，智能体生成的 92 个经过证明的改写版本加速了 51 个应用场景中的 47 个。这些应用级收益小于函数级收益，因此，选择哪些函数进行优化成为一个重要问题。由此可见，当前的智能体已经能够对独立函数以及从真实程序迁移而来的应用执行经验证优化。我们讨论了尚存的挑战，以及在生产环境中实现经验证优化所需的步骤。