miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

• URL: http://arxiv.org/abs/2511.03108v1
• Date: Wed, 05 Nov 2025 01:27:49 GMT
• Title: miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
• Abstract summary: We analyze the formal and informal statements in the miniF2F benchmark from the perspective of an AI system tasked to participate in a math Olympiad consisting of the problems in miniF2F.<n>Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature.<n>We present the miniF2F-v2 with fully verified formal and informal statements and proofs.
• Score: 16.8655558789989
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad consisting of the problems in miniF2F. In such setting, the model has to read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds to the original informal statement presented to the model. Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the miniF2F-v2 with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on miniF2F-v2 leads to the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that a higher quality benchmark can help the community better evaluate progress in the field of formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at https://github.com/roozbeh-yz/miniF2F_v2.

Related papers

• NovGauge: A Fine-Grained Benchmark for Diagnosing LLMs' Capability in Paper Novelty Assessment [54.4265627247104]
  Large language models (LLMs) are increasingly used in peer review at major AI conferences.<n>Existing benchmarks assess novelty as a single holistic score.<n>We present NovGauge, a human-anchored benchmark for fine-grained novelty assessment diagnosis.
  arXiv  Detail & Related papers  (2026-09-10T08:34:56Z)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieve is a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs.<n>It decomposes proof steps into local reasoning units, extracts typed proof obligations, and verifies them.<n>On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43% exact first-error accuracy.
  arXiv  Detail & Related papers  (2026-08-26T18:43:30Z)
• Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
  We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones.<n>We build a benchmark with both perturbations on miniF2F and MATH-500.<n>We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations.
  arXiv  Detail & Related papers  (2026-06-12T18:10:21Z)
• Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
  Pythagoras-Prover is a compute-efficient family of Lean theorem provers built for practical compute budgets.<n>For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT.<n>We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements.
  arXiv  Detail & Related papers  (2026-06-10T18:43:11Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction [95.91743732150233]
  Goedel-Prover-V2, a series of open-source language models, set a new state-of-the-art in automated theorem proving.<n>We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems.<n>Goedel-Prover-V2-32B achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode.
  arXiv  Detail & Related papers  (2025-08-05T16:28:22Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench.<n>We propose a novel framework that decouples high-level reasoning from low-level proof generation.<n>We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success.
  arXiv  Detail & Related papers  (2025-07-07T22:38:49Z)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models [13.498044623556737]
  This paper introduces textbfDSP+, an improved version of the Draft, Sketch, and Prove framework.<n>It features a emphfine-grained and integrated neuro-symbolic enhancement for each phase.<n> DSP+ solves 80.7%, 32.8%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench.
  arXiv  Detail & Related papers  (2025-06-13T06:25:59Z)
• Mathesis: Towards Formal Theorem Proving from Natural Languages [40.397691467863886]
  We develop Mathesis, the first end-to-end theorem proving pipeline processing informal problem statements.<n>It contributes Mathesis-Autoformalizer, the first autoformalizer using reinforcement learning to enhance the formalization ability of natural language problems.<n>It also proposes a Mathesis-Prover, which generates formal proofs from the formalized statements.
  arXiv  Detail & Related papers  (2025-06-08T09:04:14Z)
• Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving [44.5694120006447]
  We present a principled formulation of problem-solving as a deterministic Markov decision process.<n>We also present a novel framework, FPS, which utilizes existing FTP environments to perform process-verified problem-solving.<n>We construct three benchmarks on problem-solving: FormalMath500, a formalization of a subset of the MATH500 benchmark; MiniF2F-Solving and PutnamBench-Solving, adaptations of FTP benchmarks MiniF2F and PutnamBench.
  arXiv  Detail & Related papers  (2025-05-07T16:02:14Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems.<n>First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4.<n>Next, we develop a large dataset of formal proofs by training a series of provers.<n>Finally, we obtain the dataset Goedel-Pset-v1-solved, which contains proofs for over 800K statements from Goedel-Pset-v1
  arXiv  Detail & Related papers  (2025-02-11T15:27:35Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Autoformalization with Large Language Models [22.86710743804944]
  A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. We show large language models provide new prospects towards this goal. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6%$ to $35.2%$.
  arXiv  Detail & Related papers  (2022-05-25T09:53:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.