Reproduce “dafny-annotator: AI-Assisted Verification of 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
Gabriel Poesia, Chloe Loughridge, Nada Amin
The authors present an LLM tool that suggests annotations for Dafny programs, which checks candidate placements. They create synthetic examples by editing programs and removing annotations. On 83 held-out programs needing annotations, LLaMA 3.1 8B reached 50.6% success with DafnyBench and DafnySynth, versus 15.7% for the base model and DafnyBench alone; this excludes other held-out programs and specification writing.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.