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

RePro：用于大语言模型数学解题可靠评估的证明验证基准重写框架

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.

摘要： 数据污染损害了大语言模型（LLM）在数学解题能力评估上的可靠性。虽然基于重写的评估方法可以缓解模型对题目的记忆效应，但现有方法缺乏对题目有效性和答案正确性的保证。

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.

我们提出了“证明验证基准重写”（RePro）框架。这是首个将面向 Lean 的神经自动定理证明器（ATP）集成到基准重写中的框架，它通过 Lean 验证的证明来确保重写后的题目和重新生成的答案的正确性。

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.

在 GSM8K 和 MATH 数据集上的实验表明，RePro 保留的重写实例在定义明确性、可行性和答案正确性方面均达到了 100%，而现有方法仍会产生无效或错误的实例。

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 this https URL.

此外，多个模型在经过证明验证的重写基准测试中表现出准确率下降，这表明它们的性能对题目表层和结构上的变化非常敏感，且部分性能表现可能源于对题目的记忆效应。我们的源代码和数据已在链接中提供。