PaperlayerView exact revision on arXiv

Source-linked AI summary

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, Weiyang Liu

arXiv:2505.02735v1cs.AIcs.LG

TL;DR

Formal mathematical reasoning is difficult to benchmark comprehensively because existing datasets are limited in scope and scale. FormalMATH introduces a large, diverse Lean4 benchmark and evaluates theorem provers on it. The evaluation finds low success under practical budgets alongside domain bias and other proof-generation difficulties.

  • Problem

    Existing formal-mathematics benchmarks are limited in scope and size, leaving a need to assess theorem provers across diverse domains and difficulty levels.

    Source: §1 · p. 2

  • Method

    FormalMATH provides 5,560 formally verified Lean4 problems across domains and difficulty levels, with multi-LLM semantic verification checking alignment to the original problems.

    Source: §1 · p. 2, §3.2 · p. 5

  • Results

    16.46% was Kimina-Prover’s pass@32 score on FormalMATH-Full, and provers showed domain bias, simplified-tactic reliance, and reduced success with natural-language solution guidance in CoT scenarios.

    Source: §1 · p. 2, §6 · p. 15

  • Takeaways & Limitations

    FormalMATH presents a challenging benchmark and identifies cross-domain generalization and proof reasoning as open problems for theorem provers.

    Source: §6 · p. 15

    Automated tactics rely on fixed heuristics and pre-tagged lemmas, which can expand search, time out, or fail to provide witnesses for constructive proofs.

    Source: §5.2 · p. 13

Abstract

from arXiv · show

Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning.

1 Introduction

FormalMATH targets benchmark gaps in scope, size, and difficulty by assembling a large, diverse Lean4 problem set. The paper also introduces a human-in-the-loop construction pipeline and evaluates theorem provers on the resulting benchmark.

1 Introduction

  • Existing benchmarks are limited in scope and size, while reported success rates above 80.7% on some existing benchmarks suggest possible performance saturation.MiniF2F has 244 test problems and ProofNet has 186.Source: §1 · p. 2
  • FormalMATH contains 5,560 formally verified Lean4 statements across diverse domains and difficulty levels, from high-school Olympiad problems to undergraduate theorems.The benchmark spans areas including algebra, geometry, calculus, number theory, and discrete mathematics.Source: §1 · pp. 2–3
  • The human-in-the-loop pipeline combines multi-LLM autoformalization, semantic verification, and negation-based disproof filtering to reduce manual verification.The pipeline retains 72.09% of translated statements before manual review.Source: §1 · pp. 2–3
  • 16.46% was Kimina-Prover’s pass@32 score on FormalMATH-Full, while BFS-Prover reached 11.13% with a 1 × 32 × 100 sampling budget.Figure 2a compares theorem provers on the full benchmark.Source: §1 · p. 2, Figure 2 · p. 3
  • Existing provers show domain bias, doing well in algebra but poorly in calculus, and often reduce multi-step reasoning to single-tactic invocations.The introduction also reports that natural-language solution guidance can reduce proof success in CoT scenarios.Source: §1 · pp. 2–3

2 Related Work

Related work covers theorem-proving approaches and Lean4 benchmarks, including the manual formalization costs that motivate scalable dataset construction.

2 Related Work

  • Prior autoformalization validation often relies on ground-truth formalizations, and manual formalization in major Lean4 benchmarks limits scalability.FormalMATH uses automated multi-LLM filtering before manual review.Source: §2 · p. 3
  • Proof-search methods combine tactic generation with search, while single-pass generation produces entire proofs; the paper compares both approaches on FormalMATH.Search strategies include best-first search, Monte-Carlo tree search, and Lean-STAR sampling.Source: §2 · pp. 3–4
  • Lean4 benchmarks include library-derived resources and statement-only tasks requiring systems to generate proofs from scratch for compiler verification.The passage identifies LeanDojo as library-derived and MiniF2F [ZHP21], ProofNet [APS+23], FIMO [LSX+23], and PutnamBench [TLJ+24] as statement-only benchmarks.Source: §2 · p. 4
  • FormalMATH contributes 5,560 diverse problems drawn from high-school competition and undergraduate sources.The cited sources include Omni-Math [GSY+24], BlueMO, U-Math [CPA+24], Hardmath [FMW+24], and DEMIMATH.Source: §2 · p. 4

3 FormalMATH: A Large Formal Mathematical Reasoning Benchmark

FormalMATH is a 5,560-statement Lean4 benchmark spanning high-school through undergraduate mathematics. Its validation pipeline retains 72.1% of statements from the final LLM semantic-verification stage for expert review.

3.1 Overall Dataset Statistics

  • FormalMATH contains 5,560 verified Lean4 statements spanning high-school competition problems through undergraduate topics across diverse mathematical domains.Topics include algebra, number theory, discrete mathematics, geometry, calculus, and linear and abstract algebra.Source: §3.1 · p. 4

3.2 The Proposed Human-in-the-loop Pipeline for Data Collection and Filtering

  • The pipeline uses coding-specialized and theorem-proving LLMs, while a general-purpose LLM iteratively translates natural-language problems into Lean4 statements.Type-checked candidate statements form a corpus of 9,260 paired training examples for fine-tuning autoformalization models.Source: §3.2 · p. 5
  • Autoformalizers generate best-of-N Lean4 candidates, and compiler checks retain syntactically valid statements for semantic verification.Source: §3.2 · p. 5
  • Multiple LLMs back-translate Lean4 statements, compare them with the original problems, and retain only statements all models judge aligned.This step filters 60.7% of syntactically correct but semantically misaligned statements.Source: §3.2 · p. 5
  • 4.63% unanimous agreement on HardMath contrasts with around 30% for high-school competition problems, with lower consensus on undergraduate-level formalizations.Source: §3.2 · p. 5
  • Negation-based disproof applies off-the-shelf provers to statement negations; boundary-case testing and case analysis filtered out 1.6% of statements.The example uses n = 7 and systematic interval case analysis to derive contradictions.Source: §3.2 · p. 6
  • 72.1% of statements from the last LLM semantic-verification stage were retained, resulting in 21.7% successfully formalized statements after expert review.The reported pipeline rates are 30.1% before and 21.7% after expert verification.Source: §3.2 · p. 6

4 Experiments and Discussions

The experiments evaluate theorem provers on FormalMATH and a curated subset under varying models, domains, sampling budgets, and prompting strategies. Results show low overall success, uneven domain performance, limited returns from scaling, and stronger results from naive CoT than from natural-language-augmented CoT.

4.2 Evaluating Test-time Scaling of Formal Theorem Provers on FormalMATH-Lite

  • 18.78%: BFS-Prover rises from 27.10% via Pass@1×32×100 to 45.88% via Pass@32×32×100 under a 32× budget expansion.STP improves 4.58 percentage points, from 48.59% at Pass@32 to 53.17% at Pass@3200 despite a 100× sampling-budget increase.Source: Table 3 · p. 7, §4.2 · p. 10

4.1 Evaluating Formal Theorem Provers on FormalMATH

  • Kimina-Prover reaches only 16.46% Pass@32, while BFS-Prover reaches 11.13% Pass@1×32×100 on FormalMATH.Both use Qwen2.5-Math-7B as their base model, but differ in training approach.Source: §4.1 · p. 8
  • STP reaches 13.87% (+4.89% over SFT) and Goedel-Prover 13.53% (+4.55% over SFT), versus DeepSeek-V1.5-SFT at 8.97%.DeepSeek-V1.5-RL reaches 10.18%, a +1.21% gain over SFT.Source: §4.1 · p. 8
  • Goedel-Prover’s Pass@32 ranges from 50% in undergraduate algebra to 0% in discrete mathematics, alongside a training corpus with 68% applied mathematics and algebra.Precalculus reaches 33.71%, compared with 1.92% in differentiation and 0% in integration.Source: §4.1 · p. 9

4.2 Evaluating Test-time Scaling of Formal Theorem Provers on FormalMATH-Lite

  • FormalMATH-Lite contains 425 problems—359 high-school and 66 undergraduate—and balances solvable with unsolvable problems while aligning domain proportions with the full benchmark.It supports test-time scaling analysis when evaluating the full benchmark at large sampling budgets is prohibitively expensive.Source: §4.2 · p. 9
  • Ensembling four SPG methods raises STP’s 53.17% to 54.11% (+0.84%), while a misplaced tactic or type error invalidates a formal proof trajectory.The authors report that current verifier-guided search implementations remain computationally impractical and lack scaling efficiency.Source: §4.2 · p. 10

4.3 CoT Can Enhance Model Capabilities on Formal Mathematical Reasoning

  • At Pass@3200, DeepSeek-V1.5-SFT scores 50.6% with CoT, 49.2% with NL-augmented CoT, and 47.0% vanilla; RL scores 51.7%, 51.2%, and 49.8%, respectively.The experiments test SFT and RL models across the three strategies using test-time scaling up to Pass@3200; mean perplexity rises from 1.93 with naive CoT to 5.07 with NL-augmented CoT.Source: §4.3 · pp. 10–11
  • Naive CoT turns residue cases modulo 13 into explicit Lean hypotheses discharged by omega, whereas NL-augmented CoT omits tactic-level obligations.The authors hypothesize a mismatch between informal reasoning’s action space and Lean4’s tactic space.Source: §4.3 · p. 11

5 Delving into Common Error Patterns of Existing Provers

The section analyzes sampled prover failures and identifies recurring errors in automation use, complex inequalities, incomplete proofs, and redundant hypotheses. Case studies show these errors in algebraic and calculus problems.

5.2 Error Patterns Analysis and Case Study

  • The four common failure patterns are incomplete proofs, complex-inequality failures, improper automation use, and redundant hypothesis introduction.The analysis sampled 100 failed proofs per prover, used a two-stage LLM diagnosis and classification process, and had experts review and correct the results.Source: §5.1 · p. 12
  • Overused automation can expand search, time out, or mishandle constructive goals that require explicit witnesses.Tactics such as aesop, simp, and linarith depend on heuristics and pre-tagged lemmas; they may transform goals into irrelevant forms or leave constructive reasoning incomplete.Source: §5.2 · pp. 12–13
  • In a functional-equation example, the prover chooses the invalid witness a = 0 and uses simp without analyzing the core function.The required witness must satisfy both a ≤ 1 ∨ a > 0 and the stated functional equation.Source: §5.2 · p. 13
  • Direct nlinarith fails on a cyclic fractional inequality whose denominator expansion yields a degree-9 polynomial with about 55 monomials.The proof sketch instead applies AM-GM, derives reciprocal bounds for each term, and sums them.Source: §5.2 · p. 13
  • Redundant revert and reintro steps obscure proof logic when no induction or hypothesis strengthening is needed.The variables and hypotheses are already available in context, so the proof can use them directly.Source: §5.2 · p. 13
  • A calculus proof attempt stops without justifying limit-integral interchange or bounding the integrand’s tail decay.It also misuses monotonicity without verifying the domination or integrability conditions required for the Dominated Convergence Theorem.Source: §5.2 · pp. 14–15

6 Concluding Remarks

FormalMATH provides a large, diverse collection of verified Lean4 statements and a human-in-the-loop construction pipeline. Evaluation finds low prover success, domain bias, and reduced success with natural-language guidance in CoT scenarios.

6 Concluding Remarks

  • FormalMATH contains 5,560 formally verified Lean4 statements spanning domains from algebra to calculus and levels from high-school Olympiad to undergraduate curricula.The benchmark includes number theory and discrete mathematics among its domains.Source: §6 · p. 15
  • The human-in-the-loop pipeline combines specialized LLM formalization, multi-LLM semantic verification, and negation-based disproof filtering, retaining 72.09% of statements before manual review.Source: §6 · p. 15
  • 16.46% accuracy is the top performer’s result, alongside domain bias and over-reliance on simplified automation tactics.The evaluation also reports a negative impact of natural-language solution guidance on proof success in CoT scenarios.Source: §6 · p. 15

A Data Sources

The appendices describe the datasets used to build FormalMATH and illustrate the benchmark’s natural-language and Lean4 statements with calculus and number-theory examples.

A Data Sources

B Examples of Statements in FormalMATH

C The Error Types of Our Autoformalization Pipeline

The supplied appendix materials identify an error-classification statistics table and a figure showing the distribution of mathematical domains in FormalMATH-Lite.

C The Error Types of Our Autoformalization Pipeline

  • Table 7 is titled “Error Classification Statistics (%)”.Source: Table 7 · p. 22
  • Figure 8 depicts the distribution of mathematical domains in FormalMATH-Lite.Source: Figure 8 · p. 22

E.1 Errors in Definition

Definition errors arise when formalized statements fail to preserve the mathematical entities, types, or constraints of the source problem. Examples include omitted geometric ordering and mismatched variable types.

E.2 Errors in Definition

  • Mismatched variable types can cause failures when applying tactics specialized to a particular type.The passage identifies this as a common issue.Source: §E.1 · p. 23
  • A geometry formalization that gives only side lengths without specifying the vertices’ order on the circle may not uniquely define the quadrilateral.Different point orderings can share the same side lengths.Source: §E.1 · p. 23
  • Autoformalized definitions can mismatch mathematical entities or use variables with types different from those required by the problem.One example substitutes natural numbers for positive integers; another defines entities that lack mathematical significance and may not compile.Source: §E.1 · pp. 23–24

E.2 Errors in Expressions

Expression errors can change the intended logical structure or scope of a formal statement. The examples include misplaced quantifiers and other incorrect mathematical or logical operations.

E.2 Errors in Expressions

  • Expression errors also include incorrect arithmetic or logical operations, improper variable use, and incorrect application of mathematical or logical rules..Source: §E.2 · p. 24
  • A misplaced existential quantifier in a biconditional can link existence of a solution to the entire equivalence instead of only its left-hand claim.The corrected form scopes existence over the equation p = x^2 + 3y^2.Source: §E.2 · p. 25
  • A misplaced universal quantifier can misrepresent the intended scope of a polynomial identity and its classification.The proposed correction uses parentheses to delimit the equation governed by the quantifier.Source: §E.2 · pp. 25–26

E.3 Errors in Constraint Condition

Constraint-condition errors arise when formalized assumptions differ from the original problem’s requirements. The examples include omitted, spurious, and semantically weakened conditions.

E.3 Errors in Constraint Condition

  • Replacing “same minimum value” with a common lower bound weakens the intended relationship between two functions.The formalized condition says both functions are at least y for every x.Source: §E.3 · p. 26
  • The student-friend problem’s formalization omits the condition that each student has at most five friends.The passage says this omission may make the solution space differ from the original problem’s requirements.Source: §E.3 · p. 27
  • A formalized condition can add an assumption absent from the problem, as with the extra bound on c in the partial-fraction example.The added constraint is 0 ≤ c < 31.Source: §E.3 · p. 27

F Errors in Proof Goals

The appendix illustrates errors in proof goals and gives prompts for semantic verification, domain classification, proof generation, and error analysis. Its examples show how a formal goal can omit requested conclusions or misstate the logical form of a task.

F Errors in Proof Goals

  • A proof goal may verify a maximum value while omitting the requested characterization of all maximizing tuples, or frame a least-index task as an equivalence.The Fibonacci example requires both that m = 256 works and that no smaller positive integer works.Source: F Errors in Proof Goals · p. 28

G Prompt for Semantic Verification

  • The semantic-verification prompt asks models to back-translate Lean statements, compare them with the natural-language problems, and return binary judgments.The described approach uses group voting among LLMs.Source: G Prompt for Semantic Verification · p. 29

H Prompt for Domain Classification

  • The domain-classification prompt requests a brief problem summary and classification chains drawn from a specified mathematics framework.It limits classifications to at most three chains and requires framework-conforming categories.Source: H Prompt for Domain Classification · pp. 29, 31

I.1 Prompt for Vanilla Generation

  • The vanilla-generation prompt asks the model to complete the supplied Lean 4 code.Source: §I.1 · p. 32

I.2 Prompt for CoT Generation

  • The CoT-generation prompt requests a Lean 4 completion with explanatory comments preceding each code line.Source: §I.2 · p. 32

I.3 Prompt for NL-Augmented CoT

  • The NL-augmented CoT prompt adds a natural-language solution before asking for Lean code, and its example includes unsupported modular-arithmetic reasoning.The example’s informal residue claims are not materialized as the concrete hypotheses needed by Lean’s tactics.Source: §I.3 · p. 32

J Prompt for Error Pattern Diagnosis

K Prompt for Error Pattern Categorization

Loading 2505.02735v1…