Technical Summary: Faults in Our Formal Benchmarking

Problem Statement

While Large Language Models (LLMs) have advanced automated theorem proving in Lean, the reliability of the benchmarks used to evaluate them is compromised. A common intuition suggests that Lean benchmarks are "self-verifying" because the Lean kernel checks every proof artifact. However, this paper argues that the kernel only certifies that a proof establishes a given formal statement; it does not verify that the formal statement faithfully encodes the intended informal problem, nor that the evaluation harness is robust to trivial or adversarial solutions.

Consequently, benchmark scores can be misleading due to:

1. Specification Errors: The formal statement omits necessary hypotheses or constraints, making problems easier or vacuously true.
2. Formalization Errors: The translation from natural language to Lean misrepresents the problem (e.g., wrong domains, incorrect quantifiers).
3. Evaluation Loopholes: Flaws in the evaluation harness allow models to "pass" without demonstrating genuine capability (e.g., exploiting sorry, unsafe tactics, or kernel bugs).
4. Maintenance Decay: Rapid evolution of Lean and its libraries (mathlib) causes version drift, rendering datasets uncompileable or semantically shifted over time.

Methodology

The authors conducted a corpus-scale audit of five widely used Lean theorem-proving benchmarks and their forks: miniF2F, ProofNet, FormalMath, CombiBench, and ProverBench (covering approximately 10,000 problem variants).

The methodology involved three primary components:

1. Fault Taxonomy Development: The authors categorized defects based on where they enter the benchmarking pipeline: Fidelity Issues (during formalization), Evaluation Loopholes (during proof checking/reporting), and Maintenance Issues (source errors and version drift).
2. Automated Static Checkers: They implemented 12 Lean 4 metaprograms to detect mechanical hazards. These checkers use semantic guard proving (via tactics like omega, assumption, and simp) to identify issues such as:
   • Counterexamples (concrete values disproving the theorem).
   • Vacuous theorems (unsatisfiable hypotheses).
   • Unsound axioms or sorry usage in proofs.
   • Lean-specific arithmetic hazards (division by zero, truncated natural subtraction, analytic domain violations).
3. LLM-Assisted Semantic Audit: Recognizing that static analysis cannot detect semantic mismatches (e.g., missing hypotheses that are mathematically implied but not syntactically present), the authors evaluated LLMs on a labeled 92-problem challenge set. They used few-shot prompting to classify errors across six categories (e.g., specification errors, domain mismatches, formalization errors).

Key Results

The audit surfaced 4,833 findings across the datasets, with 398 carrying a machine-checkable certificate of unprovability or vacuity.

• Defect Distribution:
  • FormalMath: 3,250 findings (dominated by division by zero and natural subtraction issues).
  • ProverBench: 370 findings (high rate of axiom usage and counterexamples).
  • miniF2F variants: 135–193 findings per variant, highlighting issues with incomplete formalization and version proliferation.
  • ProofNet: 67–82 findings, often related to underspecification.
• LLM Verification: Static checkers produced false positives when guards were embedded in type definitions or structures. LLM filtering (using models like Gemini 3.0 Flash and GPT-5.2) reduced findings by ~35% on ProverBench while preserving all confirmed true positives, achieving ~83% accuracy.
• Semantic Audit Performance: LLMs achieved high recall (0.80–0.91) but low precision (0.20–0.30) in detecting semantic errors. They were significantly better at spotting explicit specification errors (F1 ~0.51) than deep formalization errors (F1 ~0.18), which require understanding mathematical intent.
• Impact on Scores: The authors demonstrated that defects have bidirectional effects on reported prover scores:
  • Deflation: Unprovable or false statements (due to source errors) add impossible items to the denominator, artificially lowering scores.
  • Inflation: Weakened formalizations (missing hypotheses) make problems easier, artificially inflating scores.
  • Example: Correcting 20 flawed problems in a subset allowed DeepSeek-Prover-V2-7B to solve 3/20 and Kimina-Prover-8B to solve 2/20, whereas they solved 0/20 on the original flawed statements. Conversely, repairing weakened statements in ProofNet lowered pass rates for tested provers.

Key Contributions

1. Comprehensive Audit: A large-scale, systematic audit of the five major Lean benchmarks, revealing that defects are systematic rather than anecdotal.
2. Fault Taxonomy: A structured classification of benchmark defects into Fidelity, Evaluation, and Maintenance categories, clarifying that different interventions are required for each (e.g., static analysis for encoding hazards vs. human review for semantic intent).
3. Tooling Suite:
   • Static Checkers: A suite of 12 automated checkers implemented as Lean 4 metaprograms.
   • Audit Prompts: A set of recall-oriented prompts for LLMs to assist in semantic auditing.
   • Corrected Snapshots: Release of corrected dataset variants and audit results.
4. Release Standards: Proposals for trustworthy benchmark creation, including:
   • Using proof wanted instead of sorry to prevent sorry from acting as an axiom.
   • Disabling autoImplicit to force explicit type declarations.
   • Prohibiting axioms in problem files.
   • Pinning Lean/mathlib versions to prevent drift.

Significance and Claims

The paper claims that while Lean's kernel provides mathematical certainty about the relationship between a proof and a formal statement, it does not guarantee the validity of the benchmark itself. The authors argue that the current state of formal benchmarking suffers from a "trust gap" where specification fidelity and evaluation robustness are often overlooked.

The significance of this work lies in:

• Reproducibility: Highlighting that version proliferation and undocumented forks make cross-paper comparisons unreliable.
• Evaluation Integrity: Demonstrating that reported scores in automated theorem proving are often artifacts of dataset defects rather than genuine model capability.
• Actionable Remediation: Providing a practical toolkit (checkers, prompts, standards) to help benchmark creators identify and fix defects before release, thereby improving the quality of training data and the trustworthiness of evaluation results.

The authors remain modest, acknowledging that their audit is not a complete human-verified enumeration of all defects and that some issues require deep mathematical insight or Lean expertise to resolve. However, they assert that their taxonomy and tools are sufficient to prevent high-impact failures and guide future dataset stewardship.