让AI生成代码的同时自动生成可验证的证明，提升程序可靠性。
AxDafny: Agentic Verified Code Generation in Dafny
- 用验证器引导迭代修复，自动补全代码与证明
- 在250个题目上验证成功率超基线6.5个百分点
- 适合需要高可靠代码的系统开发与安全领域
我们研究了在Dafny中进行智能体式代码生成，要求模型同时生成可执行代码和可验证的证明。提出AxDafny框架，通过验证器引导，迭代生成实现、不变量、断言和终止性论证。引入LiveCodeBench-Pro-Dafny（LCB-Pro-Dafny）基准，包含250个竞赛风格编程题，已转化为带形式化规范的Dafny代码，并配备基于验证器的评估工具。在LCB-Pro-Dafny上，AxDafny显著优于基线GPT-5的验证成功率。在DafnyBench上，验证成功率达到92.7%，比此前最强的证明提示基线高出6.5个百分点。最后，我们发现验证成功率与运行时测试表现衡量的是代码的不同方面。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。