Berkeley RDI 与 AWS 发布 Aqueduct：用 Lean 等价证明验证智能体软件优化

UC Berkeley 与 AWS 团队提出 Aqueduct 框架，让编程智能体加速已有函数并在 Lean 4 中证明新实现 f′ 与原函数 f 在所有输入上等价，无需人工写规格。