RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving

• URL: http://arxiv.org/abs/2609.00062v1
• Date: Sun, 30 Aug 2026 14:23:48 GMT
• Title: RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
• Abstract summary: 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.
• Score: 27.43470148162019
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Data contamination undermines the reliable evaluation of large language models (LLMs) on mathematical problem solving. While rewriting-based evaluation mitigates memorization, existing methods lack guarantees of problem validity and answer correctness. We propose Proof-Verified Benchmark Rewriting (RePro), the first framework to integrate Lean-oriented neural automated theorem provers (ATPs) into benchmark rewriting, which rewrites problems and regenerates answers with correctness ensured by Lean-verified proofs. Experiments on GSM8K and MATH show that RePro's retained rewritten instances achieve 100% well-definedness, feasibility, and answer correctness, while existing methods still produce invalid or incorrect instances. Moreover, several models exhibit accuracy drops on proof-verified rewritten benchmarks, suggesting that their performance is sensitive to surface-level and structural variations and may partly reflect memorization effects. Our source code and data are available at https://github.com/AI4Engi/RePro.

Related papers

• Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving [13.87786274932945]
  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.
  arXiv  Detail & Related papers  (2026-06-28T16:46:36Z)
• Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs [6.320612572570053]
  Mask-Proof is a pipeline that turns real proofs into automatically checkable masked-step tasks.<n>The resulting Mask-ProofBench contains 292 curated problems across diverse research areas.<n>Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning.
  arXiv  Detail & Related papers  (2026-06-13T11:26:09Z)
• Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts [19.455779459310982]
  We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines.<n>We propose a process-guided approach inspired by human proof-refactoring.
  arXiv  Detail & Related papers  (2026-06-02T14:56:10Z)
• Learning to Repair Lean Proofs from Compiler Feedback [4.55626337217127]
  We study Lean proof repair as a supervised learning problem.<n>We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised theorems.<n>We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers.
  arXiv  Detail & Related papers  (2026-02-03T01:53:56Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  This paper formalizes the Refinement Provenance Inference (RPI) audit task as Refinement Provenance Inference (RPI)<n>We propose RePro, a logit-based framework that fuses teacher-forced likelihood features with logit-ranking signals.<n>During training, RePro learns a transferable representation via shadow fine-tuning, and uses a lightweight linear head to infer provenance on unseen victims without training-data access.
  arXiv  Detail & Related papers  (2026-01-05T10:16:41Z)
• Incorporating Self-Rewriting into Large Language Model Reasoning Reinforcement [54.63337314382886]
  We introduce self-rewriting framework, where a model rewrites its own reasoning texts, and subsequently learns from the rewritten reasoning to improve internal thought process quality.<n>For algorithm design, we propose a selective rewriting approach wherein only "simple" samples, defined by the model's consistent correctness, are rewritten.<n>Experiments on diverse tasks with different model sizes validate the effectiveness of self-rewriting.
  arXiv  Detail & Related papers  (2025-11-20T13:10:52Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Repairing vulnerabilities without invisible hands. A differentiated replication study on LLMs [5.10123605644148]
  Automated Vulnerability Repair (AVR) is a fast-growing branch of program repair.<n>Recent studies show that large language models (LLMs) outperform traditional techniques.
  arXiv  Detail & Related papers  (2025-07-28T16:39:16Z)
• 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)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  We propose a new protocol for inconsistency detection benchmark creation and implement it in a 10-domain benchmark called SummEdits. Most LLMs struggle on SummEdits, with performance close to random chance. The best-performing model, GPT-4, is still 8% below estimated human performance.
  arXiv  Detail & Related papers  (2023-05-23T21:50:06Z)

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.