智能体为真实软件生成经Lean证明的等价加速重写

事件综述根据 1 篇报道整理，11月11日更新

UC Berkeley 与 AWS 的研究者提出 Aqueduct 框架：让编码智能体加速现有函数，并在 Lean 4 证明助手中证明加速版本 f′ 与原函数 f 对所有输入返回相同结果，以现有代码本身作为规格。 在 17 个 C、C++、Go 和 Rust 应用上，Aqueduct 将其迁移到 Lean，92 个经证明的重写使 51 个应用场景中的 47 个变快；在 Verina 基准的 189 个小程序中，智能体为 156 个生成了经证明的加速。研究团队指出，应用层面整体加速仅 1.12×，因为函数加速只按该函数耗时占比计入，选择优化哪些函数因此是重要问题。 上述结果来自团队自述的论文与项目网站，尚未见独立复现。

综述由模型根据报道生成，细节以各篇原文为准。