AWS 与 UC Berkeley 让 Agent 用 Lean 证明代码优化等价，平均提速 1.85 倍

UC Berkeley 与 AWS 提出 Agentic Verified Optimization，让 Agent 通过 Lean 证明优化后代码与原函数等价；在 Verina 的 189 个参考实现中，156 个获得更快的已证明改写，几何平均提速 1.85×。