10:35官方账号arXiv cs.AI@Benjamin Breen, Austin Letson, Borja Requena Pozo, Leopoldo SarraAxDafny 是一种基于验证器引导的修复框架,可迭代生成实现、不变式、断言和终止参数。研究者引入了 LCB-Pro-Dafny 基准,包含 250 道竞赛编程题,配有形式化规范和验证评估。在 LCB-Pro-Dafny 上,AxDafny 相比 GPT-5.5 基线显著提升验证成功率。在 DafnyBench 上,AxDafny 达到 92.7% 验证成功率,比此前最强的证明提示基线高出 6.5 个百分点。实验还表明,验证成功与运行时测试表现衡量了代码生成的不同方面。论文AxDafnyDafnyLCB-Pro-Dafny推荐理由:想搞形式化验证代码生成?这篇论文的 AxDafny 用验证器做迭代修复,把 Dafny 编程题的验证成功拉到 92.7%,比之前的最好方法还高 6.5 个百分点。原文稍后读已读值得跟进有用关注 AxDafny