MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
summary
miniF2F gets fully translated into Dafny and a compact library of ~100 axiomatized lemmas, then run through Dafny’s SMT automation and 14 off‑the‑shelf LLMs. Dafny verifies 99/244 (40.6%) test and 109/244 (44.7%) validation problems with empty proofs; LLMs provide iterative hints and the best model reaches 55.7% pass@4 while many sit near 50%. Results show SMT handles low‑level steps reliably but LLMs only partially close the remaining gap.
AI-written summary · about
chapters (9)
- 0:00MiniF2F-Dafny project
- 1:27MiniF2F benchmark
- 4:44Translating MiniF2F to Dafny
- 8:14Formalizing MiniF2F in Dafny
- 9:41Dafny’s SMT automation success
- 11:05LLM-guided proof synthesis
- 14:22Limitations of LLM proofs
- 16:08Dafny versus other provers
- 16:49Proof formats questions
related talks
17mNeuro-Symbolic Proof Generation for Scaling Systems Software Verification
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
27mExploring the Mechanisms of LLM Reasoning Capabilities
22mTowards Automated Verification of LLM-Synthesized C Programs
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
19mLLMs reasoning and agentic capabilities over time