aiqbench analysis
This research introduces RePro, a novel framework that integrates automated theorem provers into benchmark rewriting to ensure 100% validity and correctness in LLM mathematical evaluation. By eliminating data contamination risks inherent in previous methods, the study reveals that current model performance metrics may be inflated by memorization rather than genuine reasoning capabilities. The availability of proof-verified datasets offers a robust standard for future reliability testing in arithmetic problem solving.
RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
arXiv:2609.00062v1 Announce Type: cross 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. 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.
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. 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 this https URL.
Computation and Language (cs.CL); Artificial Intelligence (cs.AI)
arXiv:2609.00062 [cs.CL]
(or arXiv:2609.00062v1 [cs.CL] for this version)
https://doi.org/10.48550/arXiv.2609.00062 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 223 words
Related coverage

[AINews] Meta Muse Wonder & Wonder Full: MSL’s Claude 5.5-tier Frontier Model
Latent Space · Oct 13, 2026

[AINews] not much happened today
Latent Space · Sep 18, 2026

[AINews] not much happened today
Latent Space · Sep 10, 2026

Projection sampling preserves capabilities but diminishes gains from alignment fine-tuning
LessWrong · Oct 16, 2026