AxDafny：Dafny 中的代理式验证代码生成

本文研究了 Dafny 语言中的代理式代码生成，要求模型同时生成可执行代码及验证所需的证明工件。我们提出了 AxDafny，这是一个验证器引导的修复框架，能迭代生成实现、不变量、断言及终止性论证。此外，引入了 LiveCodeBench-Pro-Dafny 基准，包含 250 个翻译为 Dafny 的竞赛级编程问题及其形式化规范。实验表明，AxDafny 在验证成功率上显著优于基线模型，并在 DafnyBench 上达到 92.7% 的成功率。