MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Sean B. Holden
cs.LG
Dec 11, 2025 · v3
TL;DR
Translates the Lean miniF2F benchmark into Dafny. As a baseline comparison, it runs Lean 4's grind tactic on the Lean miniF2F test problems.
Abstract
LLMs excel at reasoning, but validating their steps remains challenging. Formal verification offers a solution through mechanically checkable proofs. Interactive theorem provers (ITPs) dominate mathematical reasoning but require detailed low-level proof steps, while auto-active verifiers offer automation but focus on software verification. Recent work has begun bridging this divide by evaluating LLMs for software verification in ITPs, but the complementary direction, LLMs for mathematical theorem proving in auto-active verifiers, remains unexplored. We present MINIF2F-DAFNY, the first translation of the widely-used mathematical benchmark miniF2F to an auto-active verifier: Dafny. We find that Dafny's automation alone solves 39-44% of problems with empty proofs, whereas many require substantial proof guidance in ITPs. We evaluate 8 off-the-shelf LLMs on proof generation, with the best model (Claude Opus 4.6) achieving 62.7% cumulative pass@4 on the full test set, improving over the 38.9% empty-proof baseline by 23.8 percentage points. These results show that auto-active verification offers a complementary empirical setting for AI-assisted mathematical reasoning, where LLMs provide high-level guidance while SMT automation handles low-level details. Our benchmark and evaluation infrastructure are publicly available on
https://github.com/dafny-lang/miniF2F.
Problem
LLM-based formal mathematical theorem proving has been studied almost entirely in interactive theorem provers such as Lean. Auto-active verifiers, which rely on SMT automation, had not been evaluated on pure mathematics.
Approach
The authors translate the 488 miniF2F problems (244 test, 244 validation) from Lean into Dafny lemmas with empty proof bodies. Supporting definitions and a library of 174 lemmas are axiomatized for the translation. They measure how much Dafny/Z3 solves with empty proofs, compare this against Lean 4's grind tactic on the Lean versions, and evaluate 8 off-the-shelf LLMs at generating proof hints.
Results
With empty proofs, Dafny verifies 38.9% of test problems, while Lean grind solves 32.4%; the two overlap but each solves problems the other misses. The best LLM, Claude Opus 4.6, reaches 62.7% cumulative pass@4 on the test set.
| Model | Pass@1 | Pass@4 |
|---|
| Claude Opus 4.6 | 58.2 | 62.7 |
| Claude Sonnet 4.5 | 52.5 | 55.7 |
| Qwen 3 Coder 480B | 45.5 | 48.8 |
| Dafny Verifier (empty proof) | 38.9 | 38.9 |
| Lean grind | 32.4 | 32.4 |
miniF2F-Dafny test set results (%)
