RePro

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

Xiyuan Zhou^1,, Zhuoqi Li^2,, Xinlei Wang³, Yirui He^2,4, Yuhao Wu², Yuheng Cheng²,
Yan Xu^1,†, Junhua Zhao^2,5,†, Jinjin Gu^3,†

¹Nanyang Technological University    ²The Chinese University of Hong Kong, Shenzhen
³INSAIT, Sofia University "St. Kliment Ohridski"    ⁴Shenzhen Loop Area Institute    ⁵AIRS

^*Equal contribution    ^†Corresponding authors

         

Overview  |  Method  |  Released Data  |  Quick Start  |  Citation

Important

🎉 RePro has been accepted to the Main Conference of EMNLP 2026.

Overview

Data contamination can make mathematical reasoning benchmarks unreliable: a model may reproduce memorized answers instead of demonstrating genuine reasoning. Rewriting benchmark problems helps reduce surface-level overlap, but existing approaches may introduce ill-defined questions, infeasible constraints, or incorrect reference answers.

RePro is a proof-verified benchmark rewriting framework that combines large language models (LLMs), neural automated theorem provers (ATPs), and the Lean proof assistant. A rewritten instance is released only when it is:

• Well-defined - the question is unambiguous and has a valid target.
• Feasible - its constraints admit a meaningful solution.
• Correct - its reference answer is backed by a Lean-verified proof.

Experiments on GSM8K and MATH show that RePro produces rewritten benchmarks with formally verified reference answers while exposing model sensitivity to surface and structural variations.

Method

RePro uses a progressive three-stage verification pipeline:

1. Feasibility screening filters ill-defined or infeasible rewritten questions.
2. Executable formalization translates each candidate into Lean and checks compilation and semantic consistency.
3. Proof-level verification uses a neural ATP to search for a proof, which is accepted only after Lean kernel verification.

Only candidates that complete the full path are retained.

Released Data

The repository includes proof-verified rewritten instances for two mathematical reasoning benchmarks:

File	Benchmark	Split	Instances
gsm8k.csv	GSM8K	Released subset	219
1.csv	MATH	Level 1	201
2.csv	MATH	Level 2	213
3.csv	MATH	Level 3	278
4.csv	MATH	Level 4	201
5.csv	MATH	Level 5	201

Each CSV contains the following fields:

Field	Description
original_question	Original benchmark problem
original_answer	Original benchmark solution or answer
rewritten_question	RePro-generated problem
new_answer	Answer extracted from the verified proof
lean_proof	Lean proof artifact used for verification

Repository Structure

RePro-E24F/
├── RePro.py                     # End-to-end rewriting and verification pipeline
├── gsm8k.csv                    # Rewritten GSM8K instances
├── 1.csv ... 5.csv              # Rewritten MATH instances by difficulty level
├── assets/
│   └── affiliations/            # Institution logos used by this README
└── README.md

The main pipeline implements question rewriting, feasibility screening, Lean formalization, compilation checking, semantic consistency checking, ATP proof generation, Lean proof verification, and answer extraction.

Quick Start

1. Install dependencies

Create and activate a Python environment, then install the packages imported by RePro.py:

python -m venv .venv
source .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install datasets lean-interact openai pandas requests

The pipeline creates a temporary Lean v4.22.0 project with mathlib through lean-interact. Make sure the local environment can install and run the required Lean toolchain.

2. Configure services

RePro uses an OpenAI-compatible LLM endpoint and a formalization/proving backend:

export OPENAI_API_KEY="your_api_key"
export OPENAI_BASE_URL="https://your-openai-compatible-endpoint/v1"
export BACKEND_API_URL="https://your-formalization-and-proving-backend"

3. Run the pipeline

python RePro.py

The current entry point selects one unprocessed Level-1 Algebra problem from the MATH training split per invocation and writes the result to RePro_output.csv. Modify the dataset filter and sample count in main() when running larger experiments.

Output

For every selected problem, the pipeline records:

• the original problem and answer;
• the rewritten problem;
• the answer extracted from the verified Lean proof; and
• the full Lean proof artifact.

If a candidate does not pass every verification stage within the configured retry limits, it is recorded as unsuccessful rather than included as a verified rewrite.

Citation

If you find RePro useful, please cite:

@inproceedings{zhou2026repro,
  title     = {{RePro}: Proof-Verified Benchmark Rewriting for Reliable Evaluation of {LLM} Mathematical Problem Solving},
  author    = {Zhou, Xiyuan and Li, Zhuoqi and Wang, Xinlei and He, Yirui and Wu, Yuhao and Cheng, Yuheng and Xu, Yan and Zhao, Junhua and Gu, Jinjin},
  booktitle = {Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing},
  year      = {2026}
}