PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Xiyuan Zhou, Zhuoqi Li, Xinlei Wang, Yirui He, Yuhao Wu, Yuheng Cheng, Yan Xu, Junhua Zhao, Jinjin Gu

arXiv:2609.00062v1cs.CLcs.AI

TL;DR

Data contamination and heuristic rewriting weaken confidence that mathematical benchmark scores reflect genuine reasoning and correct evaluation targets. RePro integrates LLM rewriting with Lean-oriented theorem proving and proof-assistant checking, retaining only formally verified instances; on GSM8K and MATH, retained instances achieve 100% well-definedness, feasibility, and answer correctness. Its coverage remains limited by ATP capability and Lean formalization requirements.

  • Problem

    Data contamination threatens reliable LLM mathematical evaluation, while existing rewriting methods lack guarantees of problem validity and answer correctness.

  • Method

    RePro combines LLM-generated rewriting and screening with Lean-oriented ATP proof search and proof-assistant checking, retaining only formally verified instances.

  • Results

    On GSM8K and MATH, RePro achieves 100% well-definedness, feasibility, and answer correctness among retained rewritten instances, whereas prior methods still produce invalid or incorrect instances.

  • Takeaways & Limitations

    Proof-verified rewriting provides reliable retained benchmarks and can reveal model-specific sensitivity to benchmark reformulation and potential memorization-related signals.

  • Takeaways & Limitations

    RePro depends on ATP capability and Lean formalization, so correct solvable problems may be filtered out when proofs are not found or problems cannot be expressed formally.

Abstract

from arXiv · show

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.

1 Introduction

Rewriting can reduce contamination but does not reliably guarantee valid problems or correct answers. RePro combines LLM rewriting with Lean-oriented theorem proving and proof-assistant checking to retain formally verified instances.

  • Data contamination can let LLMs score highly through memorization rather than genuine mathematical reasoning.
  • Heuristic rewriting and model-generated validation make problem validity and answer correctness difficult to guarantee.
  • RePro combines diverse LLM-generated rewrites with conservative screening, ATP proof search, and Lean verification.
  • Only rewritten instances with formally verified reference answers are retained in the released benchmarks.
  • 100% of retained RePro instances satisfy well-definedness, feasibility, and answer correctness on both GSM8K and MATH.Prior methods still produce invalid problems or incorrect reference answers.
  • RePro evaluates rewritten benchmarks using well-definedness, feasibility, and answer correctness as reliability-oriented criteria.

2 Related Work

Dynamic benchmark generation creates new evaluation instances through rewriting and related automated approaches. RePro contributes a verification pipeline that progressively filters rewrites and uses kernel-checked Lean proofs, addressing reliability concerns underexplored in prior work.

  • Dynamic Benchmark Generation: Benchmark rewriting applies semantic or structural transformations such as paraphrasing, numerical substitution, and structural perturbation.
  • Dynamic Benchmark Generation: Dynamic benchmark methods aim to reduce memorization cues while reusing existing evaluation resources.
  • RePro progressively filters rewritten instances to obtain valid questions with verified answers.
  • Neural Lean provers generate candidate proof scripts that Lean checks before acceptance, while benchmark verification remains underexplored.

3 RePro

RePro uses staged screening, Lean formalization, theorem-prover search, and proof checking to construct rewritten benchmarks with reliable problem statements and reference answers. Candidates are retained only after validity checks, verified proofs, and target-answer alignment.

  • Rewriting and Feasibility Screening: RePro generates rewrites through numerical reparameterization, logical restructuring, constraint modification, and contextual reconstruction.
  • Feasibility Screening: Feasibility screening removes ambiguous, inconsistent, contradictory, unrealistic, or infeasible candidate problems.Feasibility concerns semantic and constraint consistency, not merely formal derivability.
  • Executable Formalization: Passing candidates are translated into executable Lean specifications and checked for syntactic and semantic consistency.The semantic checker uses a conservative all-pass policy across three temperature-zero judgments.
  • Verification Boundaries: Semantic screening does not formally guarantee natural-language-to-Lean equivalence; proof verification and answer alignment provide later correctness checks.
  • Proof-level Verification: ATP-generated candidate proofs are verified in Lean, and only instances with successfully verified answers are retained.Proof-level verification is the only stage that determines answer correctness.
  • Answer Alignment: Answer alignment accepts only proof-extracted answers that exactly match the quantity requested by the rewritten problem.No additional computation, normalization, simplification, or inference is allowed.

4 Evaluation Criteria

Reliable benchmark instances require both valid problems and correct reference answers, especially after rewriting can alter semantics or constraints. RePro evaluates these requirements through well-definedness, feasibility, and answer correctness using a Lean-, ATP-, and screening-based pipeline.

  • A reliable evaluation instance must contain a clearly specified, logically coherent, solvable problem and a correct ground-truth answer.
  • Rewriting can change surface wording, problem semantics, constraints, or answer consistency, creating ambiguity, missing information, or incorrect references.
  • Well-definedness: Well-definedness requires sufficient and unambiguous information to determine the task and its objective.
  • Feasibility: Feasibility requires a valid solution under basic real-world or task-specific constraints.
  • Answer Correctness: Answer correctness requires successful formalization, valid proof verification, and matching to the requested target quantity.
  • For each criterion c, the reported rate is computed as Nc/N over the total generated rewritten instances N.

5 Experimental Methodology

RePro is evaluated on GSM8K and MATH against automatic rewriting baselines using diverse open-source language models and a proof-verification pipeline. Its experiments measure rewriting quality, generation coverage, and model performance under controlled benchmark transformations.

  • Datasets: RePro is evaluated on GSM8K and MATH, while harder benchmarks were excluded because current ATP bottlenecks caused very low generation rates.GSM8K contains grade-school mathematics problems, whereas MATH covers five difficulty levels.
  • Evaluation Metrics: Table 1 compares well-definedness, feasibility, answer correctness, and generation rate on full generated sets and RePro-success subsets.The table reports both rewriting quality and coverage under two evaluation scopes.
  • Models: The evaluation covers Qwen, Llama, DeepSeek-R1, and Gemma model families across multiple parameter scales.This selection supports comparisons across architectures and training methods while controlling model scale.
  • RePro Pipeline: RePro uses LLM rewriting and feasibility screening, Lean 4 formalization, ATP proof generation, and Lean 4 verification.The specified pipeline uses Qwen3-MAX, Goedel-Formalizer-V2-8B, and Goedel-Prover-V2-8B.
  • Baselines: Baselines include Auto-Dataset, ITD, and VarBench, which generate rewritten instances while preserving semantic or computational structure.Their approaches range from semantic similarity rewriting to variable resampling with executable solution functions.

6 Results

RePro produces highly reliable retained rewrites and exposes how ATPs, rewriters, and proof-search budgets affect coverage. Proof-verified rewriting also reveals substantial, model-specific accuracy changes across reformulated mathematical problems.

  • Rewriting Quality Comparison: 100% well-definedness, feasibility, and answer correctness are achieved by RePro on both GSM8K and MATH retained instances.Existing methods continue to produce invalid problems or incorrect reference answers.
  • Rewriting Quality Comparison: AutoDataset, ITD, and VarBench reach only 79.99%, 81.15%, and 87.36% correctness on MATH, versus 87.10%, 89.11%, and 95.14% on GSM8K.Their feasibility rates also remain below 100%, and baseline invalidity persists on the RePro-success subset.
  • Rewriting Quality Comparison: Human judgments fully agree with automatic reliability results in an independent audit of 2,400 sampled rewritten instances.The audit covers RePro and all baselines.
  • Generation Factors: Stronger ATPs and rewriters improve generation coverage, while increasing the ATP call limit provides additional but diminishing gains.Generation success also decreases as MATH difficulty rises from Level 1 to Level 5.
  • ATP Capability: 84.6% miniF2F pass@32 success is reported for Goedel-Prover, compared with 68.0% for DeepSeek-Prover and 63.1% for Kimina-Prover.Generation success generally follows ATP capability, although DeepSeek-Prover performs worse than expected from its miniF2F result.
  • ATP Capability: 59.16% MATH generation rate lets RePro match VarBench's 58.76% while retaining validity and answer correctness through formal verification.The comparison illustrates a quality-coverage trade-off under stricter generation constraints.
  • Rewriter Capability: 88.31% GSM8K generation is achieved by Qwen3-MAX, compared with 68.55% for Qwen3-32B and 58.87% for Qwen3-8B.Qwen3-MAX has the highest success rate across datasets and difficulty levels and is used as the default rewriter.
  • ATP Call Limit: 88.31% GSM8K and 59.16% overall MATH generation rates are reached at pass@3, up from 76.21% and 50.17% at pass@1.The pass@2-to-pass@3 improvement is smaller than the pass@1-to-pass@2 improvement.

7 Conclusion

RePro addresses reliability in contamination-resistant mathematical benchmarking by retaining only rewritten instances that are formalized and Lean-verified. On GSM8K and MATH, it achieves fully well-defined, feasible, and correct retained instances while revealing model-specific sensitivity to reformulation.

  • Conclusion: RePro integrates ATPs and proof-assistant checking to retain rewritten instances with formally supported reference answers.The framework targets reliability in rewriting-based evaluation for contamination-resistant LLM benchmarking.
  • Conclusion: 100% well-defined, feasible, and correct retained instances are achieved on MATH and GSM8K, while existing methods still produce invalid problems or incorrect answers.The conclusion also reports sensitivity to benchmark reformulation and signals of potential memorization or benchmark-specific pattern reliance.

Limitations

RePro combines LLM rewriting with conservative screening, Lean formalization, ATP proof search, and proof-assistant verification. Its main limitations are dependence on prover capability, Lean formalizability, and heuristic semantic alignment checks.

  • LLM roles: LLMs generate rewrites, screen feasibility, assess semantic consistency, extract proof-grounded answers, and classify final-answer matches.These uses are constrained by later formal verification and target matching.
  • Verification pipeline: RePro retains rewritten problems only after feasibility screening, Lean compilation, proof generation, Lean checking, and answer validation.The pipeline uses staged filters rather than relying on rewriting alone.
  • Formal verification: Proof acceptance requires a compiling Lean statement and a generated proof that passes Lean checking without using sorry.Formal proof generation is therefore subject to kernel-level verification.
  • Semantic alignment: Semantic alignment screening is conservative and may discard valid formalizations, but it is not a formal proof of natural-language-to-Lean equivalence.The screen checks apparent task consistency before proof search.
  • Answer recovery: Post-proof answer extraction is read-only: candidates must be copied from the Lean proof, while final-answer classification checks target alignment without new computation.This separates proof verification from answer reporting.

D Obtaining the Final Answer from Verified Proofs

RePro recovers answers from verified proofs through literal extraction followed by target-answer checking. This design preserves traceability and prevents post-proof computation or selection from introducing new reasoning.

  • Answer-recovery design: RePro divides post-proof answer recovery into literal extraction and final-answer checking.The two stages address proof traceability and target alignment separately.
  • Literal extraction: Literal extraction copies only spans appearing verbatim in the verified proof and forbids computation, normalization, inference, or rewriting.For example, 2 + 3 cannot be converted to 5 unless 5 also appears explicitly.
  • Multiple quantities: For multiple target quantities, the extractor returns all corresponding proof spans separated by commas without reordering or reformatting.The output must preserve the proof-grounded representation.
  • Target matching: Final-answer checking distinguishes requested answers from intermediate, wrong-target, unresolved, or unknown values.A candidate is retained only when it is classified as final and matches the rewritten problem’s target.
  • Guarantees: The design guarantees traceability to the verified proof, prevents answer generation after verification, and aligns output with the requested quantity.These properties keep reported answers proof-grounded and query-aligned.

E Dataset Selection and Data Distribution

RePro evaluates rewritten instances from GSM8K and MATH, retaining roughly 200 verified examples per subset through rejection sampling. Retention declines with MATH difficulty, so the balanced retained set does not preserve the original distribution.

  • Dataset selection: GSM8K and MATH were selected because they are widely used and compatible with current Lean-oriented ATP capabilities.GSM8K supports controlled grade-school rewriting, while MATH spans five difficulty levels.
  • Difficulty boundary: 0% RePro generation success was observed on a preliminary sample of 30 AIME 2025 problems.The paper therefore leaves harder benchmarks such as AIME and Omni-MATH for future work as ATP capabilities improve.
  • Sampling protocol: Rejection sampling continues until approximately 200 verified rewritten instances are obtained for each subset.Only candidates satisfying all verification criteria enter the final evaluation set.
  • Retention rates: Retention rates are 88.3% for GSM8K and 92.2%, 75.8%, 73.9%, 57.1%, and 33.7% for MATH LV1–LV5, respectively.The declining rates indicate difficulty-dependent selection under current formalization and proving capabilities.
  • Data distribution: The retained subset is nearly uniform across difficulty levels but does not preserve MATH’s original difficulty distribution.Harder levels require substantially more sampled candidates because their retention rates are lower.

G Representative Successful RePro Cases

Representative cases show RePro retaining arithmetic, set-valued, symbolic-factorization, and optimization rewrites. Each passes feasibility, formalization, proof verification, and target-answer checks.

  • GSM8K unit conversion: The unit-conversion case verifies a rewritten answer of 5 cents per sheet from 1600 cents and 320 sheets.The proof preserves the requested cost-per-sheet quantity and the monetary/counting structure.
  • Set-valued answer: The inverse-function case verifies that the solution set for g(x) = g^-1(x) is {3}.Lean proves set equality, not merely that one candidate satisfies the equation.
  • Symbolic factorization: The factorization case rewrites 36 −4x2 to 81 −9y2 and verifies the answer 9(3 −y)(3 + y).Lean checks the algebraic identity between the expanded and factored expressions.
  • Optimization: The optimization case verifies y = 1873/4 as feasible and no larger than any other positive value satisfying the condition.The formal statement encodes positivity, the area inequality, and minimality.
  • Cross-case verification: Across the cases, retained instances pass feasibility, compilation, semantic alignment, Lean proof verification, and target-answer matching.The examples span numerical, set-valued, symbolic, and optimization answer types.
  • Interpretation: The reported 100% reliability metrics apply to retained rewritten instances, not to all raw LLM-generated rewrites.Generation and verification are decoupled, and unreliable candidates are filtered out.

I Confound Analysis for Rewriting Sensitivity

RePro analyzes whether performance changes after proof-verified rewriting reflect simple surface, numeric, and length changes or deeper complexity differences. Surface and numeric changes show near-zero associations with accuracy drops, whereas solution and Lean proof complexity show weak positive associations; improvement cases also reveal sensitivity to clearer problem specification.

  • Analysis setup: The analysis uses RePro-retained MATH instances containing original problems, proof-verified rewrites, and corresponding Lean proofs.Correctness is evaluated for each original–rewritten problem pair and model.
  • Interpretation: The results show a bidirectional pattern: many models drop in accuracy after rewriting, while some improve on particular rewritten instances.Accordingly, performance changes are interpreted as model-specific sensitivity to benchmark reformulation, with possible memorization-related signals rather than proof of contamination.
  • Confound metrics: Problem length change measures whether rewriting makes statements longer or shorter, while surface-form distance measures string-level divergence after normalization.Surface similarity is computed after lowercasing and whitespace normalization; larger divergence values indicate greater surface-form change.
  • Correlation results: Near-zero correlations show that surface-level and numeric changes are not meaningfully associated with model-averaged accuracy drops.The numeric analysis covers range changes and changes in the number of numeric quantities.
  • Correlation results: Weak positive correlations link solution-length change, rewritten solution length, and Lean proof length with accuracy drops.These metrics leave increased solution and formal-proof complexity as plausible contributing factors.
  • Improvement cases: Manual improvement cases suggest that rewriting can improve accuracy by clarifying the target quantity, condition structure, or information flow rather than reducing mathematical difficulty.One example attributes improvement to directly stating whether the requested output is the x-value or the maximum function value.

J Analysis of Failure Cases in DeepSeek-Prover-V2-7B

DeepSeek-Prover-V2-7B fails through output corruption, goal-inappropriate tactic selection, semantic drift, repetition, and incomplete generation. These failures show that syntactic validity or execution alone does not ensure mathematically correct, well-defined benchmark instances.

  • Inappropriate Tactic Selection: The prover repeatedly applies generic tactics such as norm_num or omega when the goal requires algebraic normalization over Real.For symbolic polynomial identities, tactics such as ring or ring_nf are appropriate, whereas repeated generic tactics fail to resolve the goal.
  • Semantic Drift in Theorem Statement: Generated theorem statements can drift from intended problem semantics, causing proof attempts to target incorrect or irrelevant goals.The failure concerns the theorem target itself rather than merely the subsequent proof script.
  • Output Boundary Corruption: More than 94% of unsuccessful proofs exhibit output-boundary corruption, making stable Lean theorem generation the dominant failure challenge.Unexpected special tokens can break theorem syntax, and their contents vary across samples, preventing uniformly reliable string-level repair.
  • Repetitive Tactic Generation: Approximately 39% of failed proofs contain excessive repetition of the same tactic, often without meaningful progress toward completion.Once the proof state becomes unstable, the prover may repeatedly emit common arithmetic tactics instead of maintaining goal-directed reasoning.
  • Incomplete Generation: Some generations terminate with incomplete tactic sequences or partially generated tokens, consistent with truncation or decoding instability.These failures can leave proof scripts unfinished even when the intended theorem is otherwise correctly formulated.
  • Implications for Benchmark Reliability: Format consistency and successful execution alone cannot establish well-definedness, feasibility, and answer correctness for generated benchmark instances.RePro therefore screens problem validity and retains answers only when formal statements admit Lean-verified proofs matching the requested targets.
Loading 2609.00062v1…