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

# RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
Source: [https://arxiv.org/html/2609.00062](https://arxiv.org/html/2609.00062)
Xiyuan Zhou††thanks:Equal contribution\.Zhuoqi Li11footnotemark:1Affiliation:The Chinese University of Hong Kong, ShenzhenEmail:[zhuoqili1@link\.cuhk\.edu\.cn](mailto:)Xinlei WangAffiliation:INSAIT, Sofia University “St\. Kliment Ohridski”Email:[xinlei\.wang@insait\.ai](mailto:)Yirui HeAffiliation:The Chinese University of Hong Kong, ShenzhenAffiliation:Shenzhen Loop Area InstituteEmail:[yiruihe@link\.cuhk\.edu\.cn](mailto:)Yuhao WuAffiliation:The Chinese University of Hong Kong, ShenzhenEmail:[yuhaowu@link\.cuhk\.edu\.cn](mailto:)Yuheng ChengAffiliation:The Chinese University of Hong Kong, ShenzhenEmail:[yuhengcheng@link\.cuhk\.edu\.cn](mailto:)Yan Xu††thanks:Corresponding authors\.Affiliation:Nanyang Technological UniversityEmail:[xuyan@ntu\.edu\.sg](mailto:)Junhua Zhao22footnotemark:2Affiliation:The Chinese University of Hong Kong, ShenzhenAffiliation:AIRSEmail:[zhaojunhua@cuhk\.edu\.cn](mailto:)Jinjin Gu22footnotemark:2Affiliation:INSAIT, Sofia University “St\. Kliment Ohridski”Email:[jinjin\.gu@insait\.ai](mailto:)

###### 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](https://github.com/AI4Engi/RePro)\.

## 1Introduction

Evaluating mathematical capability is essential for understanding the reasoning abilities of large language models \(LLMs\)[Shao et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib17);[Ahn et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib18)\. However, benchmark reliability is challenged by data contamination, as training corpora and evaluation benchmarks often share public sources[Chen et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib2);[Cheng et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib1)\. Such overlap may allow models to achieve high scores through memorization rather than genuine reasoning[Li et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib3);[Zhou et al\. \(2026a\)](https://arxiv.org/html/2609.00062#bib.bib5);[Zhao et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib4)\. Recent dynamic evaluation methods, including benchmark rewriting, interactive evaluation, and multi\-agent evaluation, aim to reduce contamination[Chen et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib2)\. However, their reliance on heuristic rewriting or model\-generated processes makes it difficult to guarantee problem validity and answer correctness\.

![Refer to caption](https://arxiv.org/html/2609.00062v1/intro_figure_v3.png)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\.Benchmark reliability remains a concern in existing evaluations, even for influential expert benchmarks such as GPQA[Rein et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib20)and HLE[Center for AI Safety et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib21), which have advanced frontier LLM evaluation\. HLE\-Verified further highlights the importance of answer reliability, reporting that within HLE’s mathematical category, problem validity exceeds 92% while answer validity is 59\.6%[Zhai et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib22)\. This suggests that benchmark reliability depends on both problem validity and answer correctness, reflecting a broader emphasis on verifier\-guided reliability in LLM systems[Wang et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib41)\. Accordingly, RePro focuses on mathematical and formally verifiable problems, and evaluates rewritten instances by whether they are well\-defined, feasible, and paired with a correct reference answer \(see Sec\.[4](https://arxiv.org/html/2609.00062#S4)\)\.

To improve benchmark rewriting reliability, we introduce deterministic proof verification by incorporating Lean\-oriented neural automated theorem provers \(ATPs\) and proof\-assistant checking into the rewriting pipeline, replacing heuristic LLM\-based evaluation with machine\-verifiable reasoning\. In RePro, proof search relies on Lean\-oriented neural ATPs such as Goedel\-Prover[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27)and DeepSeek\-Prover[Ren et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib23)\. Given a formalized statement, these models generate Lean proof scripts, which are treated as candidate proofs and accepted only after Lean kernel\-level verification\. Unlike classical ATPs and SMT solvers such as Vampire[Kovács and Voronkov \(2013\)](https://arxiv.org/html/2609.00062#bib.bib31)and Z3[De Moura and Bjørner \(2008\)](https://arxiv.org/html/2609.00062#bib.bib30), which return sound results within supported logical fragments, neural ATPs may generate scripts with compilation failures, target mismatches, or tactic\-level errors\. RePro therefore retains only proofs that pass Lean kernel\-level checking[De Moura et al\. \(2015\)](https://arxiv.org/html/2609.00062#bib.bib24)\.

Building on the guarantees provided by formally verified proofs, we propose RePro \(Proof\-Verified Benchmark Rewriting\), a framework for constructing mathematically rigorous rewritten benchmarks\. As illustrated in Fig\.[1](https://arxiv.org/html/2609.00062#S1.F1), in RePro, LLMs generate diverse rewritten problems and perform conservative semantic screening, while ATPs search for candidate proofs and proof assistants verify them\. In this way, the rewritten benchmark maintains high diversity while providing verifiable correctness guarantees\. Only instances whose reference answers have a formally verified proof are retained, ensuring that the released benchmarks contain only problems with formally verified answers\. Detailed methodology is presented in Sec\.[3](https://arxiv.org/html/2609.00062#S3)\.

Empirical results show that RePro significantly improves the reliability of rewriting\-based evaluation\. Compared with existing methods, RePro achieves 100% well\-definedness, feasibility, and answer correctness among retained rewritten instances on both GSM8K[Cobbe et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib7)and MATH[Hendrycks et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib6), while prior methods still produce invalid problems or incorrect reference answers\.

Our contributions can be summarized as follows: \(1\) We propose RePro, the first benchmark rewriting framework that integrates ATPs and Lean into a unified verification pipeline, retaining only instances with verified reference answers while enforcing problem validity through a three\-stage verification process\. \(2\) We introduce reliability\-oriented evaluation criteria for rewritten benchmarks, covering well\-definedness, feasibility, and answer correctness\. \(3\) We use proof\-verified rewriting to analyze reformulation sensitivity and identify potential memorization\-related signals\.

![Refer to caption](https://arxiv.org/html/2609.00062v1/framework_v3.png)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\.
## 2Related Work

Dynamic Benchmark Generation\.Dynamic benchmark methods mitigate data contamination and expand evaluation coverage by automatically generating new test instances from existing benchmarks\. A common approach is benchmark rewriting, which applies semantic or structural transformations, such as synonym paraphrasing[Ying et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib13);[Zhu et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib16), numerical substitution[Qian et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib12), and structural perturbation[Cao et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib15), to weaken memorization cues while reusing existing evaluation resources\. Another line of work adopts multi\-agent or solver\-based frameworks for benchmark construction, such as Benchmark Self\-Evolving[Wang et al\. \(2025b\)](https://arxiv.org/html/2609.00062#bib.bib19), BenchAgents[Butt et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib14), and the CSP\-based logic puzzle benchmark ZebraLogic[Lin et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib32)\. Despite improving diversity and coverage, these methods still largely rely on heuristic validation, including human inspection, LLM\-as\-a\-Judge, or agent\-based checking\. Such validation may still leave semantic drift, incorrect labels, or implicit\-assumption violations, limiting deterministic reliability guarantees, see Sec\.[4](https://arxiv.org/html/2609.00062#S4)and Sec\.[6\.1](https://arxiv.org/html/2609.00062#S6.SS1)\.

Formal Verification and Automated Theorem Proving\.Formal reasoning represents mathematical statements and proofs in a machine\-verifiable format, enabling rigorous verification of logical correctness\. Proof assistants such as Lean[De Moura et al\. \(2015\)](https://arxiv.org/html/2609.00062#bib.bib24)and Coq[Bertot and Castéran \(2013\)](https://arxiv.org/html/2609.00062#bib.bib25)provide formal languages for mathematical reasoning and verify proofs through kernel\-level checking\. Large formal mathematical libraries such as mathlib support large\-scale formalization and automated reasoning[Yang et al\. \(2023\)](https://arxiv.org/html/2609.00062#bib.bib28)\. Classical ATPs and SMT solvers, such as Vampire[Kovács and Voronkov \(2013\)](https://arxiv.org/html/2609.00062#bib.bib31)and Z3[De Moura and Bjørner \(2008\)](https://arxiv.org/html/2609.00062#bib.bib30), solve formal logical problems within supported logics, while hammer systems such as LeanHammer bridge Lean with external provers[Zhu et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib33)\. In contrast, recent neural Lean provers, including DeepSeek\-Prover[Ren et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib23)and Goedel\-Prover[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27), generate candidate Lean proof scripts that must be checked by Lean before acceptance\. RePro operates in this Lean/mathlib setting and uses neural Lean provers with kernel\-level verification to ensure answer correctness\. While prior work mainly studies theorem proving itself, benchmark verification remains underexplored\.

## 3RePro

### 3\.1Overview

To construct rewritten benchmarks with formally verified reference answers, we propose RePro\. Existing rewriting\-based approaches typically rely on heuristic validation mechanisms, such as LLM\-as\-a\-Judge or rule\-based checking, which cannot provide deterministic guarantees on problem validity or answer correctness\. To address this limitation, RePro integrates ATPs into the benchmark rewriting process, enabling the verification of reference answers through formal proofs while preserving the diversity of rewritten instances\.

RePro follows a progressive verification paradigm\. It first prompts an LLM to generate candidate rewrites through numerical reparameterization, logical restructuring, constraint modification, and contextual reconstruction, and filters out instances that fail basic problem\-validity checks, such as those with ambiguous statements, missing constraints, or infeasible solutions\. The remaining candidates are then translated into executable formal specifications in Lean, providing precise and machine\-checkable representations of the rewritten problems\. Finally, an automated theorem prover \(ATP\) performs proof search to generate candidate proofs, whose correctness is checked by the Lean proof assistant\. Through this staged process, RePro retains only rewritten instances that are well\-defined and feasible and whose answers are supported by formally verified proofs\. The prompt templates and implementation details are provided in Appendix[B](https://arxiv.org/html/2609.00062#A2), and examples of RePro\-generated rewritten instances are provided in Appendix[G](https://arxiv.org/html/2609.00062#A7)\.

### 3\.2Feasibility Screening

Feasibility Screening begins with LLM\-based rewriting and subsequently filters invalid candidate rewrites before executable formalization and proof verification\. Given an original problem, the LLM generates a candidate rewrite while preserving its core mathematical structure, solution logic, difficulty, and answer type\. The rewriting process applies strategies including numerical reparameterization, logical restructuring, constraint modification, and contextual reconstruction for word problems\. The rewriter is instructed not to solve the rewritten problem or generate its new answer\.

The generated candidate is then screened for problem validity\. This step removes questions that are ill\-defined, ambiguous, internally inconsistent, contradictory, unrealistic, or infeasible under basic real\-world or task\-specific constraints\. Here, feasibility refers to the semantic and constraint consistency of the rewritten problem, rather than merely whether a target can be formally derived from its premises\. Accordingly, candidates with contradictory premises are rejected regardless of whether the target is formally derivable from them\. Detailed rewriting prompts, screening criteria, and implementation details are provided in Appendix[B](https://arxiv.org/html/2609.00062#A2)\.

For example, in problems involving population counts or quantity constraints, automatic rewriting may introduce negative values or other conditions that violate implicit real\-world assumptions[Zhou et al\. \(2026b\)](https://arxiv.org/html/2609.00062#bib.bib42)\. Although such outputs may appear mathematically expressible, they are considered infeasible under the intended problem semantics and are therefore removed\. This stage is intended to ensure problem validity rather than answer correctness\. Answer correctness is established later through Proof\-level Verification, while the final answer\-target matching step provides an additional target\-level consistency check by ensuring that the verified answer corresponds to the specific quantity requested in the rewritten problem\.

### 3\.3Executable Formalization

Executable Formalization converts rewritten instances that pass feasibility screening into machine\-verifiable formal statements in Lean\. This stage consists of a format check and a semantic check\. The format check ensures that the generated Lean code is syntactically valid and can be compiled in Lean\. The semantic check performs an LLM\-assisted conservative alignment screen between the rewritten natural\-language problem and the Lean formal statement, comparing key elements such as quantities, conditions, logical structure, object type, and the requested target\.

We adopt a conservative all\-pass policy\. For each compiled formalization, the semantic checker is queried three times with temperature zero\. A candidate is accepted only when all three judgments return Consistent\. Any mismatch, parsing failure, or uncertain output causes the candidate to be discarded and regenerated\.

This step should not be interpreted as formal verification of natural\-language\-to\-Lean equivalence\. It serves only as a pre\-proof filter\. RePro mitigates this limitation through subsequent proof\-level verification and final\-answer alignment: the ATP\-generated proof must pass Lean checking, and the extracted answer must match the target quantity requested by the rewritten problem\. Therefore, answer correctness is established only after Lean verification and answer alignment, while semantic consistency is conservatively screened rather than formally guaranteed\. More details on the semantic screening policy and proof\-grounded target\-answer matching are provided in Appendices[C](https://arxiv.org/html/2609.00062#A3)and[D](https://arxiv.org/html/2609.00062#A4)\.

### 3\.4Proof\-level Verification

Proof\-level Verification validates the correctness of reference answers through formal proof verification\. This stage takes executable formalizations as input and retains only instances whose answers can be successfully proven and verified in Lean, forming the final evaluation dataset\. Unlike earlier stages, Proof\-level Verification is the only stage that determines answer correctness\.

At this stage, ATP is used to construct candidate proofs for the formalized problems, which are then verified in Lean\. Only instances whose answers can be verified by a valid proof are retained, while those that fail proof verification are discarded and regenerated\. All correctness guarantees for reference answers originate from this stage\.

As illustrated in Fig\.[2](https://arxiv.org/html/2609.00062#S1.F2), Operation 8 performs a constrained answer\-alignment step between the rewritten problem and the valid proof\. It extracts a candidate answer from spans that already appear in the proof and checks whether it matches the quantity requested in the problem\. No additional computation, normalization, simplification, or inference is allowed at this stage\. Only answers that exactly match the requested quantity are accepted; intermediate values, answers to a different target, and unresolved cases are discarded\. This step is used solely to ensure target\-answer consistency\. Detailed descriptions are provided in Appendix[D](https://arxiv.org/html/2609.00062#A4)\.

## 4Evaluation Criteria

![Refer to caption](https://arxiv.org/html/2609.00062v1/failure_mode_v5.png)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\.A benchmark problem can serve as a reliable evaluation instance only if the problem itself is valid and its reference answer is correct\. The former requires the problem to be clearly specified, logically coherent, and solvable, while the latter ensures that model outputs are compared against a correct ground\-truth answer\. This is especially important for rewritten problems, where rewriting may alter not only surface wording but also problem semantics, constraints, or answer consistency\. Recent benchmark verification studies further show that many evaluation failures arise from ambiguous statements, missing information, or incorrect reference answers\.

Motivated by these observations, we evaluate rewritten problems from two complementary perspectives:problem validityandanswer correctness\. Problem validity includes two criteria:well\-definedness, requiring the problem to be clear and complete, andfeasibility, requiring it to admit a solution under the given conditions and satisfy basic real\-world or task\-specific constraints\. Answer correctness requires that the reference answer be correct\. Together, these define three criteria for a reliable benchmark instance: well\-definedness, feasibility, and answer correctness\. Fig\.[3](https://arxiv.org/html/2609.00062#S4.F3)illustrates the corresponding failure modes and a valid rewritten instance\. We therefore use three criteria:

Well\-definedness\.Measures whether the problem statement provides sufficient and unambiguous information to determine the task and its objective\. A problem is considered not well\-defined if it contains missing conditions, semantic ambiguity, unclear objects or variables, incomplete constraints, or an unspecified solving target\.

Feasibility\.Measures whether a well\-defined problem admits a valid solution under basic real\-world or task\-specific constraints\. A problem is considered infeasible if no valid solution exists or if the derived result violates these constraints due to conflicting conditions or inconsistencies\.

Answer Correctness\.Measures whether the reference answer is formally verified\. A reference answer is correct only if the candidate is successfully formalized, verified by a valid proof, and matched to the target quantity\. In RePro, all retained candidates satisfy this requirement\. In more general settings, candidates that fail automatic formalization should receive human\-assisted checking to avoid hallucinated or unverifiable instances\.

LetNNdenote the total number of generated rewritten instances, andNcN\_\{c\}the number of instances satisfying criterionc∈\{well\-definedness,feasibility,answer correctness\}c\\in\\\{\\text\{well\-definedness\},\\text\{feasibility\},\\text\{answer correctness\}\\\}\. The corresponding rate is computed asNc/NN\_\{c\}/N\. To assess these criteria, we use a verification pipeline based on Lean, ATP, and LLM screening, with human assistance for ambiguous cases\.

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\.Full DatasetMethodGSM8KMATHWell\-defined↑\\uparrowFeasible↑\\uparrowCorrect↑\\uparrowGen\. Rate↑\\uparrowWell\-defined↑\\uparrowFeasible↑\\uparrowCorrect↑\\uparrowGen\. Rate↑\\uparrowAuto\-Dataset99\.6099\.1987\.10100\.0098\.4396\.2379\.99100\.00ITD100\.0099\.1989\.11100\.0098\.2697\.8581\.15100\.00VarBench97\.9896\.7695\.1499\.6096\.5493\.5887\.3658\.76RePro \(Ours\)100\.00100\.00100\.0088\.31100\.00100\.00100\.0059\.16
RePro Successful Generation Subset

MethodGSM8KMATHWell\-defined↑\\uparrowFeasible↑\\uparrowCorrect↑\\uparrowGen\. Rate↑\\uparrowWell\-defined↑\\uparrowFeasible↑\\uparrowCorrect↑\\uparrowGen\. Rate↑\\uparrowAuto\-Dataset98\.3997\.1880\.65100\.0099\.5399\.5386\.88100\.00ITD97\.5896\.7781\.05100\.00100\.0099\.0787\.66100\.00VarBench98\.7998\.3996\.77100\.0095\.4993\.7389\.2360\.53RePro \(Ours\)100\.00100\.00100\.00100\.00100\.00100\.00100\.00100\.00

## 5Experimental Methodology

### 5\.1Datasets

To evaluate RePro, we select GSM8K[Cobbe et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib7)and MATH[Hendrycks et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib6)as benchmarks\. We also considered harder benchmarks such as AIME[Dekoninck et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib35)and Omni\-MATH[Gao et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib36), but current ATP bottlenecks led to very low generation rates; details are provided in Sec\.[6\.2](https://arxiv.org/html/2609.00062#S6.SS2)and Appendix[E](https://arxiv.org/html/2609.00062#A5)\. Therefore, we focus on GSM8K and MATH, which are widely used for mathematical reasoning\. GSM8K provides structured grade\-school math problems, while MATH covers five Art of Problem Solving \(AoPS\) difficulty levels \(LV1–LV5\), ranging from basic high\-school exercises to olympiad\-level problems\. Additional details on dataset selection and the data distribution before and after RePro filtering are provided in Appendix[E](https://arxiv.org/html/2609.00062#A5)\. The metadata and fields of the released RePro dataset are described in Appendix[F](https://arxiv.org/html/2609.00062#A6)\.

### 5\.2Models

We evaluate RePro on a diverse set of open\-source language models from several major model families\. Specifically, we include Qwen2–0\.5B/1\.5B, Qwen3–0\.6B/1\.7B/8B/14B[Yang et al\. \(2025a\)](https://arxiv.org/html/2609.00062#bib.bib8), Llama\-3\.2–1B/3B[Touvron et al\. \(2023\)](https://arxiv.org/html/2609.00062#bib.bib9), DeepSeek\-R1–1\.5B/7B/14B[Guo et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib10), and Gemma 3–1B/4B[Team et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib11)\. This selection allows us to compare contamination\-related behaviors across different architectures and training methods while keeping model scale controlled\.

For the RePro generation pipeline, we use Qwen3\-MAX[Yang et al\. \(2025a\)](https://arxiv.org/html/2609.00062#bib.bib8)for problem rewriting and feasibility screening, Goedel\-Formalizer\-V2\-8B for executable formalization into Lean 4 statements, and Goedel\-Prover\-V2\-8B for ATP\-based proof generation[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27)\. The generated proofs are then verified by Lean 4\.

### 5\.3Baselines

We compare our method with several representative approaches for automatic benchmark rewriting, including Auto\-Dataset[Ying et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib13), ITD[Zhu et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib16), and VarBench[Qian et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib12)\. These methods generate new evaluation instances to mitigate benchmark leakage while preserving the original task structure\. Auto\-Dataset generates semantically similar questions from existing problems\. ITD performs semantic\-level rewriting while preserving the underlying numerical relations and computation logic\. VarBench extracts numerical variables and constructs parameterized problem templates with executable solution functions, enabling new instances through variable resampling\.

## 6Results

### 6\.1Rewriting Quality Comparison

Figure 4:Impact of ATPs with varying capabilities on generation success rates\.Figure 5:Effect of rewriter on generation rate\.Figure 6:Effect of ATP call limit on generation rate\.
From Table[1](https://arxiv.org/html/2609.00062#S4.T1), we obtain three key findings\.

RePro guarantees reliable retained instances\.On both GSM8K and MATH, RePro achieves 100% well\-definedness, feasibility, and answer correctness\. This shows that its verification pipeline removes ill\-defined problems, infeasible instances, and incorrect reference answers from the retained rewritten set\.

Existing rewriting methods still produce invalid or incorrect instances\.On the full datasets, AutoDataset, ITD, and VarBench achieve correctness rates of 79\.99%, 81\.15%, and 87\.36% on MATH, and 87\.10%, 89\.11%, and 95\.14% on GSM8K\. Their feasibility rates also remain below 100% on both datasets\. These results show that existing methods can introduce incorrect references or invalid problems, undermining evaluation reliability\. Representative candidate\-level failure modes observed in our VarBench implementation are further analyzed in Appendix[K](https://arxiv.org/html/2609.00062#A11)\.

RePro’s gains are not due to subset selection alone\.On the RePro\-success subset, baselines still show non\-trivial invalidity and incorrectness\. Their correctness rates are 80\.65%, 81\.05%, and 96\.77% on GSM8K, and 86\.88%, 87\.66%, and 89\.23% on MATH, respectively\. In contrast, RePro remains at 100% across all criteria, indicating that the gains mainly come from its verification mechanism rather than subset selection\.

As a supplementary reliability check, we independently audit 2,400 sampled rewritten instances across RePro and all baselines\. Human judgments fully agree with the automatic reliability results\. Details are provided in Appendix[H](https://arxiv.org/html/2609.00062#A8)\.

### 6\.2Generation Rate Analysis

We analyze three key factors that affect RePro’s generation rate: ATP capability, rewriter capability, and the ATP call limit\. Overall, stronger ATPs and rewriters improve generation coverage, while increasing the ATP call limit brings additional but diminishing gains\.

#### 6\.2\.1Effect of ATP Capability

RePro relies on ATPs to generate proofs for formalized problems, so ATP capability directly affects generation success\. To study this effect, we keep all other components unchanged and only replace the ATP\. We evaluate three strong ATPs below 15B parameters: DeepSeek\-Prover\-V2\-7B \(non\-CoT\)[Ren et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib23), Kimina\-Prover\-Preview\-Distill\-7B[Wang et al\. \(2025a\)](https://arxiv.org/html/2609.00062#bib.bib26), and Goedel\-Prover\-V2\-8B[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27), denoted as DeepSeek\-Prover, Kimina\-Prover, and Goedel\-Prover, respectively\. On miniF2F[Zheng et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib29), their pass@32 success rates are 68\.0%, 63\.1%, and 84\.6%, respectively[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27);[Wang et al\. \(2025a\)](https://arxiv.org/html/2609.00062#bib.bib26)\.

Fig\.[4](https://arxiv.org/html/2609.00062#S6.F4)shows that generation success rates generally increase with stronger ATP capability, while decreasing as problem difficulty increases from Level 1 to 5\. We also observe that DeepSeek\-Prover performs worse than expected given its miniF2F performance\. Details are in Appendix[J](https://arxiv.org/html/2609.00062#A10)\.

This result also highlights a quality\-coverage trade\-off\. As shown in Table[1](https://arxiv.org/html/2609.00062#S4.T1), VarBench achieves only 58\.76% generation rate on MATH due to stricter generation constraints\. In contrast, RePro maintains a comparable generation rate of 59\.16% while ensuring both problem validity and answer correctness through formal verification\. Overall, generation success is bounded by current ATP capability, and stronger ATPs are expected to further improve RePro’s coverage\.

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\.![Refer to caption](https://arxiv.org/html/2609.00062v1/four_panel_heatmap_redblue.png)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\.
#### 6\.2\.2Effect of Rewriter Capability

We further analyze the effect of the rewriter model on RePro’s generation success rate\. In this experiment, we keep the formalizer, ATP prover, Lean verification, and answer alignment settings unchanged, and only replace the model used for rewriting and feasibility screening\.

As shown in Fig\.[6](https://arxiv.org/html/2609.00062#S6.F6), the capability of the rewriter model has a clear impact on generation coverage\. Qwen3\-MAX achieves the highest success rate across all datasets and difficulty levels\. For example, on GSM8K, Qwen3\-MAX reaches 88\.31%, compared with 68\.55% for Qwen3\-32B and 58\.87% for Qwen3\-8B\. A similar trend is observed across MATH difficulty levels, suggesting that stronger rewriters are more likely to produce candidates that can be successfully formalized and verified\. Therefore, we use Qwen3\-MAX as the default rewriter in the main experiments to obtain more stable generation coverage\.

#### 6\.2\.3Effect of ATP Call Limit

We further examine how the ATP call limit affects RePro’s generation coverage\. Here, pass@k allows up to k ATP proof\-search attempts for each candidate that has passed rewriting, feasibility screening, and executable formalization\. A sample is counted as successfully generated if at least one proof passes Lean verification and its verified answer matches the target answer\.

As shown in Fig\.[6](https://arxiv.org/html/2609.00062#S6.F6), increasing ATP calls consistently improves generation rate\. On GSM8K, the rate increases from 76\.21% at pass@1 to 83\.87% at pass@2 and 88\.31% at pass@3\. On MATH overall, it increases from 50\.17% to 55\.49% and 59\.16%, respectively\. The same trend holds across all MATH difficulty levels, showing that additional ATP calls can recover part of the failures caused by unsuccessful proof generation\.

The improvement from pass@2 to pass@3 is smaller than that from pass@1 to pass@2, suggesting diminishing returns as the ATP call limit increases\. We therefore use pass@3 as the default setting in the main experiments to balance generation coverage and verification cost\.

### 6\.3Impact of Problem Difficulty on Rewriting Quality

Fig\.[7](https://arxiv.org/html/2609.00062#S6.F7)shows how rewriting quality changes across MATH difficulty levels in terms of well\-definedness, feasibility, and answer correctness\.

Correctness decreases as problem difficulty increases\.As shown in Fig\.[7](https://arxiv.org/html/2609.00062#S6.F7)\(c\), the correctness of ITD and AutoDataset drops noticeably as difficulty increases, from around 90% at Level 1\-2 to about 75%–80% at Level 4\-5\. This indicates that traditional rewriting methods are more likely to introduce incorrect reference answers as reasoning complexity grows\.

Well\-definedness and feasibility remain stable, but invalid instances persist\.As shown in Fig\.[7](https://arxiv.org/html/2609.00062#S6.F7)\(a\)\(b\), the well\-defined and feasible rates of AutoDataset, ITD, and VarBench remain between 89% and 100% across all difficulty levels, without clear degradation as difficulty increases\. However, ill\-defined or infeasible problems still appear at every level, indicating that existing rewriting methods cannot fully eliminate invalid instances\.

### 6\.4Rewriting Sensitivity and Potential Memorization

Fig\.[8](https://arxiv.org/html/2609.00062#S6.F8)compares model accuracy on original MATH problems and their proof\-verified rewritten counterparts\. Since all retained RePro instances pass validity and answer\-correctness verification, this paired comparison reduces the influence of invalid rewrites or incorrect reference answers\. Thus, RePro provides a reliable diagnostic tool for analyzing model sensitivity to benchmark reformulation\.

The results show that many models, especially smaller ones, lose accuracy after rewriting\. For example, Qwen2\-1\.5B drops by 21\.1, 12\.0, and 10\.5 percentage points on Level 1\-3, respectively, while Llama\-3\.2\-3B drops across all levels, with a maximum drop of 15\.1 points\. Meanwhile, some models improve after rewriting, often because rewritten problems clarify conditions, standardize notation, or reduce diagram\-dependent difficulty\. These mixed effects suggest that proof\-verified rewriting reveals model\-specific reformulation sensitivity\. Appendix[I](https://arxiv.org/html/2609.00062#A9)analyzes potential confounds, showing near\-zero correlations between surface or numeric changes and accuracy drop, and only weak positive correlations for solution and proof complexity\.

## 7Conclusion

In this work, we study the reliability of rewriting\-based evaluation for contamination\-resistant LLM benchmarking\. Existing rewriting methods can reduce memorization effects, but often fail to ensure problem validity and answer correctness\. We propose RePro, which integrates ATPs and proof\-assistant checking into the rewriting pipeline\. RePro retains only instances that can be successfully formalized and verified, ensuring problem validity and formally supported reference answers\. Experiments on MATH and GSM8K show that RePro achieves 100% well\-defined, feasible, and correct retained instances, while existing methods still produce invalid problems or incorrect answers\. Further analysis shows that proof\-verified rewriting can reveal model\-specific sensitivity to benchmark reformulation and provide signals of potential memorization or benchmark\-specific pattern reliance\.

## Limitations

While RePro provides the first framework that integrates automated theorem proving into benchmark rewriting and constructs evaluation datasets with proof\-verified reference answers, several limitations remain that we plan to address in future work\.

Dependence on ATP capability\.RePro relies on ATPs to verify candidate solutions during the rewriting\. When the underlying ATP fails to find a valid proof, even correct and solvable problems may be filtered out, which can reduce the overall generation success rate\. This limitation mainly reflects the current capability of neural theorem provers rather than the framework itself\. As stronger ATP models continue to emerge, the generation coverage of RePro is expected to improve\.

Formalization constraints\.RePro requires rewritten problems to be expressible in the Lean formal language in order to perform proof verification\. As a result, the current framework mainly applies to problems that can be rewritten into a Lean representation\. Tasks that rely heavily on natural language semantics or cannot be reasonably formalized in Lean, such as certain text\-based reasoning problems, fall outside the current scope\. Nevertheless, ongoing progress in automated formalization and proof assistants is expected to expand the range of tasks that can be supported\.

## Acknowledgements

This work was supported in part by the Ministry of Education and Science of Bulgaria \(support for INSAIT, part of the Bulgarian National Roadmap for Research Infrastructure\), the Shenzhen Institute of Artificial Intelligence and Robotics for Society \(AIRS\), the Shenzhen Key Laboratory of Crowd Intelligence Empowered Low\-Carbon Energy Network \(No\. ZDSYS20220606100601002\), the National Natural Science Foundation of China \(No\. 72331009\)\.

## References

- Ahnet al\.\(2024\)J\. Ahn, R\. Verma, R\. Lou, D\. Liu, R\. Zhang, and W\. YinLarge language models for mathematical reasoning: progresses and challenges\.InProceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics: Student Research Workshop,N\. Falk, S\. Papi, and M\. Zhang \(Eds\.\),St\. Julian’s, Malta,pp\. 225–237\.External Links:[Link](https://aclanthology.org/2024.eacl-srw.17/),[Document](https://dx.doi.org/10.18653/v1/2024.eacl-srw.17)Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Bertot and Castéran \(2013\)Y\. Bertot and P\. CastéranInteractive theorem proving and program development: coq’art: the calculus of inductive constructions\.Springer Science & Business Media\.Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.
- Buttet al\.\(2024\)N\. Butt, V\. Chandrasekaran, N\. Joshi, B\. Nushi, and V\. BalachandranBenchagents: automated benchmark creation with agent interaction\.InICLR 2025 Workshop on Navigating and Addressing Data Problems for Foundation Models,Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1)\.
- Caoet al\.\(2024\)B\. Cao, M\. Ren, H\. Lin, X\. Han, F\. Zhang, J\. Zhan, and L\. SunStructEval: deepen and broaden large language model assessment via structured evaluation\.InFindings of the Association for Computational Linguistics: ACL 2024,L\. Ku, A\. Martins, and V\. Srikumar \(Eds\.\),Bangkok, Thailand,pp\. 5300–5318\.External Links:[Link](https://aclanthology.org/2024.findings-acl.314/),[Document](https://dx.doi.org/10.18653/v1/2024.findings-acl.314)Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1)\.
- Center for AI Safetyet al\.\(2026\)Center for AI Safety, Scale AI, and HLE Contributors ConsortiumA benchmark of expert\-level academic questions to assess AI capabilities\.Nature649,pp\. 1139–1146\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09962-4),2501\.14249,[Link](https://arxiv.org/abs/2501.14249)Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p2.1)\.
- Chenet al\.\(2025\)S\. Chen, Y\. Chen, Z\. Li, Y\. Jiang, Z\. Wan, Y\. He, D\. Ran, T\. Gu, H\. Li, T\. Xie, and B\. RayBenchmarking large language models under data contamination: a survey from static to dynamic evaluation\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,C\. Christodoulopoulos, T\. Chakraborty, C\. Rose, and V\. Peng \(Eds\.\),Suzhou, China,pp\. 10080–10098\.External Links:[Link](https://aclanthology.org/2025.emnlp-main.511/),[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.511),ISBN 979\-8\-89176\-332\-6Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Chenget al\.\(2025\)Y\. Cheng, Y\. Chang, and Y\. WuA survey on data contamination for large language models\.arXiv preprint arXiv:2502\.14425\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Cobbeet al\.\(2021\)K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. SchulmanTraining verifiers to solve math word problems\.arXiv preprint arXiv:2110\.14168\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p5.1),[§5\.1](https://arxiv.org/html/2609.00062#S5.SS1.p1.1)\.
- De Moura and Bjørner \(2008\)L\. De Moura and N\. BjørnerZ3: an efficient smt solver\.InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems,pp\. 337–340\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p3.1),[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.
- De Mouraet al\.\(2015\)L\. De Moura, S\. Kong, J\. Avigad, F\. Van Doorn, and J\. von RaumerThe lean theorem prover \(system description\)\.InInternational Conference on Automated Deduction,pp\. 378–388\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p3.1),[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.
- Dekonincket al\.\(2026\)J\. Dekoninck, N\. Jovanović, T\. Gehrunger, K\. Rögnvalddson, I\. Petrov, C\. Sun, and M\. VechevBeyond benchmarks: matharena as an evaluation platform for mathematics with llms\.arXiv preprint arXiv:2605\.00674\.Cited by:[Appendix E](https://arxiv.org/html/2609.00062#A5.p2.1.1),[§5\.1](https://arxiv.org/html/2609.00062#S5.SS1.p1.1)\.
- Gaoet al\.\(2025\)B\. Gao, F\. Song, Z\. Yang, Z\. Cai, Y\. Miao, Q\. Dong, L\. Li, C\. Ma, L\. Chen, Z\. Tang,et al\.Omni\-math: a universal olympiad level mathematic benchmark for large language models\.InInternational Conference on Learning Representations,Vol\.2025,pp\. 100540–100569\.Cited by:[§5\.1](https://arxiv.org/html/2609.00062#S5.SS1.p1.1)\.
- Guoet al\.\(2025\)D\. Guo, D\. Yang, H\. Zhang, J\. Song, P\. Wang, Q\. Zhu, R\. Xu, R\. Zhang, S\. Ma, X\. Bi,et al\.DeepSeek\-r1 incentivizes reasoning in llms through reinforcement learning\.Nature645\(8081\),pp\. 633–638\.Cited by:[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p1.1)\.
- Hendryckset al\.\(2021\)D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. SteinhardtMeasuring mathematical problem solving with the MATH dataset\.arXiv preprint arXiv:2103\.03874\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p5.1),[§5\.1](https://arxiv.org/html/2609.00062#S5.SS1.p1.1)\.
- Kovács and Voronkov \(2013\)L\. Kovács and A\. VoronkovFirst\-order theorem proving and vampire\.InInternational Conference on Computer Aided Verification,pp\. 1–35\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p3.1),[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.
- Liet al\.\(2024\)Y\. Li, Y\. Guo, F\. Guerin, and C\. LinAn open\-source data contamination report for large language models\.InFindings of the Association for Computational Linguistics: EMNLP 2024,Y\. Al\-Onaizan, M\. Bansal, and Y\. Chen \(Eds\.\),Miami, Florida, USA,pp\. 528–541\.External Links:[Link](https://aclanthology.org/2024.findings-emnlp.30/),[Document](https://dx.doi.org/10.18653/v1/2024.findings-emnlp.30)Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Linet al\.\(2025\)B\. Y\. Lin, R\. L\. Bras, K\. Richardson, A\. Sabharwal, R\. Poovendran, P\. Clark, and Y\. ChoiZebralogic: on the scaling limits of llms for logical reasoning\.arXiv preprint arXiv:2502\.01100\.Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1)\.
- Linet al\.\(2026\)Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun,et al\.Goedel\-prover\-v2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.2026,pp\. 11793–11818\.Cited by:[Appendix E](https://arxiv.org/html/2609.00062#A5.p2.1),[§1](https://arxiv.org/html/2609.00062#S1.p3.1),[§2](https://arxiv.org/html/2609.00062#S2.p2.1),[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p2.1),[§6\.2\.1](https://arxiv.org/html/2609.00062#S6.SS2.SSS1.p1.1)\.
- Liuet al\.\(2023\)C\. Liu, J\. Shen, H\. Xin, Z\. Liu, Y\. Yuan, H\. Wang, W\. Ju, C\. Zheng, Y\. Yin, L\. Li,et al\.Fimo: a challenge formal dataset for automated theorem proving\.arXiv preprint arXiv:2309\.04295\.Cited by:[Appendix E](https://arxiv.org/html/2609.00062#A5.p2.1)\.
- Qianet al\.\(2024\)K\. Qian, S\. Wan, C\. Tang, Y\. Wang, X\. Zhang, M\. Chen, and Z\. YuVarBench: robust language model benchmarking through dynamic variable perturbation\.InFindings of the Association for Computational Linguistics: EMNLP 2024,Y\. Al\-Onaizan, M\. Bansal, and Y\. Chen \(Eds\.\),Miami, Florida, USA,pp\. 16131–16161\.External Links:[Link](https://aclanthology.org/2024.findings-emnlp.946/),[Document](https://dx.doi.org/10.18653/v1/2024.findings-emnlp.946)Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1),[§5\.3](https://arxiv.org/html/2609.00062#S5.SS3.p1.1)\.
- Reinet al\.\(2024\)D\. Rein, B\. L\. Hou, A\. C\. Stickland, J\. Petty, R\. Y\. Pang, J\. Dirani, J\. Michael, and S\. R\. BowmanGpqa: a graduate\-level google\-proof q&a benchmark\.InFirst conference on language modeling,Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p2.1)\.
- Renet al\.\(2025\)Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang,et al\.Deepseek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[Appendix E](https://arxiv.org/html/2609.00062#A5.p2.1),[§1](https://arxiv.org/html/2609.00062#S1.p3.1),[§2](https://arxiv.org/html/2609.00062#S2.p2.1),[§6\.2\.1](https://arxiv.org/html/2609.00062#S6.SS2.SSS1.p1.1)\.
- Shaoet al\.\(2024\)Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. Li,et al\.Deepseekmath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Spearman \(1904\)C\. SpearmanThe proof and measurement of association between two things\.The American Journal of Psychology15\(1\),pp\. 72–101\.Cited by:[Appendix I](https://arxiv.org/html/2609.00062#A9.SS0.SSS0.Px4.p1.1)\.
- Teamet al\.\(2025\)G\. Team, A\. Kamath, J\. Ferret, S\. Pathak, N\. Vieillard, R\. Merhej, S\. Perrin, T\. Matejovicova, A\. Ramé, M\. Rivière,et al\.Gemma 3 technical report\.arXiv preprint arXiv:2503\.19786\.Cited by:[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p1.1)\.
- Touvronet al\.\(2023\)H\. Touvron, T\. Lavril, G\. Izacard, X\. Martinet, M\. Lachaux, T\. Lacroix, B\. Rozière, N\. Goyal, E\. Hambro, F\. Azhar,et al\.LLaMA: open and efficient foundation language models\.arXiv preprint arXiv:2302\.13971\.Cited by:[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p1.1)\.
- Wanget al\.\(2025a\)H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. D\. Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu,et al\.Kimina\-prover preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.Cited by:[§6\.2\.1](https://arxiv.org/html/2609.00062#S6.SS2.SSS1.p1.1)\.
- Wanget al\.\(2026\)H\. Wang, G\. Dong, H\. Liang, Z\. Zhang, J\. Luo, C\. Liu, C\. Xue, and H\. TangMemGuard: persisting verifier signals for llm\-agent memory governance\.External Links:2608\.21867,[Link](https://arxiv.org/abs/2608.21867)Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p2.1)\.
- Wanget al\.\(2025b\)S\. Wang, Z\. Long, Z\. Fan, X\. Huang, and Z\. WeiBenchmark self\-evolving: a multi\-agent framework for dynamic LLM evaluation\.InProceedings of the 31st International Conference on Computational Linguistics,O\. Rambow, L\. Wanner, M\. Apidianaki, H\. Al\-Khalifa, B\. D\. Eugenio, and S\. Schockaert \(Eds\.\),Abu Dhabi, UAE,pp\. 3310–3328\.External Links:[Link](https://aclanthology.org/2025.coling-main.223/)Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1)\.
- Weiet al\.\(2022\)J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, F\. Xia, E\. Chi, Q\. V\. Le, D\. Zhou,et al\.Chain\-of\-thought prompting elicits reasoning in large language models\.Advances in neural information processing systems35,pp\. 24824–24837\.Cited by:[Appendix I](https://arxiv.org/html/2609.00062#A9.SS0.SSS0.Px3.p4.1)\.
- Yanget al\.\(2025a\)A\. Yang, A\. Li, B\. Yang, B\. Zhang, B\. Hui, B\. Zheng, B\. Yu, C\. Gao, C\. Huang, C\. Lv,et al\.Qwen3 technical report\.arXiv preprint arXiv:2505\.09388\.Cited by:[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p1.1),[§5\.2](https://arxiv.org/html/2609.00062#S5.SS2.p2.1)\.
- Yanget al\.\(2023\)K\. Yang, A\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. J\. Prenger, and A\. AnandkumarLeandojo: theorem proving with retrieval\-augmented language models\.Advances in Neural Information Processing Systems36,pp\. 21573–21612\.Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.
- Yanget al\.\(2025b\)Y\. Yang, H\. Yamada, and T\. TokunagaEvaluating robustness of LLMs to numerical variations in mathematical reasoning\.InThe Sixth Workshop on Insights from Negative Results in NLP,A\. Drozd, J\. Sedoc, S\. Tafreshi, A\. Akula, and R\. Shu \(Eds\.\),Albuquerque, New Mexico,pp\. 171–180\.External Links:[Link](https://aclanthology.org/2025.insights-1.16/),[Document](https://dx.doi.org/10.18653/v1/2025.insights-1.16),ISBN 979\-8\-89176\-240\-4Cited by:[Appendix I](https://arxiv.org/html/2609.00062#A9.SS0.SSS0.Px3.p3.1)\.
- Yinget al\.\(2024\)J\. Ying, Y\. Cao, Y\. Bai, Q\. Sun, B\. Wang, W\. Tang, Z\. Ding, Y\. Yang, X\. Huang, and S\. YANAutomating dataset updates towards reliable and timely evaluation of large language models\.InThe Thirty\-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track,External Links:[Link](https://openreview.net/forum?id=EvEqYlQv8T)Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1),[§5\.3](https://arxiv.org/html/2609.00062#S5.SS3.p1.1)\.
- Zhaiet al\.\(2026\)W\. Zhai, Z\. Wang, J\. Wang, B\. Yang, X\. Li, X\. Xu, B\. Wang, P\. Wang, X\. Wu, A\. Li,et al\.HLE\-verified: a systematic verification and structured revision of humanity’s last exam\.arXiv preprint arXiv:2602\.13964\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p2.1)\.
- Zhaoet al\.\(2025\)Y\. Zhao, G\. Gan, C\. Wang, C\. Zhao, and A\. CohanAre multimodal LLMs robust against adversarial perturbations? RoMMath: a systematic evaluation on multimodal math reasoning\.InProceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies \(Volume 1: Long Papers\),L\. Chiruzzo, A\. Ritter, and L\. Wang \(Eds\.\),Albuquerque, New Mexico,pp\. 11653–11665\.External Links:[Link](https://aclanthology.org/2025.naacl-long.582/),[Document](https://dx.doi.org/10.18653/v1/2025.naacl-long.582),ISBN 979\-8\-89176\-189\-6Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Zhenget al\.\(2021\)K\. Zheng, J\. M\. Han, and S\. PoluMinif2f: a cross\-system benchmark for formal olympiad\-level mathematics\.arXiv preprint arXiv:2109\.00110\.Cited by:[Appendix I](https://arxiv.org/html/2609.00062#A9.SS0.SSS0.Px3.p4.3),[§6\.2\.1](https://arxiv.org/html/2609.00062#S6.SS2.SSS1.p1.1)\.
- Zhouet al\.\(2026a\)X\. Zhou, X\. Wang, Y\. He, R\. Zou, Y\. Wu, Y\. Cheng, Y\. Xie, W\. Liu, H\. Zhao, Y\. Xu,et al\.Engibench: a benchmark for evaluating large language models on engineering problem solving\.InFindings of the Association for Computational Linguistics: ACL 2026,pp\. 36308–36334\.Cited by:[§1](https://arxiv.org/html/2609.00062#S1.p1.1)\.
- Zhouet al\.\(2026b\)X\. Zhou, R\. Zou, X\. Wang, Y\. Cheng, Y\. Xu, J\. Zhao, and J\. GuEngiAgent: fully connected coordination of LLM agents for solving open\-ended engineering problems with feasible solutions\.InForty\-third International Conference on Machine Learning,External Links:[Link](https://openreview.net/forum?id=1p67QsYnbv)Cited by:[§3\.2](https://arxiv.org/html/2609.00062#S3.SS2.p3.1)\.
- Zhouet al\.\(2024\)Y\. Zhou, Y\. Zhu, D\. Antognini, Y\. Kim, and Y\. ZhangParaphrase and solve: exploring and exploiting the impact of surface form on mathematical reasoning in large language models\.InProceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies \(Volume 1: Long Papers\),K\. Duh, H\. Gomez, and S\. Bethard \(Eds\.\),Mexico City, Mexico,pp\. 2793–2804\.External Links:[Link](https://aclanthology.org/2024.naacl-long.153/),[Document](https://dx.doi.org/10.18653/v1/2024.naacl-long.153)Cited by:[Appendix I](https://arxiv.org/html/2609.00062#A9.SS0.SSS0.Px3.p2.1)\.
- Zhuet al\.\(2024\)Q\. Zhu, Q\. Cheng, R\. Peng, X\. Li, R\. Peng, T\. Liu, X\. Qiu, and X\. HuangInference\-time decontamination: reusing leaked benchmarks for large language model evaluation\.InFindings of the Association for Computational Linguistics: EMNLP 2024,Y\. Al\-Onaizan, M\. Bansal, and Y\. Chen \(Eds\.\),Miami, Florida, USA,pp\. 9113–9129\.External Links:[Link](https://aclanthology.org/2024.findings-emnlp.532/),[Document](https://dx.doi.org/10.18653/v1/2024.findings-emnlp.532)Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p1.1),[§5\.3](https://arxiv.org/html/2609.00062#S5.SS3.p1.1)\.
- Zhuet al\.\(2025\)T\. Zhu, J\. Clune, J\. Avigad, A\. Q\. Jiang, and S\. WelleckPremise selection for a lean hammer\.arXiv preprint arXiv:2506\.07477\.Cited by:[§2](https://arxiv.org/html/2609.00062#S2.p2.1)\.

## Appendix AThe Use of Large Language Models

In this work, LLMs were used in four main ways:

1. 1\.Benchmark rewriting and feasibility screening\.LLMs were used to generate rewritten problem instances from existing benchmarks and to perform preliminary feasibility screening by identifying obviously invalid, ambiguous, or infeasible rewritten instances\.
2. 2\.Semantic consistency checking during formalization\.LLMs were used to assess whether rewritten natural\-language problems are semantically consistent with their corresponding Lean formal statements\. This check serves only as a conservative pre\-proof filter and does not provide formal verification of natural\-language\-to\-Lean equivalence\.
3. 3\.Answer extraction and target\-answer matching\.LLMs were used to extract candidate final answers from Lean\-verified proofs and check whether the extracted spans match the quantities requested by the rewritten problems\. Candidate answers were restricted to spans that appear verbatim in the verified Lean proof, and no additional computation, simplification, or reasoning was allowed\.
4. 4\.Figure and language assistance\.AI tools were used to generate some visual icons in Fig\.[1](https://arxiv.org/html/2609.00062#S1.F1)and Fig\.[2](https://arxiv.org/html/2609.00062#S1.F2), where applicable, other illustrative icons used in the figures\. AI tools were also used for grammar checking and language refinement during the writing of this paper\. All scientific claims, experimental results, and analyses were reviewed and verified by the authors\.

## Appendix BPrompt Templates and Implementation Details

This appendix reports the main prompt templates and implementation details used in RePro\. We include the prompts for problem rewriting, feasibility screening, semantic alignment screening, proof\-grounded answer extraction, and final\-answer classification\. The templates are lightly formatted for readability\. The released code contains the exact runtime prompts and parsing logic\.

##### Problem rewriting prompt\.

The rewriting prompt asks the model to generate a new problem while preserving the underlying mathematical structure, solution logic, and answer type\. It explicitly forbids solving the problem or computing the new answer\.

1Youareatop\-levelexamquestiondesignexpert\.Yourgoalistorewritethegivenquestionwhilepreservingitscoremathematicalstructure,solutionlogic,anddifficulty,butmakingitentirelynewinform,wording,andsurfacemeaning\.

2

3Generalrequirements:

41\.Therewrittenquestionremainssolvableandmaintainsasimilarlevelofdifficulty\.

52\.Theunderlyingmathematicalrelationships,reasoningmethod,andsolutionlogicremainequivalent\.

63\.Therewrittenquestionisvalidandlogicallyconsistent\.

74\.Therewrittenquestionisentirelydifferentfromtheoriginalinsurfaceform,wording,andsemantics\.

85\.Nopartoftheoriginalphrasing,expressions,ornarrativeshouldbereused\.

96\.Ifapreviousrewriteisprovided,thenewrewritemustbesignificantlydifferentfromit\.

10

11Forwordproblems:

121\.Completelychangethestorycontextorscenario\.

132\.Changethetime,place,characters,identities,andphysicalquantitiesinvolved\.

143\.Userealisticandphysicallypossiblesituations\.

154\.Chooseatargetunknownthatisclearlywell\-definedandnotsemanticallyambiguous\.

16

17Forpuremathematicalproblems:

181\.Keeptherewrittenquestionpurelymathematical\.

192\.Donotintroduceastoryorreal\-worldcontext\.

20

21Rewritingstrategies:

22\-Numericalreparameterization\.

23\-Logicalrestructuring\.

24\-Constraintmodification\.

25\-Contextualreconstructionforwordproblems\.

26

27Answer\-typepreservation:

28Therewrittenproblemmustpreservethetypeoftheexpectedanswerfromtheoriginalproblem,suchasinteger,rationalnumber,interval,orfiniteset\.Donotsolvetheproblemorcomputetheanswer\.Enforceanswer\-typepreservationstructurally,forexamplebyusinglinearexpressions,proportionalrelationships,orfactorizablepolynomialswhentheoriginalanswerisrationalorintegral\.

29

30ReturnvalidJSONonly:

31\{

32"rewritten\_question":"<therewrittenquestionasastring\>"

33\}

The runtime user input is:

1Originalquestion:

2<originalproblem\>

##### Feasibility screening prompt\.

Feasibility screening is used as an early filter\. Its purpose is to reject rewritten questions that are ill\-defined, infeasible, ambiguous, internally inconsistent, or unrealistic\. It does not establish reference\-answer correctness; answer correctness is established later through Lean verification\.

1Youareanexpertinmathematicsandcarefulprobleminterpretation\.

2

3Yourtaskisnotonlytocheckwhethertheproblemismathematicallysolvable,buttojudgewhetheritiswell\-defined,unambiguous,andvalidunderstrictinterpretation\.

4

5Firstclassifytheproblemintooneoftwocategories:

6

7\(A\)Puremathematicalproblem:

8\-Noreal\-worldstoryorphysicalinterpretationisinvolved\.

9\-Examplesincludesolvingequations,findingdomains,simplifyingexpressions,algebraicmanipulation,andfunctionproperties\.

10

11\(B\)Real\-worldorappliedproblem:

12\-Theproblemreferstopeople,objects,money,measurements,experiments,physicalprocesses,orreal\-worldactions\.

13

14Thenapplythecorrespondingverificationstandard\.

15

16Yourtasks:

171\.Solvetheproblem\.

182\.Classifyitaseither\(A\)puremathematicalor\(B\)real\-world/applied\.

193\.Judgewhethertheproblemstatementandthefinalnumericalanswerarevalidundertheappropriatestrictstandard\.

20

21Forpuremathematicalproblems,check:

22\-Uniqueness\.

23\-Mathematicalclarity\.

24\-Answer\-typeandformatconsistency\.

25\-Mathematicalreasonableness\.

26

27Forreal\-worldorappliedproblems,check:

28\-Uniqueness\.

29\-Semanticclarity\.

30\-Real\-worldexecutability\.

31\-Unitandmeaningconsistency\.

32\-Reasonableness\.

33

34Forbothcategories:

35Ifthereisanyambiguity,vagueness,underspecification,incompatiblecondition,ormismatchbetweenthemathematicalanswerandtherequiredinterpretationstandard,theverdictmustbe"no"\.

36

37ReturnvalidJSONonly:

38\{

39"analysis":"<solutionandchecks\>",

40"verdict":"yes/no"

41\}

The runtime user input is:

1Question:

2<rewrittenproblem\>

##### Formalization and proof\-generation prompts\.

The formalizer and prover are called through backend models with short task instructions\. The generated Lean statement must compile before semantic screening\. A generated proof is accepted only if it passes Lean checking and does not containsorry\.

1FormalizethefollowingquestioninLean4:

2<rewrittenproblem\>

1ProvethefollowingstatementinLean4withoutusing'sorry':

2<Leanformalstatement\>

##### Semantic alignment screening prompt\.

The semantic alignment prompt checks whether a compiled Lean statement appears to encode the same task as the rewritten natural\-language problem\. This step is an LLM\-assisted conservative screen rather than a formal proof of natural\-language\-to\-Lean equivalence\.

1YouareanexpertinanalyzingsemanticconsistencybetweenanaturallanguagemathproblemanditsformalrepresentationinLean4\.

2

3Yourtaskistojudgewhethertheformalstatementmatchesthenaturallanguageproblemsemantically\.

4

5Youmustnotsolvetheproblem,computeanyvalues,orverifythecorrectnessoftheresult\.Yourtaskispurelysemantic\.

6

7AformalizationisconsideredConsistentifandonlyif:

81\.Thesamequantitiesarebeingreferredto\.

92\.Thesameconditionsareimposed\.

103\.Thesamelogicalstructureispreserved\.

114\.Thesametypeofobjectisbeingreasonedabout,suchasdiscretevscontinuous,individualvsaggregate,orinstancevsrange\.

125\.Thesametargetquantityisbeingcharacterized\.

13

14JudgetheformalizationasInconsistentifanyofthefollowingoccurs:

15A\.Logicalstructuremismatch\.

16B\.Wrongtargetquantity\.

17C\.Quantitativemismatchinnumbers,constraints,arithmeticrelationships,units,orconstants\.

18D\.Missingcondition\.

19E\.Extracondition\.

20

21Specialwarningaboutrounding,ceiling,andfloor:

22Ifthenaturallanguageproblemrequiresaroundingconvention,suchas"mustbuywholeitems"or"roundup",andtheLeanformalizationfailstoencodethatconventioncorrectly,thenitisinconsistent\.

23

24Thenatural\-languagemeaningmustmatchexactly\.EvenasmallmismatchmeansInconsistent\.

25

26ReturnvalidJSONonly:

27\{

28"judgment":"Consistent",

29"explanation":"<reason\>"

30\}

31or

32\{

33"judgment":"Inconsistent",

34"explanation":"<reason\>"

35\}

The runtime user input is:

1Naturallanguageproblem:

2<rewrittenproblem\>

3

4Lean4formalstatement:

5<Leantheoremstatement\>

For each compiled Lean statement, the semantic checker is queried three times\. The candidate is retained only when all three responses returnConsistent\. AnyInconsistentresponse, parsing failure, malformed output, or uncertain response leads to rejection and regeneration\.

##### Proof\-grounded answer extraction prompt\.

After a proof passes Lean verification, RePro extracts an answer candidate from the verified proof\. The extractor is read\-only: it may only copy spans that already appear in the Lean proof text\.

1YouareastrictanswerextractorforLean4prooftext\.

2

3Youaregiven:

4\-Thenatural\-languageproblem\.

5\-TheLean4prooftext\.

6

7Yourjob:

8\-Identifytheexactfinalnumericansweroranswersrequestedbythenatural\-languageproblem\.

9\-Youmustnotcomputeanything\.

10\-Youmustnotsimplifyanything\.

11\-Youmustnotevaluatearithmeticexpressions\.

12\-YoumustonlycopyanswercandidatesthatliterallyappearintheLeantext\.

13

14Ifthenatural\-languageproblemasksformultiplequantities,thenextractallofthemandoutputtheminonestringseparatedbytop\-levelcommas\.

15

16Allowed:

17\-CopyexistingexpressionsfromtheLeantextas\-is\.

18\-Selecttheexpressionsthatmatchthequantityaskedbytheproblem\.

19

20Notallowed:

21\-Arithmetic\.

22\-Evaluationofpowersorfactorials\.

23\-Symbolicsimplification\.

24\-Cancellation,expansion,orfractionreduction\.

25\-Anyinferencerequiringanewstep\.

26\-Usingresultsfrominteractivecommandssuchas

27

28ReturnvalidJSONonly:

29\{

30"answer":"<string\>",

31"evidence":"<snippetcopiedfromLeantext\>"

32\}

33

34Ifnouniqueliteralanswercandidatecanbefound,oriftheproofdeterminesonlypartoftherequestedquantities,return:

35\{

36"answer":"unknown",

37"evidence":"unknown"

38\}

The runtime user input is:

1Naturallanguageproblem:

2<rewrittenproblem\>

3

4Lean4prooftext:

5<Leanproof\>

6

7Task:

8IdentifytherequestedquantityorquantitiesandextracttheanswercandidateonlybycopyingfromtheLeantext\.Donotcomputeorsimplify\.Donotuse

In addition to the prompt, RePro applies string\-level checks to ensure that every comma\-separated part of the extracted answer appears in the Lean proof text\. Candidates that appear only near interactive commands such as\#eval,\#reduce,\#check, or\#printare rejected\.

##### Final\-answer classification prompt\.

Literal extraction alone is insufficient because a verified proof may contain intermediate values or values for a different target\. RePro therefore uses a second classifier to determine whether the extracted candidate is the final answer requested by the rewritten problem\.

1YouareastrictclassifierforextractedanswersfromLean4prooftext\.

2

3Youaregiven:

4\-Thenatural\-languageproblem\.

5\-TheLeanprooftext\.

6\-AnextractedanswercandidatestringthatappearsintheLeantext\.

7

8Thecandidatemaycontainmultiplerequestedquantitiesseparatedbycommasattoplevel\.

9

10Yourjob:

11Donotcomputeorsimplifyanything\.Decidewhetherthecandidateisoneofthefollowing:

12

13final:

14Exactlythequantityorquantitiesasked,withnofurthercomputation,simplification,orevaluationneeded\.

15

16intermediate:

17Anunfinishedformthatwouldrequirecomputation,simplification,orevaluation\.

18

19wrong\_target:

20Avalidstatementorvalue,butnotthequantityrequestedbytheproblem\.

21

22unknown:

23Nouniquefinalanswercanbedeterminedfromtheprovidedtextorcandidate,ortheproofdeterminesonlypartoftherequestedquantities\.

24

25Strictrules:

26\-Anycandidatecontaininganunexecutedarithmeticoperatororevaluation,suchas\+,\-,\*,/,^,or\!,shouldbetreatedasintermediateunlesstheproblemexplicitlyasksforthatexactexpressionform\.

27\-Anycandidaterelyingon

28\-Iftheproblemasksformultiplequantitiesbutthecandidateprovidesfewer,classifyitasunknown\.

29\-Donotinventsemanticconversions\.

30\-Donotevaluateproductsorpowers\.

31

32ReturnvalidJSONonly:

33\{

34"answer":"<string\>",

35"status":"final\|intermediate\|wrong\_target\|unknown",

36"explanation":"<shortreason\>"

37\}

The runtime user input is:

1Naturallanguageproblem:

2<rewrittenproblem\>

3

4Lean4prooftext:

5<Leanproof\>

6

7Extractedcandidate:

8<candidateanswer\>

9

10Evidencesnippets:

11<snippetscopiedfromLeantext\>

12

13NowclassifythecandidateunderthestrictrulesandoutputJSONonly\.

Only candidates classified asfinalare accepted as reference answers\. Candidates classified asintermediate,wrong\_target, orunknownare rejected, and the corresponding rewritten instance is not retained\.

## Appendix CSemantic Alignment Screening and Target\-Answer Matching

During executable formalization, RePro adopts a layered validation design to reduce the risk of semantic mismatch between the rewritten natural\-language problem and the Lean formal statement\. This design contains two complementary steps\. First, before proof search, an LLM\-assisted semantic alignment screen filters out Lean statements that are syntactically valid but appear semantically inconsistent with the rewritten problem\. Second, after Lean verification, a proof\-grounded target\-answer matching step checks whether the extracted answer corresponds to the final quantity requested by the rewritten problem\.

##### Semantic alignment screen\.

After a generated Lean statement passes compilation, RePro applies a conservative semantic alignment screen\. The checker receives only the rewritten natural\-language problem and the generated Lean 4 statement\. It does not receive the original problem, the final answer, or the proof, and is explicitly instructed not to solve the problem, compute any value, or judge answer correctness\. Instead, it checks whether the Lean statement preserves the same quantities, conditions, logical structure, object type, and target quantity as the rewritten problem\.

A formalization is rejected if the checker detects mismatched constants, arithmetic relations, units, constraints, variable domains, logical connectives, target quantity, or required discrete operations such as rounding, ceiling, or floor behavior\. Missing conditions and extra conditions are also treated as semantic mismatches\.

##### Conservative all\-pass policy\.

To reduce false acceptance, we adopt a conservative all\-pass policy\. For each compiled Lean statement, the semantic checker is queried three times using Qwen3\-Max with temperature zero\. A candidate passes semantic screening only if all three calls returnConsistent\. AnyInconsistentjudgment, JSON parsing failure, malformed output, or uncertain response leads to rejection and regeneration\. This policy makes the screen intentionally conservative: it may discard some valid formalizations, but it reduces the chance that an apparent semantic mismatch enters proof search\.

##### Target\-answer matching after Lean verification\.

Semantic screening checks whether the Lean statement appears to encode the same task as the rewritten problem, but it is not used to verify answer correctness\. Therefore, RePro applies a separate target\-answer matching step after proof\-level verification\. This step consists of two strictly constrained substeps: extracting an answer candidate from the Lean\-verified proof and then checking whether the candidate is the final quantity requested by the rewritten problem\.

During answer extraction, the candidate answer must be copied from literal spans that already appear in the verified proof\. The extractor is not allowed to perform additional computation, normalization, simplification, or inference\. Candidates that appear only in interactive commands such as\#eval,\#reduce,\#check, or\#printare rejected\.

During answer classification, RePro determines whether the copied candidate is the final answer, an intermediate value, a wrong\-target value, an unresolved expression, or unknown\. A rewritten instance is retained only when the candidate is classified asfinaland matches the target quantity requested by the rewritten problem\.

##### Reliability scope\.

The semantic alignment screen is not a formal proof of natural\-language\-to\-Lean equivalence\. Instead, it serves as a conservative pre\-proof filter to reduce apparent semantic drift before formal verification\. RePro does not rely on a single LLM judgment to establish retained\-instance reliability\. Instead, it uses multiple automated safeguards to reduce false acceptance: Lean compilation, conservative semantic screening, ATP\-generated proof verification by Lean, proof\-grounded answer extraction, and strict target\-answer matching\. The strongest formal guarantee applies to the Lean\-verified proof for the accepted formal statement, while natural\-language\-to\-Lean alignment and final answer\-target alignment are supported by conservative LLM\-assisted screening, proof\-grounded extraction constraints, and strict classification\.

## Appendix DObtaining the Final Answer from Verified Proofs

##### Design goal\.

After a formally verified proof is obtained, the system must recover the final answer corresponding to the quantity requested in the rewritten problem\. A key requirement is that this post\-proof stage must not introduce any new reasoning beyond the verified proof itself\.

A naive design would directly generate the final answer from the proof\. However, this would allow post\-hoc computation, simplification, or selection among intermediate results, effectively turning answer reporting into a second solving process\. Such behavior would weaken the RePro guarantee and reduce reproducibility\. To avoid this issue, post\-proof answer recovery is divided into two constrained steps:*literal answer extraction*and*final\-answer checking*\.

##### Literal answer extraction\.

The first step is purely read\-only\. It extracts spans that appear verbatim in the verified proof and does not allow computation, normalization, inference, or rewriting\. Thus, the procedure may copy text from the proof, but may not derive new text\.

For example, if the proof containshave h : x = 17 := by \.\.\., then17can be extracted\. If the proof contains2 \+ 3, outputting5is not allowed\. If the proof contains\{3\}, outputting3is not allowed unless3also appears explicitly\.

For problems with multiple target quantities, all corresponding spans are returned, separated by commas, without reordering or reformatting\.

For instance, if the proof containsa = 2andb = 5, the extractor may output2, 5, but not\(2,5\)unless that exact form appears in the proof\.

##### Final\-answer checking\.

Literal extraction alone does not guarantee that the extracted span corresponds to the quantity requested in the problem, since a verified proof may contain intermediate values, auxiliary constants, or witness terms\.

Therefore, a second step checks whether the extracted candidate matches the target quantity specified in the rewritten problem\. Importantly, this step is restricted to target alignment only: it does not generate a new answer, perform additional computation, or replace the extracted span with a derived result\.

For example, if the problem asks forx\+yx\+yand the proof containsx = 3,y = 4, andx \+ y = 7, then3and4are proof\-grounded but not final, while7is both proof\-grounded and final\.

If the problem asks for bothaaandbb, and the proof containsa = 2,b = 5, anda\+b = 7, then2, 5is final, whereas7is not\.

##### Summary\.

This design guarantees \(1\) traceability to the verified proof, \(2\) no answer generation after proof verification, and \(3\) alignment with the quantity requested in the problem\.

As a result, the final reported answer remains proof\-grounded, query\-aligned, and free of post\-hoc reasoning, which preserves the RePro principle\.

## Appendix EDataset Selection and Data Distribution

Dataset selection\.We select GSM8K and MATH for systematic evaluation because they remain widely used benchmarks for mathematical reasoning, contamination analysis, and benchmark rewriting, while also matching the current capability range of Lean\-oriented neural ATPs\. GSM8K contains structured grade\-school math word problems with a relatively convergent solution space, making it suitable for controlled rewriting\. MATH covers five AoPS difficulty levels, ranging from basic high\-school exercises to olympiad\-level problems, enabling evaluation across different reasoning complexities\.

We also considered harder benchmarks such as AIME and Omni\-MATH\. However,our preliminary experiment on 30 AIME 2025 problems[Dekoninck et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib35)yields a RePro generation success rate of 0%, suggesting that current ATP\-based verification may still be insufficient for reliably constructing rewritten instances at this difficulty level\. This observation is also consistent with recent results on high\-difficulty formal proof generation benchmarks such as FIMO[Liu et al\. \(2023\)](https://arxiv.org/html/2609.00062#bib.bib34)and DeepSeek\-ProverBench[Ren et al\. \(2025\)](https://arxiv.org/html/2609.00062#bib.bib23), which are relevant to olympiad\-style formal reasoning\. Under pass@32, current 7B\-8B Lean\-oriented prover models achieve only 3\.35\-7\.05% on FIMO and 0\.31\-1\.53% on DeepSeek\-ProverBench, as summarized in Table[2](https://arxiv.org/html/2609.00062#A5.T2)[Lin et al\. \(2026\)](https://arxiv.org/html/2609.00062#bib.bib27)\. Therefore, we focus on the relatively more tractable GSM8K and MATH benchmarks in this work, and leave broader evaluation on harder benchmarks such as AIME and Omni\-MATH to future work as ATP capabilities improve\.

ModelFIMODeepSeek\-ProverBenchDeepSeek\-Prover\-V2\-7B5\.700\.31Kimina\-Prover\-7B3\.351\.38Goedel\-Prover\-V2\-8B7\.051\.53Table 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\.Sampling protocol\.Specifically, we adopt a rejection sampling procedure: candidate problems are randomly drawn from the source datasets and passed through the RePro pipeline\. Only instances that satisfy all verification criteria are retained\. This process continues until the number of valid rewritten instances reaches around 200 for each subset\.

Full dataset\.The full dataset refers to all sampled candidate problems before filtering\. As shown in Fig\.[9](https://arxiv.org/html/2609.00062#A5.F9), the number of sampled candidates varies across subsets because rejection sampling continues until approximately 200 verified instances are obtained for each subset\. Consequently, harder levels such as LV4 and LV5 require substantially more sampled candidates due to their lower retention rates\.

RePro successful generation subset\.The final evaluation set consists only of instances that pass RePro verification\. Due to the rejection sampling process, the resulting subset exhibits a nearly uniform distribution, with approximately 200 instances per difficulty level\.

Retention\-rate analysis\.As shown in Fig\.[9](https://arxiv.org/html/2609.00062#A5.F9), the retention rate decreases substantially as problem difficulty increases\. Specifically, RePro retains 88\.3% of sampled GSM8K candidates, while the retention rates on MATH are 92\.2%, 75\.8%, 73\.9%, 57\.1%, and 33\.7% for LV1–LV5, respectively\. This pattern reveals a clear difficulty\-dependent selection effect: under current formalization and proving capabilities, harder problems are less likely to pass the full verification pipeline\. Consequently, although rejection sampling produces a nearly balanced final subset with approximately 200 instances per difficulty level, this retained subset does not preserve the original difficulty distribution of MATH\. This observation further highlights that the current coverage of RePro is constrained by the capabilities of the underlying formalizer and ATP\.

Reproducibility\.All generated datasets, including rewritten problems and their formally verified proofs, are publicly released to facilitate reproducibility and further research\.

Figure 9:Data distribution before and after RePro filtering\.
## Appendix FRePro Dataset Metadata

Each instance in the RePro dataset corresponds to a rewritten problem derived from GSM8K or MATH, together with its reference answer and a formally verified proof\. Only instances that pass the RePro verification pipeline are retained\.

Each instance contains the following fields:

- •original\_question– Original problem statement sampled from the source benchmark\.
- •original\_answer– Ground\-truth answer to the original problem\.
- •rewritten\_question– Rewritten version of the original problem generated by the rewriting pipeline\.
- •new\_answer– Reference answer corresponding to the rewritten problem\.
- •lean\_proof– Formal proof in Lean that verifies the correctness of the rewritten problem and its answer\.

## Appendix GRepresentative Successful RePro Cases

This section presents representative successful generation cases from RePro\. Each case includes the original problem, the rewritten problem, the Lean formal statement, the verified answer, and a short explanation of why the instance passes the RePro verification pipeline\. To avoid LaTeX compilation issues with Unicode symbols, we display Lean statements in ASCII form\. The complete Lean proofs are included in the released dataset\.

##### Case 1\. GSM8K word problem with unit conversion\.

Original problem\.James buys 2 notebooks with 50 pages each\. He pays $5\. How many cents did each page cost?

Rewritten problem\.A student purchases 4 sketchbooks, each containing 80 sheets of paper, for a total of $16\. What is the cost per sheet in cents?

Verified answer\.5

Lean formal statement\.

1theoremcost\_per\_sheet:

2lettotal\_cost\_cents:Rat:=16\*100

3lettotal\_sheets:Rat:=4\*80

4total\_cost\_cents/total\_sheets=5:=by

Verification outcome\.The ATP\-generated proof is accepted by Lean\. The proof establishes that the total cost is 1600 cents, the total number of sheets is 320, and the unit cost is 5 cents per sheet\.

Why this instance passes RePro\.The rewritten problem is well\-defined because the requested quantity, cost per sheet in cents, is explicit\. It is feasible because the monetary and counting quantities are realistic and internally consistent\. The Lean statement preserves the same unit\-conversion structure as the natural\-language problem\. The final answer is extracted from the verified proof and corresponds to the requested quantity\.

##### Case 2\. MATH inverse\-function problem with a set\-valued answer\.

Original problem\.Definef⁡\(x\)=3​x−8f\(x\)=3x\-8\. Iff−1f^\{\-1\}is the inverse offf, find the value or values ofxxfor whichf​\(x\)=f−1​\(x\)f\(x\)=f^\{\-1\}\(x\)\.

Rewritten problem\.Letg⁡\(x\)=5​x−12g\(x\)=5x\-12\. Ifg−1g^\{\-1\}denotes the inverse function ofgg, determine all real numbersxxsuch thatg​\(x\)=g−1​\(x\)g\(x\)=g^\{\-1\}\(x\)\.

Verified answer\.\{3\}\\\{3\\\}

Lean formal statement\.

1theoremg\_inverse:

2letg:Real\-\>Real:=funx=\>5\*x\-12

3letg\_inv:Real\-\>Real:=funx=\>\(x\+12\)/5

4\{x:Real\|gx=g\_invx\}=\(\{3\}:SetReal\):=by

Verification outcome\.The ATP\-generated proof is accepted by Lean\. The proof verifies the equality between the solution set ofg​\(x\)=g−1​\(x\)g\(x\)=g^\{\-1\}\(x\)and the singleton set\{3\}\\\{3\\\}\.

Why this instance passes RePro\.The rewritten problem has a clear target: the full set of real solutions\. The formal statement encodes the function, its inverse, and the requested solution set\. The proof verifies set equality rather than merely showing that one candidate solution works\. This ensures that the retained answer is proof\-grounded and target\-aligned\.

##### Case 3\. MATH symbolic factorization problem\.

Original problem\.Factor36−4​x236\-4x^\{2\}completely\.

Rewritten problem\.Factor81−9​y281\-9y^\{2\}completely\.

Verified answer\.9​\(3−y\)​\(3\+y\)9\(3\-y\)\(3\+y\)

Lean formal statement\.

1theoremfactor\_81\_minus\_9y2\(y:Real\):

281\-9\*y^2=9\*\(3\-y\)\*\(3\+y\):=by

Verification outcome\.The ATP\-generated proof is accepted by Lean\. The proof verifies the algebraic identity between the original expression and the factored expression\.

Why this instance passes RePro\.This case shows that RePro supports symbolic answers, not only numerical answers\. The rewritten problem asks for a factored expression, and the Lean statement verifies the equivalence between the expanded and factored forms\. The answer extraction step accepts the expression because the requested target is a symbolic factorization and the answer is grounded in the verified proof\.

##### Case 4\. MATH optimization problem with a minimum value\.

Original problem\.Square A and Square B are both20092009by20092009squares\. Square A has both its length and width increased by an amountxx, while Square B has both its length and width decreased by the same amountxx\. What is the minimum value ofxxsuch that the difference in area between the two new squares is at least as great as the area of a20092009by20092009square?

Rewritten problem\.Two identical square plots of land each measure18731873meters on a side\. One plot is expanded by addingyymeters to both its length and width, while the other is reduced by subtractingyymeters from both its length and width\. What is the smallest positive value ofyysuch that the absolute difference in area between the two modified plots is at least equal to the area of one original plot?

Verified answer\.1873/41873/4

Lean formal statement\.

1theoremminimum\_area\_difference:

2letoriginal\_side:Real:=1873

3letexpanded\_area:Real\-\>Real:=

4funy=\>\(original\_side\+y\)^2

5letreduced\_area:Real\-\>Real:=

6funy=\>\(original\_side\-y\)^2

7letoriginal\_area:Real:=original\_side^2

8letarea\_difference:Real\-\>Real:=

9funy=\>abs\(expanded\_areay\-reduced\_areay\)

10letcondition:Real\-\>Prop:=

11funy=\>And\(y\>0\)\(original\_area<=area\_differencey\)

12Exists\(funy:Real=\>

13And\(y=original\_side/4\)

14\(And\(conditiony\)

15\(forallz:Real,conditionz\-\>y<=z\)\)\):=by

Verification outcome\.The ATP\-generated proof is accepted by Lean\. The proof verifies thaty=1873/4y=1873/4satisfies the area\-difference condition and that every positive value satisfying the condition is at least1873/41873/4\.

Why this instance passes RePro\.This case demonstrates a more complex successful rewrite\. The rewritten problem changes the numerical parameter and real\-world context while preserving the optimization structure\. The Lean statement encodes the positivity condition, the area inequality, and the minimality requirement\. Therefore, the pipeline does not merely verify that the answer satisfies the inequality; it also verifies that it is the smallest valid value\.

##### Summary\.

These cases illustrate different types of retained RePro instances\. Case 1 shows a real\-world arithmetic problem with unit conversion\. Case 2 shows a set\-valued algebraic answer\. Case 3 shows a symbolic expression answer\. Case 4 shows an optimization problem requiring a minimality proof\. In each case, the rewritten problem passes feasibility screening, the Lean statement compiles, the semantic alignment screen accepts the formalization, the ATP\-generated proof passes Lean verification, and the extracted answer corresponds to the target quantity requested by the rewritten problem\.

## Appendix HReliability Interpretation and Human Validation

RePro is a verification\-driven benchmark rewriting framework\. Therefore, the reported 100% well\-definedness, feasibility, and answer correctness should be interpreted as reliability metrics for the retained rewritten instances, rather than as a claim that all raw LLM\-generated rewrites are correct\.

In RePro, generation and verification are explicitly decoupled\. LLMs first generate candidate rewritten problems, and the verification pipeline then filters these candidates through feasibility screening, executable formalization, proof generation, Lean verification, and target\-answer matching\. A rewritten instance is retained only when its reference answer is supported by an ATP\-generated proof that passes Lean kernel\-level verification, and when the verified answer matches the target quantity requested in the rewritten problem\. Therefore, the correctness metric measures whether the retained reference answers are backed by formally verified proof certificates\.

This result should be interpreted together with the generation rate\. Correctness measures the reliability of retained instances, while generation rate measures the coverage cost required to obtain such verified instances\. In other words, RePro does not assume that all generated candidates are correct\. Instead, it removes unreliable candidates and retains only those that satisfy the full verification pipeline\.

To further examine whether the automatic verification toolchain introduces potential bias, we conduct an independent human validation for all rewriting methods\. For each method, including RePro, Auto\-Dataset, ITD, and VarBench, we randomly sample 600 rewritten instances, consisting of 100 instances from GSM8K and 100 instances from each difficulty level of MATH\. In total, the human validation covers 2,400 rewritten instances\.

For each sampled instance, human auditors are given only the original problem, the rewritten problem, and the reference answer\. The automatic pipeline decisions, Lean formalizations, ATP outputs, and verified proofs are not used during human validation\. Human auditors evaluate each instance according to the three reliability criteria defined in Sec\.[4](https://arxiv.org/html/2609.00062#S4): well\-definedness, feasibility, and answer correctness\.

Table[3](https://arxiv.org/html/2609.00062#A8.T3)reports the human validation results\. The human judgments are fully consistent with the automatic pipeline judgments across all methods, datasets, and criteria\. In particular, all sampled RePro\-retained instances are confirmed to be well\-defined, feasible, and paired with correct reference answers\. For baseline methods, the human validation also confirms the invalid problems and incorrect reference answers identified by the automatic reliability evaluation\.

MethodDataset\#CheckedWell\-defined AgreementFeasibility AgreementCorrectness AgreementAuto\-DatasetGSM8K100100\.00100\.00100\.00Auto\-DatasetMATH500100\.00100\.00100\.00ITDGSM8K100100\.00100\.00100\.00ITDMATH500100\.00100\.00100\.00VarBenchGSM8K100100\.00100\.00100\.00VarBenchMATH500100\.00100\.00100\.00ReProGSM8K100100\.00100\.00100\.00ReProMATH500100\.00100\.00100\.00TotalAll2400100\.00100\.00100\.00Table 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\.
## Appendix IConfound Analysis for Rewriting Sensitivity

This section further analyzes possible factors behind performance changes after proof\-verified rewriting\. The goal is not to prove data contamination, but to examine whether these changes can be explained by simpler rewriting\-induced factors, such as problem length change, surface\-form change, numeric changes, solution complexity, and proof complexity\. Direct evidence of data contamination would require overlap analysis against model training data or external corpora, which is beyond the scope of this work\.

##### Data and unit of analysis\.

We conduct the analysis on the RePro\-retained MATH evaluation set\. Each retained instance contains an original problem, a proof\-verified rewritten problem, and a corresponding Lean proof\. For instanceiiand modelmm, we define correctness on the original and rewritten problems as

ci,mo​r​i,ci,mr​e​w∈\{0,1\},c\_\{i,m\}^\{ori\},c\_\{i,m\}^\{rew\}\\in\\\{0,1\\\},where 1 denotes a correct answer and 0 denotes an incorrect answer\. The accuracy drop for this model\-instance pair is defined as

di,m=ci,mo​r​i−ci,mr​e​w\.d\_\{i,m\}=c\_\{i,m\}^\{ori\}\-c\_\{i,m\}^\{rew\}\.Thus,di,m=1d\_\{i,m\}=1means that the model answers the original problem correctly but fails on the rewritten problem, whiledi,m=−1d\_\{i,m\}=\-1means the opposite\. To analyze instance\-level confounds, we compute the average drop across evaluated models:

d¯i=1M​∑m=1Mdi,m\.\\bar\{d\}\_\{i\}=\\frac\{1\}\{M\}\\sum\_\{m=1\}^\{M\}d\_\{i,m\}\.

##### Overall observation\.

The results show a bidirectional pattern\. Many models exhibit accuracy drops after rewriting, while some models improve on certain rewritten instances\. This indicates that proof\-verified rewriting does not produce a one\-directional effect\. Instead, it changes the evaluation distribution in multiple ways and should be analyzed as model\-specific sensitivity to benchmark reformulation\.

##### Confound metrics\.

For each original–rewritten pair, we compute several potential confound metrics\. Problem length change measures whether the rewritten problem becomes longer or shorter than the original problem\. We tokenize each problem statement and define

Δ​Lq​\(i\)=log⁡Lqr​e​w​\(i\)\+1Lqo​r​i​\(i\)\+1,\\Delta L\_\{q\}\(i\)=\\log\\frac\{L\_\{q\}^\{rew\}\(i\)\+1\}\{L\_\{q\}^\{ori\}\(i\)\+1\},whereLqo​r​i​\(i\)L\_\{q\}^\{ori\}\(i\)andLqr​e​w​\(i\)L\_\{q\}^\{rew\}\(i\)denote the token lengths of the original and rewritten problems\. We also consider\|Δ​Lq​\(i\)\|\|\\Delta L\_\{q\}\(i\)\|, which measures the magnitude of length change regardless of direction\.

Surface\-form distance measures how much the rewritten problem differs from the original at the string level[Zhou et al\. \(2024\)](https://arxiv.org/html/2609.00062#bib.bib39)\. We lowercase both problem statements, collapse whitespace, and compute

Ds​u​r​f​\(i\)=1−sim⁡\(qio​r​i,qir​e​w\),D\_\{surf\}\(i\)=1\-\\mathrm\{sim\}\(q\_\{i\}^\{ori\},q\_\{i\}^\{rew\}\),wheresim\\mathrm\{sim\}is the normalized sequence\-matching similarity score\. Larger values indicate greater surface\-form divergence\.

Numeric\-range change measures whether rewriting changes the numerical scale of the problem[Yang et al\. \(2025b\)](https://arxiv.org/html/2609.00062#bib.bib40)\. LetAo​r​i​\(i\)A^\{ori\}\(i\)andAr​e​w​\(i\)A^\{rew\}\(i\)be the maximum absolute numeric values in the original and rewritten problem, respectively\. We define

Δ​A​\(i\)=log⁡\(1\+Ar​e​w​\(i\)\)−log⁡\(1\+Ao​r​i​\(i\)\)\.\\Delta A\(i\)=\\log\(1\+A^\{rew\}\(i\)\)\-\\log\(1\+A^\{ori\}\(i\)\)\.We also consider\|Δ​A​\(i\)\|\|\\Delta A\(i\)\|\. Numeric\-count change measures whether rewriting introduces more or fewer numeric quantities:

Δ​N​\(i\)=Nr​e​w​\(i\)−No​r​i​\(i\),\\Delta N\(i\)=N^\{rew\}\(i\)\-N^\{ori\}\(i\),whereNo​r​i​\(i\)N^\{ori\}\(i\)andNr​e​w​\(i\)N^\{rew\}\(i\)denote the numbers of numeric literals in the original and rewritten problems\.

Solution\-length change is used as a proxy for natural\-language solution complexity[Wei et al\. \(2022\)](https://arxiv.org/html/2609.00062#bib.bib38)\. LetLso​r​i​\(i\)L\_\{s\}^\{ori\}\(i\)andLsr​e​w​\(i\)L\_\{s\}^\{rew\}\(i\)denote the token lengths of the original and rewritten solutions\. We define

Δ​Ls​\(i\)=log⁡Lsr​e​w​\(i\)\+1Lso​r​i​\(i\)\+1\.\\Delta L\_\{s\}\(i\)=\\log\\frac\{L\_\{s\}^\{rew\}\(i\)\+1\}\{L\_\{s\}^\{ori\}\(i\)\+1\}\.We also report the rewritten solution length:

Lsr​e​w,l​o​g​\(i\)=log⁡\(1\+Lsr​e​w​\(i\)\)\.L\_\{s\}^\{rew,log\}\(i\)=\\log\(1\+L\_\{s\}^\{rew\}\(i\)\)\.Finally, Lean proof length is used as a lightweight proxy for formal proof complexity[Zheng et al\. \(2021\)](https://arxiv.org/html/2609.00062#bib.bib29)\. LetLp​\(i\)L\_\{p\}\(i\)be the token length of the verified Lean proof\. We define

Lpl​o​g​\(i\)=log⁡\(1\+Lp​\(i\)\)\.L\_\{p\}^\{log\}\(i\)=\\log\(1\+L\_\{p\}\(i\)\)\.

##### Correlation analysis\.

Since length, numeric values, and proof lengths can be heavy\-tailed, we use Spearman correlation rather than Pearson correlation[Spearman \(1904\)](https://arxiv.org/html/2609.00062#bib.bib37)\. For each confound metric, we compute its correlation with the model\-averaged accuracy dropd¯i\\bar\{d\}\_\{i\}\. Table[4](https://arxiv.org/html/2609.00062#A9.T4)reports the results\.

Confound metricSpearmanρ\\rhowith accuracy dropProblem length change\-0\.000Absolute problem length change\-0\.031Surface\-form distance\-0\.031Numeric\-range change0\.014Absolute numeric\-range change0\.002Numeric\-count change\-0\.021Absolute numeric\-count change\-0\.032Solution\-length change0\.101Absolute solution\-length change0\.099Lean proof length0\.135Rewritten solution length0\.173Table 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\.The surface\-level metrics have correlations close to zero\. Problem length change, absolute problem length change, and surface\-form distance are not meaningfully associated with accuracy drop\. This suggests that the observed drops are not primarily explained by rewritten problems being longer or more surface\-dissimilar\.

The numeric metrics also have near\-zero correlations\. Numeric\-range change, absolute numeric\-range change, numeric\-count change, and absolute numeric\-count change are weakly associated with accuracy drop\. This suggests that the observed drops are not mainly driven by larger numbers, changed numerical ranges, or increased numbers of numeric quantities\.

In contrast, complexity\-related metrics show weak positive correlations\. Solution\-length change, rewritten solution length, and Lean proof length are positively associated with accuracy drop\. This indicates that some rewritten problems may become harder because they require longer solutions or more complex formal proofs\. Therefore, solution and proof complexity remain plausible contributing factors\.

##### Improvement cases\.

To better understand why some models achieve higher accuracy on the rewritten benchmark, we manually inspect representative improvement cases from Level 4, where models are more likely to answer correctly after rewriting\. These examples suggest that such improvements are not necessarily caused by reduced mathematical difficulty\. Instead, they often arise because rewriting makes the target quantity, condition structure, or information flow easier to parse\.

Example 1: Target Quantity ClarificationOriginal problem\.What value ofxxwill give the maximum value for−x2−6​x\+12\-x^\{2\}\-6x\+12?Original answer:−3\-3Rewritten problem\.For what value ofxxdoes the expression−2​x2\+16​x−5\-2x^\{2\}\+16x\-5attain its maximum value?Rewritten answer:44Interpretation\.The original wording may confuse the target: some models may output the maximum function value instead of thexx\-value that gives the maximum\. The rewrite states the target more directly\. This reflects target\-identification sensitivity, not lower mathematical difficulty\.

Example 2: Explicit Condition PhrasingOriginal problem\.For specific positive numbersmmandnn, the quadratics16​x2\+36​x\+5616x^\{2\}\+36x\+56and\(m​x\+n\)2\(mx\+n\)^\{2\}differ only in their constant term\. What ism​nmn?Original answer:1818Rewritten problem\.For certain positive integersppandqq, the quadratic expressions81​x2\+108​x\+6481x^\{2\}\+108x\+64and\(p​x\+q\)2\(px\+q\)^\{2\}have identical coefficients forx2x^\{2\}andxx, but their constant terms are not equal\. Computep​qpq\.Rewritten answer:5454Interpretation\.Both problems require the same algebra step: expand the square, match thex2x^\{2\}andxxcoefficients, and compute the product\. The original phrase “differ only in their constant term” requires the model to infer which coefficients should be matched\. The rewrite states this directly by saying that thex2x^\{2\}andxxcoefficients are identical\. This makes the condition clearer without making the algebra easier\.

Example 3: Condition Tracking ClarificationOriginal problem\.Annie is located at\(3,5\)\(3,5\)and Barbara says she is located at\(−6,2\)\(\-6,2\)\. They agree to meet at the midpoint of their current locations\. However, Barbara read the map wrong and is actually at\(−10,4\)\(\-10,4\)\. What is the positive difference in thexx\-coordinates of where they agreed to meet and where they should actually meet?Original answer:22Rewritten problem\.Annie is at\(−2,7\)\(\-2,7\), and Carlos initially reports his location as\(4,−1\)\(4,\-1\)\. Based on this, they decide on a meeting point\. Later, Carlos realizes he is actually at\(6,−5\)\(6,\-5\)\. What is the absolute difference between thexx\-coordinates of the originally planned meeting point and the correct meeting point?Rewritten answer:11Interpretation\.Both problems require computing two midpoints and comparing theirxx\-coordinates\. In the original problem, the model must infer that “where they agreed to meet” means the midpoint based on the reported location, and “where they should actually meet” means the midpoint based on the corrected location\. The rewrite names these two quantities directly as the “originally planned meeting point” and the “correct meeting point”, making the target clearer\.

##### Interpretation\.

Overall, this analysis supports a cautious interpretation of the rewriting results\. Simple problem length changes, surface\-form differences, and numeric changes do not fully explain the observed performance drops\. However, solution and proof complexity show weak positive associations with drops, meaning that increased reasoning complexity remains a plausible confound\.

Therefore, performance changes after proof\-verified rewriting are better interpreted as a reliability\-controlled diagnostic of model sensitivity to benchmark reformulation\. Accuracy drops may suggest potential memorization or benchmark\-specific pattern reliance, while improvements may reflect reduced incidental difficulty or clearer problem specification\. Direct claims about data contamination require additional overlap analysis against model training data or external corpora\.

## Appendix JAnalysis of Failure Cases in DeepSeek\-Prover\-V2\-7B

This section presents representative failure cases observed in the Lean proofs generated by DeepSeek\-Prover\-V2\-7B\. These cases illustrate several failure patterns that may contribute to the gap between the prover’s reported benchmark capability and its performance in our rewriting pipeline\.

Example 4: Inappropriate Tactic SelectionThe generated proof fails to select tactics appropriate for the current goal\. In particular, it repeatedly applies generic arithmetic tactics that do not establish the required polynomial identity over the reals\.QuestionSimplify the expression\(x\+5\)​\(x−4\)−x⁡\(x−1\)\(x\+5\)\(x\-4\)\-x\(x\-1\)\.Failed Proof[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKaW1wb3J0IEFlc29wCgpzZXRfb3B0aW9uIG1heEhlYXJ0YmVhdHMgMjAwMDAwCgpvcGVuIHNjb3BlZCBCaWdPcGVyYXRvcnMKb3BlbiBCaWdPcGVyYXRvcnMgUmVhbCBOYXQgVG9wb2xvZ3kgUmF0Cgp0aGVvcmVtIHNpbXBsaWZ5X2V4cHIgKHggOiBSZWFsKSA6CiAgKHggKyA1KSAqICh4IC0gNCkgLSB4ICogKHggLSAxKSA9IDIgKiB4IC0gMjAgOj0gYnkKICBub3JtX251bQogIDw7PiBvbWVnYQogIDw7PiBvbWVnYQogIDw7PiBvbWVnYQogIDw7PiBvbWVnYQogIDw7PiBvbWVnYQotLSBvbWl0dGVkIChvdmVyIDEwMCBsaW5lcyk=)1importMathlib2importAesop34set\_optionmaxHeartbeats20000056openscopedBigOperators7openBigOperatorsRealNatTopologyRat89theoremsimplify\_expr\(x:Real\):10\(x\+5\)\*\(x\-4\)\-x\*\(x\-1\)=2\*x\-20:=by11norm\_num12<;\>omega13<;\>omega14<;\>omega15<;\>omega16<;\>omega17\-\-omitted\(over100lines\)

In this example, the theorem statement is mathematically correct, but the generated proof does not use an appropriate algebraic normalization tactic such asringorring\_nf\. Instead, it repeatedly appliesnorm\_numandomega, which do not resolve the symbolic polynomial identity overReal\. We observe similar failure patterns in which the prover falls back to generic tactics such asnorm\_num,omega,rfl, ordecidewithout making goal\-directed progress\. These cases suggest that the prover does not always adapt its tactic selection to the current proof state and may instead revert to frequently generated arithmetic proof patterns\.

Example 5: Semantic Drift in Theorem StatementThe generated theorem does not match the intended problem semantics, leading to proof attempts for an incorrect or irrelevant goal\.QuestionA landlord leases a house to four tenants, each paying $350 monthly\. The landlord pays $1,100 per month in mortgage and maintenance fees for the property\. Calculate the landlord’s annual net loss or profit\.Formal Statement[⬇](data:text/plain;base64,dGhlb3JlbSBsYW5kbG9yZF9wcm9maXQgOgogIGxldCBudW1fdGVuYW50cyA6IE5hdCA6PSA0CiAgbGV0IG1vbnRobHlfcmVudF9wZXJfdGVuYW50IDogTmF0IDo9IDM1MAogIGxldCBtb250aGx5X2V4cGVuc2VzIDogTmF0IDo9IDExMDAKICBsZXQgbW9udGhseV9pbmNvbWUgOj0gbnVtX3RlbmFudHMgKiBtb250aGx5X3JlbnRfcGVyX3RlbmFudAogIGxldCBtb250aGx5X3Byb2ZpdCA6PSBtb250aGx5X2luY29tZSAtIG1vbnRobHlfZXhwZW5zZXMKICBsZXQgYW5udWFsX3Byb2ZpdCA6PSBtb250aGx5X3Byb2ZpdCAqIDEyCiAgYW5udWFsX3Byb2ZpdCA9IDM2MDA=)1theoremlandlord\_profit:2letnum\_tenants:Nat:=43letmonthly\_rent\_per\_tenant:Nat:=3504letmonthly\_expenses:Nat:=11005letmonthly\_income:=num\_tenants\*monthly\_rent\_per\_tenant6letmonthly\_profit:=monthly\_income\-monthly\_expenses7letannual\_profit:=monthly\_profit\*128annual\_profit=3600Failed Proof[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKaW1wb3J0IEFlc29wCgpzZXRfb3B0aW9uIG1heEhlYXJ0YmVhdHMgMjAwMDAwCgpvcGVuIHNjb3BlZCBCaWdPcGVyYXRvcnMKb3BlbiBCaWdPcGVyYXRvcnMgUmVhbCBOYXQgVG9wb2xvZ3kgUmF0Cgp0aGVvcmVtIGxhbmRsb3JkX3Byb2ZpdCA6CiAgbGV0IG51bV90ZW5hbnRzIDogTmF0IDo9IDQKICBsZXQgbW9udGhseV9yZW50X3Blcl90ZW5hbnQgOiBOYXQgOj0gMzUwCiAgbGV0IG1vbnRobHlfZXhwZW5zZXMgOiBOYXQgOj0gMTEwMAogIGxldCBtb250aGx5X2luY29tZSA6PSBudW1fdGVuYW50cyAqIG1vbnRobHlfcmVudF9wZXJfdGVuYW50CiAgbGV0IG1vbnRobHlfcHJvZml0IDo9IG1vbnRobHlfaW5jb21lIC0gbW9udGhseV9leHBlbnNlcwogIGxldCBhbm51YWxfcHJvZml0IDo9IG1vbnRobHlfcHJvZml0ICogMTIKICBhbm51YWxfcHJvZml0ID0gMzYwMCAvIDEyIDo9IGJ5CiAgbm9ybV9udW0gW211bF9jb21tLCBtdWxfYXNzb2MsIG11bF9sZWZ0X2NvbW1dCiAgPDs+IHJmbAogIDw7PiBkZWNpZGUKICA8Oz4gZGVjaWRlCiAgPDs+IGRlY2lkZQogIDw7PiBkZWNpZGUKICA8Oz4gZGVjaWRlCi0tIG9taXR0ZWQgKG92ZXIgMTAwIGxpbmVzKQ==)1importMathlib2importAesop34set\_optionmaxHeartbeats20000056openscopedBigOperators7openBigOperatorsRealNatTopologyRat89theoremlandlord\_profit:10letnum\_tenants:Nat:=411letmonthly\_rent\_per\_tenant:Nat:=35012letmonthly\_expenses:Nat:=110013letmonthly\_income:=num\_tenants\*monthly\_rent\_per\_tenant14letmonthly\_profit:=monthly\_income\-monthly\_expenses15letannual\_profit:=monthly\_profit\*1216annual\_profit=3600/12:=by17norm\_num\[mul\_comm,mul\_assoc,mul\_left\_comm\]18<;\>rfl19<;\>decide20<;\>decide21<;\>decide22<;\>decide23<;\>decide24\-\-omitted\(over100lines\)

As illustrated above, this type of failure indicates that this ATP does not consistently maintain semantic stability during proof generation\. Even when the generated statement is syntactically well\-formed, this ATP does not reliably condition its tactic selection on the actual goal, and may instead fall back to frequently observed proof patterns\. This behavior suggests that the limitation lies in the capability of this ATP, which cannot always preserve a consistent reasoning context throughout the proof\.

Example 6: Output Boundary CorruptionThe generated Lean code is corrupted by unexpected special tokens \(e\.g\.,<\|Assistant\|\>\), which break the theorem header or proposition syntax\.QuestionWhat is the value of\(13\+3\)2−\(13−3\)2\(13\+3\)^\{2\}\-\(13\-3\)^\{2\}?Failed Proof[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKaW1wb3J0IEFlc29wCgpzZXRfb3B0aW9uIG1heEhlYXJ0YmVhdHMgMjAwMDAwCgpvcGVuIHNjb3BlZCBCaWdPcGVyYXRvcnMKb3BlbiBCaWdPcGVyYXRvcnMgUmVhbCBOYXQgVG9wb2xvZ3kgUmF0Cgp0aGVvcmVtIHByb2JsZW0gOiAoMTMgKyAzKV4yIC0gKDEzIC0gMyleMiA9IDE1Njx8QXNzaXN0YW50fD4zIDo9IGJ5CiAgbm9ybV9udW0KICA8Oz4gcmZsCiAgPDs+IG5vcm1fbnVtCiAgPDs+IHJmbAogIDw7PiBub3JtX251bQogIDw7PiByZmw=)1importMathlib2importAesop34set\_optionmaxHeartbeats20000056openscopedBigOperators7openBigOperatorsRealNatTopologyRat89theoremproblem:\(13\+3\)^2\-\(13\-3\)^2=156<\|Assistant\|\>3:=by10norm\_num11<;\>rfl12<;\>norm\_num13<;\>rfl14<;\>norm\_num15<;\>rfl

This is the most frequent and dominant failure pattern in our experiments, accounting for more than 94% of the unsuccessful proofs\. In contrast, such corruption is rarely observed in the samples that pass verification, indicating that the primary difficulty for this ATP is not mathematical reasoning, but the ability to maintain stable output boundaries during generation\.

In this example, the correct statement should end with= 156 := by, while the additional token3appears after a special marker and is not a valid part of the theorem\. Although in this particular case the inserted content can be identified as corruption, it is not possible to define a fully general string\-level rule to repair all such errors\. The tokens following the special marker may vary across samples, including numbers, expressions, natural language text, or even fragments of another theorem\.

Therefore, without analyzing the intended semantics of the proof, these corruptions cannot be safely removed in a uniform way\. In other words, there is no simple and fully reliable post\-processing rule that can clean such outputs without risking unintended modifications\.

Example 7: Natural Language IntrusionThe generated proof contains long natural\-language explanations or comments instead of valid Lean tactics, causing verification failure\.QuestionIn an arithmetic sequence, the 4th term is 23 and the 6th term is 35\. Determine the value of the 8th term\.Failed Proof[⬇](data:text/plain;base64,dGhlb3JlbSBhcml0aG1ldGljX3NlcXVlbmNlX3Rlcm0gKGFfMSBkIDogUikgOgogIChhXzEgKyAzICogZCA9IDIzKSAtPgogIChhXzEgKyA1ICogZCA9IDM1KSAtPgogIChhXzEgKyA3ICogZCA9IDQ3KTx8QXNzaXN0YW50fD4hIChhXzEgPSAxKSAvXCAoZCA9IDcpIDo9IGJ5CiAgaW50cm8gaF8xIGhfMgogIGhhdmUgaF8zIDogYV8xID0gMSA6PSBieQogICAgLS0gV2UgbmVlZCB0byBzb2x2ZSBmb3IgYV8xIHVzaW5nIHRoZSBnaXZlbiBlcXVhdGlvbnMuCiAgICAtLSBGcm9tIHRoZSBmaXJzdCBlcXVhdGlvbjogYV8xICsgM2QgPSAyMwogICAgLS0gRnJvbSB0aGUgc2Vjb25kIGVxdWF0aW9uOiBhXzEgKyA1ZCA9IDM1CiAgICAtLSBTdWJ0cmFjdCB0aGUgZmlyc3QgZXF1YXRpb24gZnJvbSB0aGUgc2Vjb25kIHRvIGVsaW1pbmF0ZSBhXzE6CiAgICAtLSAoYV8xICsgNWQpIC0gKGFfMSArIDNkKSA9IDM1IC0gMjMKICAgIC0tIFNpbXBsaWZ5aW5nIGdpdmVzOiAyZCA9IDEyID0+IGQgPSA2CiAgICAtLSBTdWJzdGl0dXRlIGQgPSA2IGJhY2sgaW50byB0aGUgZmlyc3QgZXF1YXRpb246CiAgICAtLSBhXzEgKyAzICogNiA9IDIzID0+IGFfMSArIDE4ID0gMjMgPT4gYV8xID0gMjMgLSAxOCA9PiBhXzEgPSA1CiAgICAtLSBIb3dldmVyLCB0aGlzIHNvbHV0aW9uIGRvZXMgbm90IHNhdGlzZnkgdGhlIHRoaXJkIGVxdWF0aW9uOgogICAgLS0gYV8xICsgN2QgPSA0NyA9PiBhXzEgKyA3ICogNiA9IDQ3ID0+IGFfMSArIDQyID0gNDcgPT4gYV8xID0gNQogICAgLS0gVGhpcyBpbmRpY2F0ZXMgYSBtaXN0YWtlIGluIHRoZSBpbml0aWFsIGNhbGN1bGF0aW9uLiBSZWNoZWNraW5nIHRoZSBzdGVwczoKICAgIC0tIEZyb20gdGhlIGZpcnN0IGVxdWF0aW9uOiBhXzEgKyAzZCA9IDIzCiAgICAtLSBGcm9tIHRoZSBzZWNvbmQgZXF1YXRpb246IGFfMSArIDVkID0gMzUKICAgIC0tIFN1YnRyYWN0IHRoZSBmaXJzdCBlcXVhdGlvbiBmcm9tIHRoZSBzZWNvbmQ6CiAgICAtLSAyZCA9IDEyID0+IGQgPSA2CiAgICAtLSBTdWJzdGl0dXRlIGQgPSA2IGJhY2sgaW50byB0aGUgZmlyc3QgZXF1YXRpb246CiAgICAtLSBhXzEgKyAzICogNiA9IDIzID0+IGFfMSArIDE4ID0gMjMgPT4gYV8xID0gMjMgLSAxOCA9PiBhXzEgPSA1CiAgICAtLSBUaGlzIGRvZXMgbm90IHNhdGlzZnkgdGhlIHRoaXJkIGVxdWF0aW9uLCBpbmRpY2F0aW5nIGEgbWlzdGFrZS4KICAgIC0tIFJlY2hlY2tpbmcgdGhlIGluaXRpYWwgY29uZGl0aW9ucyBhbmQgY2FsY3VsYXRpb25zLCB3ZSBmaW5kIHRoYXQgdGhlIGNvcnJlY3Qgc29sdXRpb24gaXM6CiAgICAtLSBhXzEgPSAxIGFuZCBkID0gNwogICAgbGluYXJpdGgKICBoYXZlIGhfNCA6IGQgPSA3IDo9IGJ5CiAgICAtLSBTdWJzdGl0dXRlIGFfMSA9IDEgaW50byB0aGUgZmlyc3QgZXF1YXRpb246CiAgICAtLSAxICsgM2QgPSAyMyA9PiAzZCA9IDIyID0+IGQgPSAyMiAvIDMKICAgIC0tIFN1YnN0aXR1dGUgYV8xID0gMSBpbnRvIHRoZSBzZWNvbmQgZXF1YXRpb246CiAgICAtLSAxICsgNWQgPSAzNSA9PiA1ZCA9IDM0ID0+IGQgPSAzNCAvIDUKICAgIC0tIFN1YnN0aXR1dGUgYV8xID0gMSBpbnRvIHRoZSB0aGlyZCBlcXVhdGlvbjoKICAgIC0tIDEgKyA3ZCA9IDQ3ID0+IDdkID0gNDYgPT4gZCA9IDQ2IC8gNwogICAgLS0gVGhlIGNvbnNpc3RlbnQgdmFsdWUgZm9yIGQgaXMgZCA9IDcKICAgIGxpbmFyaXRoCiAgZXhhY3QgQW5kLmludHJvIGhfMyBoXzQ=)1theoremarithmetic\_sequence\_term\(a\_1d:R\):2\(a\_1\+3\*d=23\)\-\>3\(a\_1\+5\*d=35\)\-\>4\(a\_1\+7\*d=47\)<\|Assistant\|\>\!\(a\_1=1\)/\\\(d=7\):=by5introh\_1h\_26haveh\_3:a\_1=1:=by7\-\-Weneedtosolvefora\_1usingthegivenequations\.8\-\-Fromthefirstequation:a\_1\+3d=239\-\-Fromthesecondequation:a\_1\+5d=3510\-\-Subtractthefirstequationfromthesecondtoeliminatea\_1:11\-\-\(a\_1\+5d\)\-\(a\_1\+3d\)=35\-2312\-\-Simplifyinggives:2d=12=\>d=613\-\-Substituted=6backintothefirstequation:14\-\-a\_1\+3\*6=23=\>a\_1\+18=23=\>a\_1=23\-18=\>a\_1=515\-\-However,thissolutiondoesnotsatisfythethirdequation:16\-\-a\_1\+7d=47=\>a\_1\+7\*6=47=\>a\_1\+42=47=\>a\_1=517\-\-Thisindicatesamistakeintheinitialcalculation\.Recheckingthesteps:18\-\-Fromthefirstequation:a\_1\+3d=2319\-\-Fromthesecondequation:a\_1\+5d=3520\-\-Subtractthefirstequationfromthesecond:21\-\-2d=12=\>d=622\-\-Substituted=6backintothefirstequation:23\-\-a\_1\+3\*6=23=\>a\_1\+18=23=\>a\_1=23\-18=\>a\_1=524\-\-Thisdoesnotsatisfythethirdequation,indicatingamistake\.25\-\-Recheckingtheinitialconditionsandcalculations,wefindthatthecorrectsolutionis:26\-\-a\_1=1andd=727linarith28haveh\_4:d=7:=by29\-\-Substitutea\_1=1intothefirstequation:30\-\-1\+3d=23=\>3d=22=\>d=22/331\-\-Substitutea\_1=1intothesecondequation:32\-\-1\+5d=35=\>5d=34=\>d=34/533\-\-Substitutea\_1=1intothethirdequation:34\-\-1\+7d=47=\>7d=46=\>d=46/735\-\-Theconsistentvaluefordisd=736linarith37exactAnd\.introh\_3h\_4

The presence of natural\-language comments in the preceding example does not by itself cause verification failure, since comments are valid Lean syntax\. Rather, the failure arises when substantial portions of the generation are devoted to natural\-language reasoning while the actual Lean proof remains incomplete\. In such cases, the available generation budget may be consumed without producing a complete proof script, resulting in truncated or only partially formed proofs\.

Example 8: Target Corruption and Repetitive Tactic GenerationSome failed generations exhibit both instability in the theorem target and excessive repetition of generic tactics\. Once the generated target deviates from the intended statement, the prover may continue producing repetitive tactics without making meaningful progress toward a valid proof\.QuestionEvaluate35−\(3​a−b\)35\-\(3a\-b\)given thata=5a=5andb=7b=7\.Failed Proof[⬇](data:text/plain;base64,aW1wb3J0IE1hdGhsaWIKaW1wb3J0IEFlc29wCgpzZXRfb3B0aW9uIG1heEhlYXJ0YmVhdHMgMjAwMDAwCgpvcGVuIHNjb3BlZCBCaWdPcGVyYXRvcnMKb3BlbiBCaWdPcGVyYXRvcnMgUmVhbCBOYXQgVG9wb2xvZ3kgUmF0Cgp0aGVvcmVtIGV2YWx1YXRlX2V4cHJlc3Npb24gOgogIGxldCBhIDo9IDUKICBsZXQgYiA6PSA3CiAgMzUgLSAoMyAqIGEgLSBiKSA9IDI3IC8gMjcgOj0gYnkKICBsZXQgYSA6PSA1CiAgbGV0IGIgOj0gNwogIG5vcm1fbnVtCiAgPDs+IHNpbXBfYWxsCiAgPDs+IG5vcm1fbnVtCiAgPDs+IG9tZWdhCiAgPDs+IG9tZWdhCiAgPDs+IG9tZWdhCiAgPDs+IG9tZWdhCiAgPDs+IG9tZWdhCi0tIG9taXR0ZWQgKG92ZXIgMTAwIGxpbmVzKQ==)1importMathlib2importAesop34set\_optionmaxHeartbeats20000056openscopedBigOperators7openBigOperatorsRealNatTopologyRat89theoremevaluate\_expression:10leta:=511letb:=71235\-\(3\*a\-b\)=27/27:=by13leta:=514letb:=715norm\_num16<;\>simp\_all17<;\>norm\_num18<;\>omega19<;\>omega20<;\>omega21<;\>omega22<;\>omega23\-\-omitted\(over100lines\)

In this example, the intended answer is2727, whereas the generated theorem target contains27 / 27\. Thus, the failure already involves corruption of the target statement\. The subsequent proof generation further exhibits repetitive use of generic tactics such asnorm\_num,simp\_all, andomega, without recovering a valid proof\. This combination suggests that once generation deviates from the intended proof state, the prover may fall back to frequently occurring arithmetic tactic patterns rather than maintaining goal\-directed reasoning\.

This behavior is also prominent more generally: approximately 39% of the failed proofs contain excessive repetition of the same tactic, with individual tactics appearing dozens of times in some outputs\. Such repetition does not necessarily indicate progress toward completing the proof\. Instead, it is often associated with unstable or mechanical generation in which the prover repeatedly emits common closing tactics without resolving the current goal\.

We also observe outputs that terminate with incomplete tactic sequences, such as a trailing<;, or with partially generated tokens\. These cases are consistent with truncation or decoding instability, potentially exacerbated by output\-length limits\. Taken together, these failure patterns indicate that DeepSeek\-Prover\-V2\-7B may occasionally lose consistency with the intended proof state during generation, leading to corrupted targets, repetitive tactic sequences, or incomplete proof scripts that fail Lean verification\.

## Appendix KCandidate\-Level Failure Modes in VarBench Generation

VarBench generates new benchmark instances by extracting variables, constructing parameterized problems, and synthesizing executable solution functions\. To better understand the reliability issues that may arise during this generation process, we analyze representative candidate\-level failure modes observed in our implementation\. These examples are not intended to imply that every failed candidate passes all subsequent validation steps\. Rather, they illustrate why format or execution checks alone are insufficient to establish problem validity and answer correctness\.

We identify three representative failure modes: invalid or non\-executable generated programs, executable programs with incorrect outputs, and implicit constraint violations in generated problems\.

### K\.1Invalid or Non\-executable Generated Programs

Some generated solution functions are syntactically structured as valid programs but cannot be executed successfully because they contain undefined variables, invalid operations, or incompatible mathematical domains\.

Example 9: Invalid or Non\-executable Generated Programs[⬇](data:text/plain;base64,IyMjIFZhcmlhYmxlcwp4ID0gMgoKIyMjIEZ1bmN0aW9uCmRlZiBzb2x1dGlvbih4KToKICAgIHJldHVybiB4ICsgeSAgICMgeSBpcyB1bmRlZmluZWQKCltSdW50aW1lIEVycm9yXQpOYW1lRXJyb3I6IG5hbWUgJ3knIGlzIG5vdCBkZWZpbmVk)12x=2345defsolution\(x\):6returnx\+y78\[RuntimeError\]9NameError:name'y'isnotdefinedOr:[⬇](data:text/plain;base64,ZGVmIHNvbHV0aW9uKHgpOgogICAgcmV0dXJuIHNxcnQoLTEpCgpbUnVudGltZSBFcnJvcl0KVmFsdWVFcnJvcjogbWF0aCBkb21haW4gZXJyb3I=)1defsolution\(x\):2returnsqrt\(\-1\)34\[RuntimeError\]5ValueError:mathdomainerror

These examples fail during execution and can therefore be detected by a runtime check\. Nevertheless, they illustrate that producing a well\-formatted solution function does not by itself guarantee that the generated computation is executable or mathematically well\-defined\. Such failures reflect instability in the generation stage and motivate additional validation beyond surface\-level format checking\.

### K\.2Incorrect Candidate Answers despite Successful Execution

A different failure mode occurs when the generated solution function executes successfully but produces an incorrect output\. Unlike runtime errors, these failures cannot be identified from executability alone\.

Example 10: Incorrect Candidate Answer despite Successful Execution[⬇](data:text/plain;base64,IyMjIFZhcmlhYmxlcwp4ID0gNAoKIyMjIEZ1bmN0aW9uCmRlZiBzb2x1dGlvbih4KToKICAgIHJldHVybiB4ICogMgoKW1ZlcmlmaWNhdGlvbl0KRXhwZWN0ZWQgYW5zd2VyOiAxMApGdW5jdGlvbiBvdXRwdXQ6IDgKCnZlcmlmeV9jOiBGYWxzZQ==)12x=4345defsolution\(x\):6returnx\*278\[Verification\]9Expectedanswer:1010Functionoutput:81112verify\_c:False

Here, the function executes normally but returns an answer that does not match the expected result\. The subsequent verification step correctly identifies this mismatch throughverify\_c: False\. This example therefore highlights an important distinction: successful execution establishes only that a program can run, not that its output is mathematically correct\. Reliable benchmark construction consequently requires an additional answer\-validation mechanism beyond execution testing\.

### K\.3Implicit Constraint Violations

Generated problems may also violate implicit real\-world or task\-specific constraints while remaining syntactically valid and computationally executable\. Such errors are semantic rather than programmatic and may therefore evade purely format\- or execution\-based checks\.

Example 11: Implicit Constraint Violation[⬇](data:text/plain;base64,IyMjIFByb2JsZW0KQSB3ZWVrIGhhcyA4IGRheXMuIElmIGVhY2ggZGF5IGhhcyAyNCBob3VycywKaG93IG1hbnkgaG91cnMgYXJlIHRoZXJlIGluIGEgd2Vlaz8KCltJc3N1ZV0KSW5jb3JyZWN0IHdvcmxkIGtub3dsZWRnZTogYSB3ZWVrIGhhcyA3IGRheXMKCltSZXN1bHRdClNlbWFudGljYWxseSBpbnZhbGlkIHByb2JsZW0=)12Aweekhas8days\.Ifeachdayhas24hours,3howmanyhoursarethereinaweek?45\[Issue\]6Incorrectworldknowledge:aweekhas7days78\[Result\]9Semanticallyinvalidproblem

In this example, a solution program could still execute and return a numerical value, but the underlying problem is invalid because it violates basic world knowledge\. Such cases cannot necessarily be detected through program execution alone\. They instead require semantic or constraint\-level validation to determine whether the generated problem is valid under its intended interpretation\.

### K\.4Summary

These examples illustrate three complementary candidate\-level failure modes that may arise during automatic benchmark generation: non\-executable programs, executable programs with incorrect outputs, and semantically invalid problems\. Importantly, the examples do not imply that all such candidates survive every downstream validation step\. Rather, they show that format consistency and successful execution alone are insufficient to establish the three reliability dimensions considered in this work:well\-definedness,feasibility, andanswer correctness\.

RePro addresses these dimensions through a layered verification procedure\. Problem validity is screened before formalization, while reference\-answer correctness is established only for retained instances whose formal statements admit Lean\-verified proofs and whose verified answers match the requested targets\. This provides a stronger verification criterion than executability alone while also making the scope of the resulting reliability guarantees explicit\.