Reproduce “DafnyPro: LLM-Assisted Automated Verification for Dafny Programs” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche
DafnyPro is an inference-time framework designed to enhance Large Language Model (LLM) generation of verification annotations for Dafny programs. It integrates a diff-checker to prevent base code modifications, an invariant pruner to optimize annotation sets, and a hint-augmentation system to incorporate domain knowledge, yielding verification rate improvements of 14-16 percentage points on several benchmarks for Claude models and enabling smaller fine-tuned LLMs to achieve up to 69.5% verified programs on DafnyBench.
Key insights
- Rigorous verification of base code integrity (via a diff-checker) is essential to prevent LLMs from 'reward hacking' and to ensure the soundness of generated annotations.
- Optimizing LLM-generated annotations by pruning non-inductive clauses significantly improves the efficiency and success rate of the formal verification process.
- Incorporating domain-specific, problem-independent proof strategies as explicit hints can substantially improve the ability of LLMs to guide verifiers in completing proofs.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.