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

Data contamination poses a significant challenge to the reliable evaluation of large language models (LLMs) when assessing mathematical problem-solving capabilities, as training corpora and evaluation benchmarks often share public sources. While dynamic methods like benchmark rewriting aim to mitigate memorization, existing approaches rely on heuristic validation—such as LLM-as-a-Judge or human inspection—which makes it difficult to guarantee problem validity and answer correctness.

To address this lack of deterministic reliability, the authors propose Proof-Verified Benchmark Rewriting (RePro), a framework that integrates formal verification into the benchmark rewriting process. RePro is designed to create mathematically rigorous rewritten benchmarks by integrating Lean-oriented neural automated theorem provers (ATPs) into a unified verification pipeline.

The methodology involves several stages of progressive filtering:

1. Rewriting and Feasibility Screening: LLMs generate diverse candidate rewrites using various strategies, including numerical reparameterization, logical restructuring, constraint modification, and contextual reconstruction. This initial stage filters out instances that are ill-defined, ambiguous, internally inconsistent... or infeasible, ensuring basic problem validity.

2. Executable Formalization: The remaining candidates are converted into machine-verifiable formal statements in Lean. This process includes a semantic check—a conservative all-pass policy where the LLM is queried three times with temperature zero to ensure the Lean statement semantically aligns with the natural language problem, preserving the same quantities, conditions, logical structure, object type... and target quantity.

3. Proof-level Verification: An automated theorem prover (ATP) searches for candidate proofs for the formalized problems. These proofs are then subjected to Lean kernel-level verification by a proof assistant. Only instances whose answers can be successfully proven and verified in Lean are retained, establishing the definitive source of answer correctness.

4. Target-Answer Matching: A final step ensures that the extracted reference answer corresponds exactly to the quantity requested by the rewritten problem, preventing post-hoc reasoning or interpretation errors.

Empirical results demonstrate RePro's effectiveness on both GSM8K and MATH datasets. The authors report that RePro’s retained instances achieve 100% well-definedness, feasibility, and answer correctness, a feat that existing methods still produce invalid or incorrect instances. Furthermore, the study shows that proof-verified rewriting can serve as a reliable diagnostic tool for analyzing model behavior; several models exhibit accuracy drops on these benchmarks, suggesting their performance is sensitive to surface-level and structural variations and may reflect memorization effects.

The authors conclude that RePro provides a robust solution for creating evaluation datasets with verifiable correctness, ensuring the reliability of the benchmark against data contamination.

The following improvements are derived from the principles of Proof-Verified Benchmark Rewriting (RePro) and outline how they can be integrated into AI systems, specifically for training, evaluation, and self-correction.

---

1. Implementation of Deterministic Formal Validation Pipelines

• Improvement: Replacing heuristic validation (e.g., LLM-as-a-Judge) with a rigorous, multi-stage pipeline involving automated theorem provers (ATPs) and formal proof assistants (Lean). This ensures that every generated problem is not just plausible, but mathematically verifiable.

• Mechanism: The system must enforce a progressive filtering sequence:

• Feasibility Screening: Reject candidates that are ill-defined, ambiguous, or violate implicit real-world constraints (e,g., negative quantities).

• Executable Formalization: Convert the remaining natural language problems into precise Lean formal statements.

• Proof-level Verification: Use ATP to generate candidate proofs for the formalized problem and accept only those instances whose answers are supported by a valid, kernel-verified proof.

2. Integration of Semantic Alignment Screening

• Improvement: Introducing a conservative, LLM-assisted check that compares the semantic intent of the rewritten natural language problem against its formal Lean representation before proof generation.

• Mechanism: The system must query a specialized checker (e.g., Qwen3-Max at T=0) three times per compiled statement, enforcing an all-pass policy. This prevents semantic drift, ensuring the formalized structure matches the intended problem constraints (e.g., preserving unit consistency or logical connectives).

3. Enforced Target-Answer Alignment

• Improvement: Moving beyond simply checking if a reference answer is correct; the system must verify that the extracted answer precisely matches the specific quantity requested in the problem, regardless of whether an intermediate step is required.

• Mechanism: A strict, read-only Literal Answer Extraction step pulls only verbatim spans from the verified Lean proof. This candidate is then validated against a final Target-Answer Matching check, ensuring that intermediate values or answers to different quantities are rejected.

4. Development of Reliability Metrics for Benchmark Selection

• Improvement: Establishing quantifiable metrics (Well-definedness, Feasibility, Answer Correctness) to objectively assess the quality of generated data and provide a reliable measure of benchmark reliability.

• Mechanism: The system must track the ratio (Nc/N) for each criterion across all generated candidates, allowing for the automated rejection of low-quality instances without human intervention.

An AI system incorporating these methodologies will achieve the following capabilities:

1. Reliable Training Data Generation (Benchmark Creation)

• Capability: The system can automatically generate a massive set of training data where every single problem is guaranteed to be mathematically sound and have a verifiable correct answer, eliminating the need for human-assisted auditing of validity.

• Contrast: Current LLM-based generators often produce hallucinated or contradictory problems that are difficult to filter.

2. Robust Evaluation of Model Reasoning (Contamination Detection)

• Capability: The system can perform a rigorous analysis of model performance change (Accuracy) when applied to a rewritten, but mathematically equivalent, version of an original benchmark problem. This allows the system to distinguish genuine mathematical reasoning from superficial memorization or pattern reliance.

• Specific Action: It identifies models that fail on structurally similar problems (indicating reliance on surface cues) versus those that perform consistently across all types of valid rewrites.

3. Enhanced Self-Correction and Verification

• Capability: When an LLM generates a solution, the system can force it to generate not just the answer, but a formalized proof script. The system then uses Lean's kernel-level verification to confirm if the generated answer is logically supported by its own formal proof.

• Specific Action: This transforms error detection from does this look right? (heuristic) to is this provably correct? (deterministic), providing a powerful mechanism for training LLMs to verify their own claims.

4. Precise Diagnostics of Model Weaknesses

• Capability: By analyzing the relationship between various confounding factors (e.g., solution complexity, proof length, numerical range change) and the resulting accuracy drop, the system provides targeted insights into why a model failed—whether due to poor reasoning, surface-level sensitivity, or inability to handle complex formal proofs.