AxDafny: Dafny中的智能验证代码生成
AxDafny: Agentic Verified Code Generation in Dafny
AI总结：
提出AxDafny框架，通过验证器引导的修复迭代生成Dafny代码和证明，在LCB-Pro-Dafny和DafnyBench上显著提升验证成功率。
摘要：
我们研究Dafny中的智能代码生成，其中模型必须生成可执行代码和用于验证的证明工件。我们提出了AxDafny，一个验证器引导的修复框架，迭代生成实现、不变量、断言和终止参数。我们还引入了LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny)，一个包含250道竞赛风格编程问题的基准测试，这些问题被翻译成Dafny并带有形式化规范和基于验证器的评估工具。在LCB-Pro-Dafny上，AxDafny相比基线GPT-5.5显著提高了验证成功率。在DafnyBench上，AxDafny达到了92.7%的验证成功率，比之前最强的证明提示基线高出6.5个百分点。最后，我们表明验证成功率和运行时测试性能衡量了生成代码的不同方面。
英文摘要：
We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification. We present AxDafny, a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments. We also introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness. On LCB-Pro-Dafny, AxDafny substantially improves verification success over baseline GPT-5.5 performance. On DafnyBench, AxDafny achieves 92.7\% verification success, outperforming the strongest previously reported proof-hint baseline by 6.5 percentage points. Lastly, we show that verification success and runtime test performance measure different aspects of generated code.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
