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

arXiv: https://arxiv.org/abs/2609.00062 · HTML: https://mlsanity.com/paper/2609.00062/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 42 references that are in the map.
- First posted on arXiv 30 Aug 2026.

## Builds on (most cited first, 15 of 15)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [Humanity's Last Exam](https://mlsanity.com/paper/2501.14249/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Benchmark Self-Evolving: A Multi-Agent Framework for Dynamic LLM Evaluation](https://mlsanity.com/paper/2402.11443/) (2024)
- [VarBench: Robust Language Model Benchmarking Through Dynamic Variable Perturbation](https://mlsanity.com/paper/2406.17681/) (2024)
- [Inference-Time Decontamination: Reusing Leaked Benchmarks for Large Language Model Evaluation](https://mlsanity.com/paper/2406.13990/) (2024)
- [StructEval: Deepen and Broaden Large Language Model Assessment via Structured Evaluation](https://mlsanity.com/paper/2408.03281/) (2024)
- [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025)
- [EngiAgent: Fully Connected Coordination of LLM Agents for Solving Open-ended Engineering Problems with Feasible Solutions](https://mlsanity.com/paper/2605.02289/) (2026)

## Abstract (arXiv)

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.