Research map / Large language models / Agents, code and math
miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Audits miniF2F's informal and formal statements, releases corrected miniF2F-v2 (simplified and competition variants), and measures an end-to-end autoformalizer-plus-prover pipeline showing much lower accuracy than reported SoTA.
Problem
miniF2F contains formal/informal mismatches, simplified goals, and unprovable statements, so reported autoformalization (~97%) and theorem proving accuracies overstate end-to-end formal reasoning on Olympiad-style problems.
Approach
Treat miniF2F as an Olympiad: the system must read the informal statement, formalize it, and prove it, with credit only if the proof matches the original problem. The authors manually correct over 300 Lean 4 statements, producing miniF2F-v2s (simplified, aligned to formal) and miniF2F-v2c (exact competition statements, including multiple choice and hidden answers).
Key results
- Human review shows Herald autoformalization at about 62-70% on miniF2F-v1 versus the 97% LLM-judged figure in the literature.
- The best end-to-end pipeline reaches about 36% effective accuracy on the original miniF2F under the Olympiad setting, versus 70% on miniF2F-v2 with corrected statements.
- Goedel-V2-7B reaches 82.0% on miniF2F-v1 test but 74.2% on v2s-test and 72.5% on v2c-test for whole-proof generation.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Replace miniF2F-v1 test with corrected miniF2F-v2s test | Goedel-V2 · miniF2F test | accuracy: 82.0% -> 74.2% | Hurt |
| Use competition-level miniF2F-v2c test instead of miniF2F-v1 test | Goedel-V2 · miniF2F test | accuracy: 82.0% -> 72.5% | Hurt |
| Replace miniF2F-v1 test with corrected miniF2F-v2s test | DeepSeek-Prover-V2-7B · miniF2F test | accuracy: 73.4% -> 68.1% | Hurt |
| Use competition-level miniF2F-v2c test instead of miniF2F-v1 test | DeepSeek-Prover-V2-7B · miniF2F test | accuracy: 73.4% -> 64.4% | Hurt |
| Replace miniF2F-v1 test with corrected miniF2F-v2s test | Kimina-Prover-Distill-7B · miniF2F test | accuracy: 65.2% -> 59.0% | Hurt |
| Use competition-level miniF2F-v2c test instead of miniF2F-v1 test | Kimina-Prover-Distill-7B · miniF2F test | accuracy: 65.2% -> 57.0% | Hurt |
| Use Olympiad-setting scoring rather than full-score scoring, which credits excessively simplified proofs | Kimina autoformalizer + theorem provers · miniF2F-v1 test | effective accuracy: 60.2 -> 35.2 | Hurt |
| Correct miniF2F statements and evaluate in the Olympiad setting | Kimina autoformalizer + DeepSeek-Prover-V2-7B · miniF2F test | effective accuracy: 40.2 -> 60.2 | Helped |
| Correct miniF2F statements and evaluate in the Olympiad setting | Herald translator + Goedel-V2-7B · miniF2F test | effective accuracy: 36.9 -> 50.0 | Helped |
| Use competition-level statements rather than simplified v2s statements | Kimina autoformalizer + DeepSeek-Prover-V2-7B · miniF2F test, Olympiad setting | effective accuracy: 60.2 -> 52.5 | Hurt |
| Replace LLM evaluator with human expert verification | Herald translator · miniF2F-v1 test @128 | autoformalization accuracy: 97.5% -> 62.7% | Hurt |
| Replace LLM evaluator with human expert verification | Kimina autoformalizer · miniF2F-v1 test @128 | autoformalization accuracy: 98.4% -> 90.6% | Hurt |
Surprising findings
- LLM-based equivalence judging produces many false positives; human-verified Herald accuracy is far below its LLM-judged 97%.
- Excessively simplified problems in miniF2F-v1 were proved much more often than their faithful counterparts in v2, indicating the original benchmark overstates prover ability.
Limitations
- Only the Lean language is covered, though miniF2F exists in other formal languages.
- Human evaluation was performed by Lean experts on the first compiled translation for @128 rather than all samples.
Experimental setup
Datasets: miniF2F
Benchmarks: miniF2F-v1 miniF2F-v2s miniF2F-v2c
Metrics: accuracy effective accuracy pass@32 pass@128
Baselines: Herald translator Kimina autoformalizer o4-mini DeepSeek-Prover-V1.5-RL Goedel-Prover-SFT Kimina-Prover-Distill-7B DeepSeek-Prover-V2-7B Goedel-Prover-V2-7B
Builds on: miniF2F Herald translator Kimina autoformalizer
Closest papers by meaning
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.88)
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems (NeurIPS 2024 · similarity 0.87)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.87)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.87)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.