Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

• URL: http://arxiv.org/abs/2606.29493v1
• Date: Sun, 28 Jun 2026 16:46:36 GMT
• Title: Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving
• Abstract summary: Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof.<n>We audit five widely used Lean theorem-proving benchmarks and their forks, using corpus-scale static checkers to surface 4,833 findings.<n>We propose a fault taxonomy, a suite of automated checkers and recall-oriented semantic audit prompts, and release standards to guide the creation of formal math datasets.
• Score: 13.87786274932945
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof. However, the kernel only checks that a proof establishes a \emph{formal} statement; it does not verify that the statement faithfully encodes the intended informal problem, nor that evaluation harnesses are robust to trivial or adversarial solutions. We audit five widely used Lean theorem-proving benchmarks and their forks, using corpus-scale static checkers to surface 4,833 findings, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms. We also document semantic defects such as missing hypotheses, problem simplification, incomplete or incorrect translations, and Lean-specific specification hazards. Beyond dataset construction, we survey evaluation-time failure modes and show, on corrected subsets, that defects can both inflate and deflate reported prover scores. We propose a fault taxonomy, a suite of automated checkers and recall-oriented semantic audit prompts, and release standards to guide the creation of formal math datasets and to make evaluation more reproducible and trustworthy. Our checkers, audit prompts, and corrected dataset snapshots are available at https://github.com/Shashi456/atp-checkers.

Related papers

• RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving [27.43470148162019]
  We propose Proof-Verified Benchmark Rewriting (RePro) to integrate Lean-oriented neural theorem provers into benchmark rewriting.<n>RePro rewrites problems and regenerates answers with correctness ensured by Lean-verified proofs.<n> Experiments on GSM8K and MATH show that RePro's retained rewritten instances achieve 100% well-definedness, feasibility, and answer correctness.
  arXiv  Detail & Related papers  (2026-08-30T14:23:48Z)
• 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)
• Bayesian control for coding agents [63.64172141184361]
  We propose a cost-sensitive sequential hypothesis testing framework for coding agents.<n>A Bayesian controller maintains a belief over correctness and decides whether to gather more evidence, refine the candidate, verify it, or stop.<n>We show that the belief state yields an interpretable correctness score that outperforms token-probability and raw tool-success baselines for uncertainty quantification.
  arXiv  Detail & Related papers  (2026-06-23T11:41:32Z)
• Stress-Testing Neural Network Verifiers with Provably Robust Instances [10.017475431603389]
  We introduce a reusable framework for generating verification instances with ground-truth labels.<n>We also introduce the verification Difficulty Profile, a collection of estimable quantities capturing distinct sources of instance hardness.<n>Using our framework and these profiles, we evaluate five state-of-the-art verifiers and show that different instances stress distinct aspects of the verification pipeline.
  arXiv  Detail & Related papers  (2026-05-16T20:56:52Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T is a framework that evaluates the semantic correctness of formal theorems.<n>We construct a benchmark from 5 real-world Lean 4 repositories.<n>Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric.
  arXiv  Detail & Related papers  (2026-04-26T13:24:20Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  We introduce ProofGrid, a benchmark suite for evaluating reasoning through machine-checkable proofs.<n>ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling.<n> Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts.
  arXiv  Detail & Related papers  (2026-04-07T01:19:41Z)
• What Do Claim Verification Datasets Actually Test? A Reasoning Trace Analysis [34.429649156970015]
  We generate structured reasoning traces for 24K claim-verification examples using GPT-4o-mini.<n>We find that direct evidence extraction dominates, while multi-sentence synthesis and numerical reasoning are severely under-represented.
  arXiv  Detail & Related papers  (2026-04-02T05:54:51Z)
• InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
  InFi-Check is a framework for interpretable and fine-grained fact-checking of large language models.<n>InFi-Checker provides supporting evidence, classify fine-grained error types, and produce justifications along with corrections.<n>Experiments show that InFi-Checker achieves state-of-the-art performance on InFi-Check-FG.
  arXiv  Detail & Related papers  (2026-01-10T20:00:17Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  We introduce Veracity Search (VS), a discrete search algorithm over veracity assignments.<n>It performs otherwise intractable inference in the posterior distribution over latent veracity values.<n>It generalizes VS, enabling accurate zero-shot veracity inference in novel contexts.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• SoundnessBench: A Soundness Benchmark for Neural Network Verifiers [45.86647998712757]
  We develop a new benchmark for NN verification, named "SoundnessBench", specifically for testing the soundness of NN verifiers.<n>SoundnessBench consists of instances with deliberately inserted counterexamples that are hidden from adversarial attacks.<n>We demonstrate that our training effectively produces hidden counterexamples and our SoundnessBench successfully identifies bugs in state-of-the-art NN verifiers.
  arXiv  Detail & Related papers  (2024-12-04T09:24:33Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheck is a framework for building customized automatic fact-checking systems.<n>It allows users to easily customize an automatic fact-checker and verify the factual correctness of documents and claims.<n>CheckerEVAL is a solution for gauging the reliability of automatic fact-checkers' verification results using human-annotated datasets.
  arXiv  Detail & Related papers  (2024-05-09T07:15:19Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Interpretable Automatic Fine-grained Inconsistency Detection in Text Summarization [56.94741578760294]
  We propose the task of fine-grained inconsistency detection, the goal of which is to predict the fine-grained types of factual errors in a summary. Motivated by how humans inspect factual inconsistency in summaries, we propose an interpretable fine-grained inconsistency detection model, FineGrainFact.
  arXiv  Detail & Related papers  (2023-05-23T22:11:47Z)
• Zero-shot Faithful Factual Error Correction [53.121642212060536]
  Faithfully correcting factual errors is critical for maintaining the integrity of textual knowledge bases and preventing hallucinations in sequence-to-sequence models. We present a zero-shot framework that formulates questions about input claims, looks for correct answers in the given evidence, and assesses the faithfulness of each correction based on its consistency with the evidence.
  arXiv  Detail & Related papers  (2023-05-13T18:55:20Z)

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.