RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
Authors: Xiyuan Zhou, Zhuoqi Li, Xinlei Wang, Yirui He, Yuhao Wu, Yuheng Cheng, Yan Xu, Junhua Zhao, +1 more
Organizations: Nanyang Technological University · The Chinese University of Hong Kong, Shenzhen · INSAIT, Sofia University “St. Kliment Ohridski” · Shenzhen Loop Area Institute · AIRS
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.
Figures & tables
Figure 1: Overview of RePro. Existing rewriting methods may produce invalid problems or incorrect answers. RePro integrates formal verification to ensure that rewritten instances are valid questions and paired with verified answers, enabling reliable LLM evaluation.
Figure 2: Framework of the proposed verification pipeline for rewriting-based evaluation. The pipeline progressively filters rewritten instances to obtain valid questions with verified answers.
Figure 3: Failure modes of rewriting-based evaluation and our solution. Rewriting may introduce three types of reliability issues: (1) ill-defined problems caused by ambiguous or missing information, (2) infeasible problems due to conflicting constraints, and (3) incorrect answers where the reference answer is wrong. A rewritten instance is valid only if the problem is well-defined, feasible, and paired with a correct reference answer.
Full Dataset
Method
GSM8K
MATH
Well-defined ↑
Feasible ↑
Correct ↑
Gen. Rate ↑
Well-defined ↑
Feasible ↑
Correct ↑
Gen. Rate ↑
Auto-Dataset
99.60
99.19
87.10
100.00
98.43
96.23
79.99
100.00
ITD
100.00
99.19
89.11
100.00
98.26
97.85
81.15
100.00
VarBench
97.98
96.76
95.14
99.60
96.54
93.58
87.36
58.76
RePro (Ours)
100.00
100.00
100.00
88.31
100.00
100.00
100.00
59.16
Table 1: Comparison of rewriting quality across methods on GSM8K and MATH. Metrics include well-definedness (Well-defined), feasibility (Feasible), answer correctness (Correct), and generation rate (Gen. Rate). The upper table reports results on the full set of generated rewritten instances, while the lower table reports results on the subset of benchmark instances for which RePro successfully generates rewritten problems.
Figure 4: Impact of ATPs with varying capabilities on generation success rates.
Figure 6
Figure 7: Rewriting quality comparison across five difficulty levels (LV1–LV5) of the MATH dataset. (a) Proportion of well-defined problems, (b) proportion of feasible problems, and (c) proportion of correct reference answers.
Figure 8: Impact of problem rewriting on model performance across five difficulty levels. (a) Original accuracy. (b) Accuracy after rewriting. (c) Absolute accuracy change (percentage points). (d) Relative accuracy change (percentage). Positive values indicate improvements, while negative values indicate performance drops.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Model
FIMO
DeepSeek-ProverBench
DeepSeek-Prover-V2-7B
5.70
0.31
Kimina-Prover-7B
3.35
1.38
Goedel-Prover-V2-8B
7.05
1.53
Appendix
Table 2: Pass@32 success rates of recent Lean-oriented prover models on high-difficulty formal proof generation benchmarks. The low scores indicate a substantial ATP bottleneck for harder olympiad-style benchmarks.
Figure 9: Data distribution before and after RePro filtering.
Method
Dataset
#Checked
Well-defined Agreement
Feasibility Agreement
Correctness Agreement
Auto-Dataset
GSM8K
100
100.00
100.00
100.00
Auto-Dataset
MATH
500
100.00
100.00
100.00
ITD
GSM8K
100
100.00
100.00
100.00
ITD
MATH
500
100.00
100.00
100.00
VarBench
GSM8K
100
100.00
100.00
100.00
VarBench
MATH
500
100.00
100.00
100.00
Appendix
Table 3: Human-machine agreement in the independent validation. For each rewriting method, we randomly sample 600 instances, including 100 from GSM8K and 100 from each MATH difficulty level. Human auditors independently judge well-definedness, feasibility, and answer correctness without using automatic pipeline decisions, Lean formalizations, ATP outputs, or verified proofs. The table reports the percentage of sampled instances for which human judgments agree with the automatic pipeline judgments for each criterion.
Confound metric
Spearman ρ with accuracy drop
Problem length change
-0.000
Absolute problem length change
-0.031
Surface-form distance
-0.031
Numeric-range change
0.014
Absolute numeric-range change
0.002
Numeric-count change
-0.021
Appendix
Table 4: Spearman correlations between potential confound metrics and model-averaged accuracy drop on the RePro-retained MATH evaluation set. Surface-level and numeric changes have near-zero correlations with accuracy drop, while solution and proof complexity show weak positive correlations.
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6