智能体验证式优化：为真实软件生成带机器证明的等价重写

论文提出“智能体验证式优化”，让智能体在给出更快实现的同时，产出与原实现机器可验证的等价性证明，以避免现有基于测试的等价检查被智能体钻空子。作者在 Lean 4 中把任务定义在函数和仓库两个层级，并开发 Aqueduct 框架，将 C、C++、Go、Rust 程序迁移为原生 Lean，再用差分测试校验每次移植。