The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use of Large Language Models (LLMs) to automatically infer missing helper assertions in Dafny programs, with a primary focus on cases involving multiple missing assertions. To support this study, we extend the DafnyBench benchmark with curated datasets where one, two, or all assertions are removed, and we introduce a taxonomy of assertion types to analyze inference difficulty. Our approach refines fault localization through a hybrid method that combines LLM predictions with error-message heuristics. We implement this approach in a new tool called DAISY (Dafny Assertion Inference SYstem). While our focus is on multiple missing assertions, we also evaluate DAISY on single-assertion cases. DAISY verifies 63.4% of programs with one missing assertion and 31.7% with multiple missing assertions. Notably, many programs can be verified with fewer assertions than originally present, highlighting that proofs often admit multiple valid repair strategies and that recovering every original assertion is unnecessary. These results demonstrate that automated assertion inference can substantially reduce proof engineering effort and represent a step toward more scalable and accessible formal verification.

翻译：Dafny验证器虽能提供强大的正确性保证，但通常需要大量手动编写的辅助断言，这构成了其应用的重要障碍。本研究探索利用大型语言模型（LLMs）自动推断Dafny程序中缺失的辅助断言，重点关注涉及多个断言缺失的情况。为支持此项研究，我们扩展了DafnyBench基准测试集，构建了精心设计的数据集，其中分别移除一个、两个或全部断言，并引入断言类型分类法以分析推断难度。我们的方法通过结合LLM预测与错误消息启发式规则的混合策略，改进了故障定位机制。我们将该方法实现在名为DAISY（Dafny断言推断系统）的新工具中。在聚焦多断言缺失场景的同时，我们也评估了DAISY在单断言缺失案例上的表现。DAISY在单断言缺失程序中实现了63.4%的验证成功率，在多断言缺失程序中达到31.7%。值得注意的是，许多程序可以通过比原始版本更少的断言完成验证，这表明证明过程通常允许多种有效的修复策略，且无需完全恢复所有原始断言。这些结果证明，自动化断言推断能显著降低证明工程的工作量，是朝着更具可扩展性和易用性的形式化验证迈出的重要一步。