AWS 与伯克利让 Agent 用 Lean 证明代码优化等价，平均提速 1.85 倍
xiuyu_l · x · 2026-10-24
UC Berkeley 与 AWS 提出 Agentic Verified Optimization：Agent 接收现有函数 f，返回更快的实现 f′，并附上 Lean 证明 f′ 与 f 在所有输入上等价。现有代码即规格说明，无需另写形式化规格；提速必须带证明才计数，天然抗 reward hacking，且加速比是连续指标不会饱和。
- 在 Verina 的 189 个参考实现上，Agent 对 156 个给出了更快的已证明改写，几何平均提速 1.85×
- 团队还做了 Aqueduct，把 C/C++/Go/Rust 程序迁入原生 Lean：17 个迁移应用中，92 个已证明改写加速了 51 个应用场景中的 47 个，15 个优化后函数比原原生程序对应操作还快
- 关键发现：应用级收益（1.12×）远小于函数级（1.86×），如何挑选值得优化的函数成为重要问题
「编程与Agent」频道最新
- 1979 论文断言形式验证难成气候，2026 预言它将像 fuzzing 一样普及 — danbri · 2026-10-24
- Scale AI 团队打造航空高保真模拟环境，测试AI智能体应对风暴 — menhguin · 2026-10-24
- 双 iPhone 并排跑 agent：分析师称手机已能替代电脑管任务 — BenBajarin · 2026-10-24
- HumanLayer 宣布开源:主张「软件工厂」必须开放可组合 — teropa · 2026-10-24
- macOS 27 终端内置免费本地 LLM:fm 命令一行上手,完全离线免 API Key — dr_cintas · 2026-10-24
- Bug Hunt Bench 实测：Kimi K3.1 Pro 在 Claude Code 里跑分，成本差 2.9 倍 — PawelHuryn · 2026-10-24