miniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

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 GitHub.

Large language models can often produce convincing mathematical reasoning, but it is difficult to know when their answers are actually correct. Formal verification offers a way to check reasoning mechanically: a proof is accepted only if a verifier can confirm that every step is valid. This paper introduces miniF2F-Dafny, a new version of a widely used mathematical reasoning benchmark translated into Dafny, a verification language commonly used for checking software correctness. Unlike many proof assistants, Dafny can automatically handle many routine reasoning steps using built-in solver technology. This lets us study a different style of AI-assisted theorem proving, where the AI provides high-level proof guidance and the verifier fills in many low-level details. We find that Dafny can solve around 40% of the benchmark without any proof hints at all, and that modern language models can improve performance further by supplying useful proof guidance. The results suggest that software verification tools may provide a complementary path for building AI systems that can produce checkable mathematical reasoning.