EvolProver: Advancing Automated theorem proving by Evolving Formalized Problems via Symmetry and Difficulty

## Abstract

Abstract Large Language Models (LLMs) for formal theorem proving have shown significant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: EvolAST , an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and EvolDomain , which leverages LLMs to address semantic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose EvolDifficulty , which uses carefully designed evolutionary instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data to train EvolProver , a 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state-of-the-art (SOTA) on FormalMATH-Lite with a 53.8% pass@32 rate, surpassing all models of comparable size, including reasoning-based models. It also sets new SOTA records for non-reasoning models on MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32), and Ineq-Comp-Transformed (34.0% pass@32). Ablation studies further confirm our data augmentation pipeline’s effectiveness across multiple benchmarks.

## 1 Introduction

Large Language Models (LLMs) have demonstrated significant potential in mathematical reasoning, sparking a surge of research into their application for formal theorem proving. Formal languages like Lean (Moura & Ullrich, 2021), Coq (Barras et al., 1997), and Isabelle (Paulson, 1994) represent mathematical proofs as rigorous code implementations. This process demands strict syntactic precision and logical soundness, with every proof requiring compiler verification. While this guarantees the absolute reliability of proofs, it also creates a major bottleneck: the extreme scarcity of high-quality training data. Crafting formal proofs requires deep domain expertise and substantial time, a reality that fundamentally conflicts with the data-intensive paradigm of LLMs.

To address the scarcity for data, the research community has explored various data synthesis methods. For instance, DeepSeek-Prover (Xin et al., 2024a) attempts to automatically translate a large number of informal natural language problems into formal statements, using model scoring and a hypothesis rejection mechanism for screening. Goedel-Prover-V2 (Lin et al., 2025) adopts a scaffolded strategy to generate mathematical problems of appropriate difficulty to provide models with more effective learning signals. Meanwhile, STP (Dong & Ma, 2025) constructs two adversarial roles of a conjecturer and a prover that iteratively improve to jointly generate new problems and proofs.

However, a line of work has shown that models trained with such synthesized data still lack generalizability. For example, Zhao et al. (2025a) noted that minor transformations of a problem, such as transforming an inequality of the form $f(x)>g(x)$ to $f(x)+f(y)>g(x)+g(y)$, degrade the performance of LLMs drastically. Furthermore, other studies (Hao et al., 2025; Huang et al., 2025) have revealed that this fragility is not unique to formal reasoning; informal LLMs are also susceptible to minor problem transformations.
Motivated by this, we propose a novel data augmentation pipeline to improve model generalizability by addressing it from two perspectives: symmetry and difficulty.

In mathematics, symmetry means exactly invariance under certain transformations. From the symmetry perspective, the fragility of existing models against minor transformations of problems suggests they fail to learn the underlying symmetry structure of the mathematical problem.
To address this, we introduce two complementary methods targeting syntactic and semantic symmetry.
The first, EvolAST, addresses syntactic symmetry using Abstract Syntax Tree (AST). It parses a formal statement into an AST, applies equivalence transformations using a library of axioms and theorems, and converts the modified tree back into a new statement. This generates semantically identical but syntactically diverse problems. The core strength of EvolAST is its extensibility, as any mathematical equivalence can be encoded as a new transformation rule, allowing for systematic enrichment of the data’s structural diversity.

Our second method, EvolDomain, addresses semantic symmetry, where a theorem can be reinterpreted in different domains while preserving its core logic. EvolDomain uses evolutionary instructions to guide LLMs in translating theorems across mathematical domains, thereby creating novel and diverse problem statements.

Figure: Figure 1: An example of problems evolved by EvolDomain, EvolDifficulty, and EvolAST. A seed formal statement is evolved in parallel by EvolDomain and EvolDifficulty, yielding two new statements. Each of these is then further evolved by EvolAST to generate syntactic variants.
Refer to caption: x1.png

From the difficulty perspective, studies have shown that models trained on data with a narrow difficulty range often fail to generalize (Jiang et al., 2023; Parashar et al., 2025). To mitigate this, we propose EvolDifficulty, a method that uses carefully designed instructions to evolve existing theorems by adjusting their difficulty. This process creates a dataset with a much broader difficulty spectrum, which discourages models from relying on shortcuts or mere memorization.

Combining EvolAST, EvolDomain, and EvolDifficulty, we create a comprehensive data augmentation pipeline. Example problems evolved by our pipeline are provided in [Figure 1](https://arxiv.org/html/2510.00732v1#S1.F1). We apply this pipeline to augment public datasets such as STP (Dong & Ma, 2025) and Deepseek-Prover-V1 (Xin et al., 2024a). By training DeepSeek-Prover-V1.5-Base on this augmented data, we produce our model, EvolProver.
EvolProver achieves state-of-the-art (SOTA) performance on multiple benchmarks. Notably, EvolProver is a non-reasoning (i.e., non-CoT) model, yet it achieves results comparable to, and sometimes surpassing, those of reasoning models. On FormalMATH-Lite (Yu et al., 2025), it sets a new SOTA with a 53.8% pass@32 rate among
models of comparable size, including reasoning models. Furthermore, it establishes new SOTA pass@32 rates for non-reasoning models of comparable size on several benchmarks: 69.8% on MiniF2F-Test (Zheng et al., 2021), 52.2% on Ineq-Comp-Seed (Zhao et al., 2025a), and 34.0% on Ineq-Comp-Transformed (Zhao et al., 2025a). Ablation studies confirm the efficacy of our pipeline, showing that EvolProver outperforms its counterparts trained on unaugmented or partially augmented data, in some cases by over 10 percentage points.

The main contributions of this work can be summarized as follows:

- •
We propose a novel data augmentation pipeline that improves model generalizability by systematically enhancing formalized data directly from both symmetry and difficulty perspectives.
- •
We propose EvolAST, a highly extensible, AST-based method that generates syntactically diverse yet semantically equivalent problems by leveraging formal axioms and theorems as transformation rules. Additionally, we introduce EvolDomain and EvolDifficulty, two LLM-driven methods that enrich training data by translating problems across domains and evolving their difficulty, respectively.
- •
We train and release EvolProver, a powerful non-reasoning theorem prover built on our augmented data. EvolProver achieves state-of-the-art performance across multiple benchmarks, outperforming all comparable models on FormalMATH-Lite and setting new records for non-reasoning models on others.

## 2 Related Works

##### Formal Provers.

Numerous LLM-based formal provers(Ji et al., 2025; Zhang et al., 2025; Shang et al., 2025) have emerged after the advent of ChatGPT, including reasoning-based models like DeepSeek-Prover-V2 (Ren et al., 2025), non-reasoning models like STP (Dong & Ma, 2025), and tree-search models like BFS-Prover (Xin et al., 2025). Our work focuses on advancing the state-of-the-art for non-reasoning models, which offer significant computational efficiency.

Data Augmentation in Mathematical Reasoning.
The critical need for large-scale, high-quality training data has spurred significant research into automated methods for mathematical problem generation. Prominent approaches in informal mathematics include MetaMath (Yu et al., 2024), which bootstraps new data by rewriting existing questions from multiple perspectives like rephrasing and backward reasoning. Similarly, WizardMath (Luo et al., 2025a) adapts the Evol-Instruct framework (Luo et al., 2025b; Xu et al., 2024) to systematically generate problems of varying complexity. Another work, PromptCoT (Zhao et al., 2025b), focuses on synthesizing complex problems by emulating the design process of human experts, grounding the generation in core mathematical concepts and logical structures. Inspired by these methods, we introduce EvolDomain and EvolDifficulty. These methods also utilize LLMs but specifically focus on the evolution of formal mathematical statements to enhance their complexity and domain coverage, thereby increasing the diversity of the training data.

While these approaches expand the range and depth of generated problems, they also expose an inherent weakness of LLM-based evolution: the inevitable introduction of syntactic or semantic errors. To mitigate this issue, we propose EvolAST. EvolAST leverages the programmatic features of the Lean 4 proof assistant to perform rewrites directly at the Abstract Syntax Tree (AST) level. This approach ensures that all generated formal statements are syntactically correct and semantically equivalent, effectively increasing data diversity and precision.

##### Robustness of LLMs in Mathematical Reasoning.

Recent work has highlighted that LLMs lack robustness against small perturbations in mathematical problems, such as variable renaming or adding noise. For instance, the PutnamGAP benchmark (Hao et al., 2025) tests equivalence-preserving variants and shows average accuracy declines of 3-10%. Similarly, MATH-P-Hard (Huang et al., 2025) introduces structural shifts, causing performance drops of 10-25% in models like o1-mini.

While this issue is recognized in informal mathematics, the robustness of LLMs in formal reasoning systems like Lean4 and Coq remains largely underexplored. The Ineq-Comp benchmark (Zhao et al., 2025a) was developed to address this gap by measuring a prover’s performance drop between original problems and their perturbed counterparts.

## 3 Method

Our methodology is centered around a multi-stage data augmentation pipeline, as illustrated in [Figure 2](https://arxiv.org/html/2510.00732v1#S3.F2). First, we leverage LLMs to expand existing formal statements through two evolutionary processes: EvolDomain, for cross-domain translation, and EvolDifficulty, for complexity adjustment. After a rigorous verification stage, we further diversify the data’s syntactic structure using EvolAST, a deterministic AST-based transformation method. Finally, we train our model, EvolProver, on this augmented dataset. The following sections detail each component of this pipeline.

Figure: Figure 2: The workflow of our data augmentation pipeline comprises three phases: EvolDomain and EvolDifficulty, Verification, and EvolAST.
Refer to caption: x2.png

### 3.1 EvolDomain and EvolDifficulty

Proven formal statements, with their inherent semantic and syntactic correctness, serve as ideal seeds for data generation. Our work mainly builds upon two open-source datasets, Deepseek-Prover-V1 and STP-Lean, which often lack natural language descriptions. We therefore evolve these formal statements directly by instructing an LLM to generate new, related theorems.
This approach leverages the logical structure embedded in the formal language itself as a basis for creative generation, bypassing the need for natural language intermediaries.

##### EvolDomain.

EvolDomain leverages an LLM to translate a formal statement into new mathematical domains. This process involves three main steps: 1) abstracting the statement’s logical skeleton, 2) identifying an analogous concept in a target domain, and 3) instantiating a new, concrete proposition based on this analogy.

Formally, let this process be a function $\mathcal{F}$. Given a source statement $S_{i}^{\text{formal}}$ and a target domain $D_{m}$ (selected from a predefined list $\mathcal{L}_{D}=\{D_{1},D_{2},\dots,D_{M}\}$), $\mathcal{F}$ guides an LLM to first extract the statement’s abstract logical skeleton. Based on this skeleton, the model identifies a structurally similar concept in $D_{m}$ and uses it to construct a new proposition. The output is a pair consisting of a natural language description, $\widehat{P}_{i}$, and a new formal statement, $\widehat{S}_{i}^{\text{formal}}$. This can be formally represented as: $\mathcal{F}(S_{i}^{\text{formal}},D_{m})=(\widehat{S}_{i}^{\text{formal}},\widehat{P}_{i}).$

To maximize the exploration of logical connections across domains, our prompt further guides the LLM to simultaneously transfer and instantiate the core logical skeleton into 3 to 5 distinct new domains. Therefore, the final output of a single function call is a set of pairs spanning multiple domains, with each pair containing a new formal statement and its corresponding natural language description. Prompt templates and examples can be found in Appendix [A.3](https://arxiv.org/html/2510.00732v1#A1.SS3).

##### EvolDifficulty.

EvolDifficulty leverages an LLM to adjust a formal statement’s difficulty, thereby creating a dataset with a broad difficulty spectrum. We denote this process by the function $\mathcal{E}$. The process, $\mathcal{E}$, is guided by carefully designed evolution strategies. Based on expert consultation, we designed five core evolution strategies, $\mathcal{S}=\{s_{1},\dots,s_{5}\}$: (1) Adjusting Logical Structure, (2) Adjusting Mathematical Depth, (3) Adjusting Abstraction, (4) Adjusting Constraints, and (5) Adjusting Parameters. Given a formal statement $S_{i}^{\text{formal}}$, the function applies a strategy $s_{k}\in\mathcal{S}$ with an evolution direction $\delta\in\{+1,-1\}$ (for increasing or decreasing difficulty, respectively) to instruct an LLM to generate a new pair of a new formal statement $\widehat{S}_{i}^{\text{formal}}$ and its natural language description $\widehat{P}_{i}$. This can be formally represented as $\mathcal{E}(S_{i}^{\text{formal}},s_{k},\delta)=(\widehat{S}_{i}^{\text{formal}},\widehat{P}_{i}).$

By systematically applying this framework, EvolDifficulty enables fine-grained control over dataset difficulty, generating problems with a smooth gradient that enriches the dataset’s hierarchical structure. Prompt templates and examples can be found in Appendix [A.4](https://arxiv.org/html/2510.00732v1#A1.SS4).

Verification. We employ a stringent two-stage verification pipeline to ensure data quality. First, each generated statement $\widehat{S}i^{\text{formal}}$ is validated for syntactic integrity using the Lean 4 compiler. Statements that fail are given a single LLM-based repair attempt before being discarded. Second, all syntactically valid pairs $(\widehat{S}_{i}^{\text{formal}},\widehat{P}_{i})$ undergo semantic evaluation by an LLM-based judge. The judge assesses three aspects: consistency between the formal and natural language versions, propositional correctness, and difficulty appropriateness. This dual-filter mechanism, combining deterministic compilation with semantic judgment, ensures that only syntactically sound and semantically coherent data populates our final dataset. Prompt templates can be found in Appendix [A.5](https://arxiv.org/html/2510.00732v1#A1.SS5).

### 3.2 EvolAST

EvolAST is founded on the principle that formal language statements, as structured code, can be parsed into Abstract Syntax Tree (AST). This allows us to bypass non-deterministic models and instead apply a deterministic set of rewriting rules based on established axioms and theorems, guaranteeing semantic equivalence.

We formalize this process as a function $\mathcal{A}$. EvolAST implements an extensible set of rewriting rules (currently 7 rules), $\mathcal{R}=\{r_{1},\dots,r_{7}\}$, where each rule $r_{k}$ corresponds to a specific logical equivalence: (1) Hypothesis Reordering, (2) Commutativity, (3) Associativity, (4) Distributivity, (5) De Morgan’s Laws, (6) Operand Swapping for Symmetric Relations, and (7) Dual Relation Conversion. Given an input statement $S_{i}^{\text{formal}}$, the function $\mathcal{A}$ first parses it into an AST. It then recursively traverses the tree, applying any applicable rule $r_{k}\in\mathcal{R}$ at each node with a predefined probability $p$. Finally, the modified AST is recompiled into a new formal statement $\widehat{S}_{i}^{\text{formal}}$. The process can be formally represented as $\mathcal{A}(S_{i}^{\text{formal}},p)=\widehat{S}_{i}^{\text{formal}}.$ We provide an example in Appendix [A.6](https://arxiv.org/html/2510.00732v1#A1.SS6).

Since all transformations are based on strict logical equivalences, EvolAST generates syntactically diverse data while ensuring semantic correctness, thus eliminating the need for further verification. The framework is highly extensible, as any known mathematical or logical equivalence can be encoded as a new rewriting rule.

### 3.3 Training EvolProver

We trained our final model, EvolProver, by fine-tuning DeepSeekProver-V1.5-Base (Xin et al., 2024b) on our augmented dataset. The training process consists of two stages: Supervised Fine-Tuning (SFT) and Reinforcement Learning (RL). Detailed information on dataset curation and training algorithms can be found in Appendix [A.1](https://arxiv.org/html/2510.00732v1#A1.SS1).

For comparison and ablation studies, we also trained several other models. This includes a baseline model, EvolProver-Base, which was trained exclusively on the original, unaugmented public data. We also prepared a series of specialized models for our comprehensive ablation experiments, with details provided in Appendix [A.2](https://arxiv.org/html/2510.00732v1#A1.SS2).

## 4 Experiments

### 4.1 Baselines

Existing formal provers are broadly categorized into three types: non-reasoning, reasoning, and tree-search models.

Non-reasoning models generate proofs end-to-end without an intermediate thought process. Key examples include DeepSeek-Prover-V2 (non-CoT) (Ren et al., 2025), Goedel-Prover-SFT (Lin et al., 2025), and STP (Dong & Ma, 2025).

Reasoning models employ a chain-of-thought process to generate proofs, where the reasoning process is often significantly longer than the final proof. Key examples are DeepSeek-Prover-V2 (CoT) (Ren et al., 2025), Moonshot’s Kimi-Prover-Preview (Wang et al., 2025a) and Kimi-Prover (Wang et al., 2025b), and Goedel-Prover-V2 (Lin et al., 2025). Notably, DeepSeek-Prover-V2 has both a reasoning and a non-reasoning mode.
While generally higher performing, reasoning models demand substantial computational resources due to their chain-of-thought approach (e.g., more than 6000 tokens per proof vs. less than 700 for non-reasoning models). This focus on token efficiency has spurred a recent wave of interest in fast, non-reasoning models, such as Claude 4’s Non-thinking mode (Anthropic, 2025) and Grok-Code-Fast-1 (xAI, 2025).

Tree-search models represent an intermediate proof state as a node in a search tree and use a model to assign heuristic scores to guide the search order. Key examples include BFS-Prover (Xin et al., 2025), DeepSeek-Prover-V1.5 + RMaxTS (Xin et al., 2024b), and InternLM2.5-StepProver (Wu et al., 2024).

For our comparative analysis, we report the performance metrics as published by the original authors to ensure consistency and avoid discrepancies from our own re-evaluations.

### 4.2 Results

FormalMATH (Yu et al., 2025) is a broad dataset of formal theorems. We follow standard practice and evaluate on its 425-problem subset, FormalMATH-Lite, as other problems in the full dataset were used in training. Problems within FormalMATH-Lite were held out and used exclusively for final evaluation.

The results are summarized in [Table 1](https://arxiv.org/html/2510.00732v1#S4.T1). EvolProver achieves a new SOTA of 53.86% among models of comparable size, surpassing the previous best of 51.76%. Notably, our non-reasoning model outperforms top reasoning models like DeepSeek-Prover-V2 and Kimi-Prover-Preview. Furthermore, EvolProver outperforms its baseline, EvolProver-Base, by 9.14 percentage points, demonstrating the significant impact of our data augmentation pipeline.

**Table 1: Comparison with SOTA 7B-size models on the FormalMATH-Lite dataset; $\uparrow$ means increase in absolute performance over the ablation model EvolProver-Base; Average Token Length means the average number of output tokens across the benchmark. We do not report average token length for tree-search models, as this metric is not directly comparable with other model types.**
| Models | Average Token Length | Sample Budget | FormalMATH |
| --- | --- | --- | --- |
| Reasoning Models |  |  |  |
| DeepSeek-Prover-V2(COT) | 4804.6 | 32 | 51.76% |
| Kimina-Prover-Preview | 6097.7 | 32 | 48.94% |
| Tree-Search Models |  |  |  |
| InternLM2.5-StepProver | N/A | 1 $\times$ 3200 | 7.87% |
| BFS-Prover | N/A | 1 $\times$ 3200 | 27.19% |
| Non-Reasoning Models |  |  |  |
| DeepSeek-Prover-V1.5-SFT | 115.9 | 32 | 40.40% |
| DeepSeek-Prover-V1.5-RL | 163.4 | 32 | 47.98% |
| Goedel-Prover-SFT | 458.4 | 32 | 46.70% |
| STP | 186.8 | 32 | 48.59% |
| EvolProver-Base(Ours) | 629.8 | 32 | 44.71% |
| EvolProver(Ours) | 653.7 | 32 | 53.86%($\uparrow$ 9.14%) |

MiniF2F (Zheng et al., 2021) is a standard benchmark comprising 488 problems from mathematics competitions. Following common practice, we report results on its 244-problem test set, MiniF2F-Test. The results are presented in Figure [3](https://arxiv.org/html/2510.00732v1#S4.F3). EvolProver achieves a pass@32 rate of 69.80% on MiniF2F-Test, establishing a new SOTA performance among non-reasoning models of comparable size. Notably, this performance is comparable to, and in some cases exceeds, that of reasoning models, despite using significantly fewer tokens (a nearly 10-fold reduction in token consumption).

Figure: Figure 3: Comparison with SOTA models on the MiniF2F-Test dataset. Pass Rate means pass@32 success rate. Average token length is the average number of tokens generated by models across the benchmark. We categorize models as Non-CoT(non reasoning) and CoT(reasoning)
Refer to caption: x3.png

Ineq-Comp (Zhao et al., 2025a) is a benchmark designed to evaluate the robustness of formal provers against minor problem perturbations. It contains 75 seed problems from Olympiad-level inequalities and 150 corresponding transformed variants.
Each seed problem is systematically altered through simple operations(e.g., algebraic rewrites, variable duplication) to create two transformed variants. While humans can easily solve these transformed problems, formal provers often struggle with them even if they can solve the original. A model’s robustness is measured by the ratio of its performance on transformed problems to its performance on the seed problems, for which a higher ratio indicates greater robustness.

Our results are presented in [Table 2](https://arxiv.org/html/2510.00732v1#S4.T2). EvolProver again sets a new SOTA for non-reasoning models on all three metrics (seed, transformed, and ratio), outperforming the next-best non-reasoning model by a significant margin. Its performance is also comparable to that of top reasoning models. Notably, our data augmentation pipeline leads to a substantial boost in robustness: EvolProver’s robustness ratio is 30.61 percentage points higher than that of EvolProver-Base, demonstrating the effectiveness of our approach.

**Table 2: Comparison with SOTA 7B-size models on the Ineq-Comp Benchmark; Pass means pass@32 rate for reasoning models and non-reasoning models, and means 1 $\times$ 3200 pass rate for tree-search models.$\uparrow$ means increase in absolute performance over the ablation model EvolProver-Base.**
| Models | Pass on Seed | Pass on Transformed | Pass Ratio |
| --- | --- | --- | --- |
| Reasoning Models |  |  |  |
| DeepSeek-Prover-V2 (COT) | 66.23% | 44.53% | 67.23% |
| Kimina-Prover-Preview | 50.06% | 27.58% | 55.09% |
| Tree-Search Models |  |  |  |
| DeepSeek-Prover-V1.5 (RL + RMaxTS) | 42.66% | 14.83 % | 34.76 % |
| InternLM2.5-StepProver | 25.59% | 3.44 % | 16.6 % |
| Non-Reasoning Models |  |  |  |
| DeepSeek-Prover-V1.5 (RL) | 34.40% | 6.68% | 19.42% |
| Goedel-Prover-SFT | 43.46% | 14.54% | 33.47% |
| STP | 49.96% | 18.04% | 36.12% |
| EvolProver-Base (Ours) | 43.26% | 14.89% | 34.43% |
| EvolProver (Ours) | 52.20%($\uparrow$ 8.94%) | 34.02%($\uparrow$ 19.63%) | 65.17%($\uparrow$ 30.61%) |

## 5 ANALYSIS

##### Evolution Strategy.

EvolDifficulty and EvolDomain employ a general LLM to directly evolve formalized mathematical theorems. This approach addresses the inherent complexity of mathematical formalization, a task traditionally reliant on specialized models trained to convert natural language problems into formal expressions. However, the direct application of general-purpose LLMs for this purpose remains relatively unexplored, leaving their comparative advantages and limitations as an open question.

To validate our strategy of directly evolving formal statements, we compare it against a common alternative: evolving Natural Language (NL) problems first and then formalizing them. We designed a controlled experiment with four branches:

- •
EvolDomain & EvolDifficulty (Ours): Directly evolves new formal statements from existing ones.
- •
Formalization-Formalizer: Evolves NL problems, then formalizes them using a specialized model (Kimina-Formalizer-7B).
- •
Formalization-LLM-zero-shot: Evolves NL problems, then formalizes them using a general-purpose LLM (Gemini-2.5-Pro) in a zero-shot setting.
- •
Formalization-LLM-few-shot: The same as above, but in a few-shot setting.

Figure: Figure 4: Comparison of the number of candidates passing verification for four evolution methods. Our EvolDomain & EvolDifficulty performs best.
Refer to caption: x4.png

Starting with 400 seed problems, we generated an equal number of candidates using each method and passed them through our stringent verification pipeline. The number of successfully verified statements for each method is shown in [Figure 4](https://arxiv.org/html/2510.00732v1#S5.F4). Our direct evolution approach significantly outperforms all NL-based methods, confirming its superiority. The final candidate count can exceed 400 as each seed may yield multiple valid variants.

##### Domain Diversity.

Here we analyze how our framework improves domain diversity and how this enhancement translates to performance gains.
[Figure 5](https://arxiv.org/html/2510.00732v1#S5.F5) illustrates the effect of EvolDomain on a sample of 200 seed problems. The initial distribution is heavily skewed, with domains like Algebra dominating while others like Calculus are absent. After applying EvolDomain, the dataset becomes significantly more balanced: the share of over-represented domains is reduced, and previously missing categories are introduced. The domains for both sets were classified by DeepSeek-V3 and human-verified.

Figure: Figure 5: Comparison of Mathematical Domain Distribution Before and After EvolDomain.
Refer to caption: x5.png

This improved diversity directly leads to better model performance across various domains, as detailed in [Table 3](https://arxiv.org/html/2510.00732v1#S5.T3). Comparing EvolProver against the EvolProver-Base baseline, our full model achieves gains across most categories. Critically, it makes a breakthrough in Calculus, solving 3 problems where the baseline solved 0. These results confirm that our strategy not only enriches domain diversity but also enhances the model’s overall mathematical capabilities.

**Table 3: Number of proved problems on FormalMATH-Lite benchmark in different domains under 32 generation trials. EvolProver improves upon EvolProver-Base across most domains.**
| Domain | EvolProver-Base | EvolProver | Total |
| --- | --- | --- | --- |
| Algebra | 121 | 141 (+20) | 235 |
| Applied Mathematics | 28 | 33 (+5) | 46 |
| Number Theory | 16 | 23 (+7) | 45 |
| Precalculus | 14 | 15 (+1) | 23 |
| Geometry | 7 | 8 (+1) | 17 |
| Discrete Mathematics | 2 | 5 (+3) | 25 |
| Calculus | 0 | 3 (+3) | 6 |
| Multivariable Calculus | 2 | 2 (–) | 6 |
| Others | 0 | 0 (–) | 23 |

##### Ablation Experiments.

To further validate the effectiveness of our proposed methods, we conduct a series of comprehensive ablation studies. The results are presented in [Table 4](https://arxiv.org/html/2510.00732v1#S5.T4). These experiments isolate the impact of each component and demonstrate that they provide consistent benefits across multiple benchmarks and at various training stages. Experimental details are provided in Appendix [A.2](https://arxiv.org/html/2510.00732v1#A1.SS2).

**Table 4: Ablation experiment results on the FormalMATH-Lite benchmark, the MiniF2F-Test benchmark, and the Ineq-Comp benchmark. All results are pass@32 rate. Superscripts denote the training data used: superscript^0 for Public dataset only; superscript^0+1 for Public dataset + EvolDomain & EvolDifficulty augmentation; superscript^0+1+2 for Full augmentation including Public dataset, EvolDomain & EvolDifficulty, and EvolAST. EvolProver-Ablation-SFT and Evoler-SFT are trained through a sole SFT stage. EvolProver-Base, EvolProver-Ablation-RL and EvolProver are trained through an SFT stage and an RL stage.**
| Models | FormalMATH | MiniF2F | Ineq-Comp<br>(Seed) | Ineq-Comp<br>(Transformed) | Ineq-Comp<br>(Ratio) |
| --- | --- | --- | --- | --- | --- |
| EvolProver-Base^0 | 44.71% | 52.05% | 43.26% | 14.89% | 34.43% |
| EvolProver-Ablation-SFT^0+1 | 50.35% | 65.16% | 49.79% | 29.19% | 58.62% |
| EvolProver-SFT^0+1+2 | 51.53% | 66.39% | 49.82% | 30.35% | 60.19% |
| EvolProver-Ablation-RL^0+1 | 51.98% | 68.22% | 50.36% | 33.05% | 65.62% |
| EvolProver^0+1+2 | 53.96% | 69.80% | 52.20% | 34.02% | 65.17% |

## 6 Conclusion and Future Work

In this paper, we introduced a highly-extensible data augmentation pipeline with three methods: EvolDomain, EvolDifficulty, and EvolAST, designed to improve model generalizability from semantic and syntactic perspectives. Our resulting model, EvolProver, achieves new SOTA results on several key benchmarks, notably surpassing all comparable models on FormalMATH-Lite. For future work, we plan to enhance EvolProver’s reasoning capabilities by incorporating synthetically generated Chain-of-Thought data into its training.

## Reproducibility Statement

We are strongly committed to the reproducibility of our work. Our EvolAST method is designed to be highly extensible, and we encourage the community to contribute by expanding its set of applicable axioms and theorems. To facilitate this, we will release our code and models publicly upon receiving institutional approval.

## Acknowledgment

This work was supported by Ant Group Research Intern Program.

## References

- Anthropic (2025)
Anthropic.
Introducing claude 4, May 2025.
URL https://www.anthropic.com/news/claude-4.
Accessed: 2025-07-28.
- Barras et al. (1997)
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, and et al.
*The Coq Proof Assistant Reference Manual: Version 6.1*.
Inria, 1997.
Version 6.1.
- DeepSeek-AI (2025)
DeepSeek-AI.
Deepseek-v3 technical report, 2025.
URL https://arxiv.org/abs/2412.19437.
- Dong & Ma (2025)
Kefan Dong and Tengyu Ma.
Stp: Self-play llm theorem provers with iterative conjecturing and proving.
*arXiv preprint arXiv:2502.00212*, 2025.
- Hao et al. (2025)
Yuren Hao, Xiang Wan, and Chengxiang Zhai.
An investigation of robustness of llms in mathematical reasoning: Benchmarking with mathematically-equivalent transformation of advanced mathematical problems, 2025.
URL https://arxiv.org/abs/2508.08833.
- Huang et al. (2025)
Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Jiawei Ge, Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang, Yue Wu, Ming Yin, Shange Tang, Yangsibo Huang, Chi Jin, Xinyun Chen, Chiyuan Zhang, and Mengdi Wang.
Math-perturb: Benchmarking llms’ math reasoning abilities against hard perturbations, 2025.
URL https://arxiv.org/abs/2502.06453.
- Ji et al. (2025)
Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai.
Leanabell-prover-v2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning.
*arXiv preprint arXiv:2507.08649*, 2025.
- Jiang et al. (2023)
Xueying Jiang, Jiaxing Huang, Sheng Jin, and Shijian Lu.
Domain generalization via balancing training difficulty and model capability, 2023.
URL https://arxiv.org/abs/2309.00844.
- Lin et al. (2025)
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al.
Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.
*arXiv preprint arXiv:2508.03613*, 2025.
- Luo et al. (2025a)
Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, Yansong Tang, and Dongmei Zhang.
Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct, 2025a.
URL https://arxiv.org/abs/2308.09583.
- Luo et al. (2025b)
Ziyang Luo, Can Xu, Pu Zhao, Qingfeng Sun, Xiubo Geng, Wenxiang Hu, Chongyang Tao, Jing Ma, Qingwei Lin, and Daxin Jiang.
Wizardcoder: Empowering code large language models with evol-instruct, 2025b.
URL https://arxiv.org/abs/2306.08568.
- Moura & Ullrich (2021)
Leonardo de Moura and Sebastian Ullrich.
The lean 4 theorem prover and programming language.
In André Platzer and Geoff Sutcliffe (eds.), *Automated Deduction – CADE 28*, pp. 625–635, Cham, 2021. Springer International Publishing.
ISBN 978-3-030-79876-5.
- Parashar et al. (2025)
Shubham Parashar, Shurui Gui, Xiner Li, Hongyi Ling, Sushil Vemuri, Blake Olson, Eric Li, Yu Zhang, James Caverlee, Dileep Kalathil, and Shuiwang Ji.
Curriculum reinforcement learning from easy to hard tasks improves llm reasoning, 2025.
URL https://arxiv.org/abs/2506.06632.
- Paulson (1994)
Lawrence C. Paulson.
*Isabelle: A Generic Theorem Prover*, volume 828 of *Lecture Notes in Computer Science*.
Springer Berlin, Heidelberg, 1994.
ISBN 978-3-540-58244-1.
doi: 10.1007/3-540-58244-0.
- Ren et al. (2025)
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al.
Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.
*arXiv preprint arXiv:2504.21801*, 2025.
- Shang et al. (2025)
Shijie Shang, Ruosi Wan, Yue Peng, Yutong Wu, Xiong-hui Chen, Jie Yan, and Xiangyu Zhang.
Stepfun-prover preview: Let’s think and verify step by step.
*arXiv preprint arXiv:2507.20199*, 2025.
- Wang et al. (2025a)
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li.
Kimina-prover preview: Towards large formal reasoning models with reinforcement learning, 2025a.
URL https://arxiv.org/abs/2504.11354.
- Wang et al. (2025b)
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li.
Kimina-prover: Applying test-time rl search on large formal reasoning models.
*Hugging Face Community Blog*, 7 2025b.
URL https://huggingface.co/blog/AI-MO/kimina-prover.
- Wu et al. (2024)
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen.
Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024.
URL https://arxiv.org/abs/2410.15700.
- xAI (2025)
xAI.
Grok code fast 1.
https://x.ai/news/grok-code-fast-1, August 2025.
Accessed: 2025-08-26.
- Xin et al. (2024a)
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang.
Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data.
*arXiv preprint arXiv:2405.14333*, 2024a.
- Xin et al. (2024b)
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al.
Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search.
*arXiv preprint arXiv:2408.08152*, 2024b.
- Xin et al. (2025)
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen.
Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving, 2025.
URL https://arxiv.org/abs/2502.03438.
- Xu et al. (2024)
Can Xu, Qingfeng Sun, Kai Zheng, Xiubo Geng, Pu Zhao, Jiazhan Feng, Chongyang Tao, Qingwei Lin, and Daxin Jiang.
Wizardlm: Empowering large pre-trained language models to follow complex instructions.
In *The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024*. OpenReview.net, 2024.
URL https://openreview.net/forum?id=CfXh93NDgH.
- Yu et al. (2024)
Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu.
Metamath: Bootstrap your own mathematical questions for large language models, 2024.
URL https://arxiv.org/abs/2309.12284.
- Yu et al. (2025)
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al.
Formalmath: Benchmarking formal mathematical reasoning of large language models.
*arXiv preprint arXiv:2505.02735*, 2025.
- Zhang et al. (2025)
Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai.
Leanabell-prover: Posttraining scaling in formal reasoning.
*arXiv preprint arXiv:2504.06122*, 2025.
- Zhao et al. (2025a)
Haoyu Zhao, Yihan Geng, Shange Tang, Yong Lin, Bohan Lyu, Hongzhou Lin, Chi Jin, and Sanjeev Arora.
Ineq-comp: Benchmarking human-intuitive compositional reasoning in automated theorem proving on inequalities.
*arXiv preprint arXiv:2505.12680*, 2025a.
- Zhao et al. (2025b)
Xueliang Zhao, Wei Wu, Jian Guan, and Lingpeng Kong.
Promptcot: Synthesizing olympiad-level problems for mathematical reasoning in large language models, 2025b.
URL https://arxiv.org/abs/2503.02324.
- Zheng et al. (2021)
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu.
Minif2f: a cross-system benchmark for formal olympiad-level mathematics.
*arXiv preprint arXiv:2109.00110*, 2021.

## Appendix A Appendix

### A.1 Details of Training EvolProver

##### Data Curation.

Our data curation process follows a multi-stage funnel. We begin with a seed pool of approximately 3.3 million verified formal statements aggregated from four sources: DeepSeek-Prover-V1, STP-lean, MiniF2F-Valid, and FormalMATH-All (excluding the FormalMATH-Lite subset).

From this pool, we sample 70k statements for evolution. These are processed by our EvolDomain and EvolDifficulty methods using Gemini-2.5-Pro and DeepSeek-R1, which then undergo a verification process to yield 57.4k high-quality (statement, description) pairs. This verification first involves a syntax check using the Lean 4 compiler; if the compiler finds a syntax error, we use DeepSeek-V3 (DeepSeek-AI, 2025) to repair it, after which DeepSeek-V3 performs a final semantic check. Next, we apply EvolAST to this set for syntactic diversification, expanding it to approximately 96.7k entries (as a single statement can generate multiple AST variants). Finally, we generate proofs for each statement. Using DeepSeek-Prover-V2-671B and Goedel-Prover-V2-8B as expert models, we generate 50 proof candidates per statement and retain only those that pass Lean 4 compiler verification. After removing duplicates, this process results in a final training dataset of 39.2k unique (statement, proof) pairs. To prevent data leakage, We ensure that the initial states of all theorem statements in our data are different from those in the tested benchmarks.

##### Supervised Fine Tuning.

We fine-tune the DeepSeek-Prover-V1.5-Base model using full-parameter supervised fine-tuning (SFT). Our training data is a mixture of our self-evolved instruction dataset and publicly available datasets. The model is trained for one epoch with the AdamW optimizer. We set the initial learning rate to
$1.0\times 10^{-5}$ and decay it using a cosine scheduler with a 5% warmup ratio. All sequences are truncated to a maximum length of 4096 tokens, and we use a global batch size of 32.

Reinforcement Learning. Following the Supervised Fine-Tuning (SFT) stage, we further enhance the model’s performance by applying Reinforcement Learning (RL) to the SFT checkpoint. For RL training, we utilize our augmented open-source dataset of formal problems. We employ a standard binary reward: for each problem, the model receives a reward of $1$ if the generated Lean proof is correct, and 0 otherwise. This RL fine-tuning process produces the final EvolProver.

##### RL Training Details

To improve training efficacy, we curate the RL training dataset by filtering problems based on the pass@1 success rate of the SFT checkpoint. We include only problems where $0<\text{pass}@1<1/2$. This selection strategy ensures that the training set is challenging yet solvable for our model. The filtered dataset contains 2,718 problems. We initialize both the actor and critic models with the weights from the SFT checkpoint and train them using Proximal Policy Optimization (PPO). The training runs for 10 epochs with a batch size of 256, a constant actor learning rate of $1.0\times 10^{-6}$, a constant critic learning rate of $1.0\times 10^{-5}$, a clip ratio of $0.2$, and a KL divergence loss coefficient of $0.001$.

### A.2 Ablation Experiments

#### A.2.1 Ablation Model Training

To precisely evaluate the contribution of each component, we trained a series of ablation models under controlled conditions. All training hyperparameters were kept identical across corresponding stages. The models are:

- •
EvolProver-Base: Our baseline, trained on the original, unaugmented public dataset through both SFT and RL stages.
- •
EvolProver-Ablation-SFT: Trained on data augmented only by EvolDomain and EvolDifficulty, and only undergoes the SFT stage.
- •
EvolProver-Ablation-RL: Same data as above (EvolDomain and EvolDifficulty only), but undergoes the full SFT and RL training process. This model directly isolates the impact of EvolAST when compared to the final EvolProver.
- •
EvolProver-SFT: The checkpoint of our final model after being trained on the fully augmented dataset (including EvolAST) for the SFT stage only.

We did not create an “EvolAST-only” model, as EvolAST operates on the output of EvolDomain and EvolDifficulty, making such an experiment logically infeasible.

#### A.2.2 Ablation Experiment Results

The results of our ablation experiments, presented again in [Table 5](https://arxiv.org/html/2510.00732v1#A1.T5) for convenience, lead to two key conclusions.
First, data augmentation provides a substantial boost, with even the partially augmented models (Ablation-SFT/RL) drastically outperforming the EvolProver-Base model across all benchmarks, often by more than 10%.
Second, the EvolAST method consistently yields further improvements across all benchmarks. In the SFT stage, EvolProver-SFT (with EvolAST) surpasses EvolProver-Ablation-SFT (without EvolAST). Similarly, in the RL stage, the final EvolProver outperforms EvolProver-Ablation-RL. This demonstrates the value of the EvolAST method in both training phases.

**Table 5: Ablation experiment results on the FormalMATH-Lite benchmark, the MiniF2F-Test benchmark, and the Ineq-Comp benchmark. All results are pass@32 rate. Superscripts denote the training data used: superscript^0 for Public dataset only; superscript^0+1 for Public dataset + EvolDomain & EvolDifficulty augmentation; superscript^0+1+2 for Full augmentation including Public dataset, EvolDomain & EvolDifficulty, and EvolAST.**
| Models | FormalMATH | MiniF2F | Ineq-Comp<br>(Seed) | Ineq-Comp<br>(Transformed) | Ineq-Comp<br>(Ratio) |
| --- | --- | --- | --- | --- | --- |
| EvolProver-Base^0 | 44.71% | 52.05% | 43.26% | 14.89% | 34.43% |
| EvolProver-Ablation-SFT^0+1 | 50.35% | 65.16% | 49.79% | 29.19% | 58.62% |
| EvolProver-SFT^0+1+2 | 51.53% | 66.39% | 49.82% | 30.35% | 60.19% |
| EvolProver-Ablation-RL^0+1 | 51.98% | 68.22% | 50.36% | 33.05% | 65.62% |
| EvolProver^0+1+2 | 53.96% | 69.80% | 52.20% | 34.02% | 65.17%(^1^11While the performance ratio for EvolProver is slightly lower than that of EvolProver-Ablation-RL, this metric can be misleading when viewed in isolation. This is because EvolProver demonstrates absolute gains in both the numerator and the denominator of the fraction. The marginal decrease in the final ratio is therefore an artifact of the denominator’s more substantial growth, rather than an indication of inferior performance.) |

### A.3 DETAILS FOR EvolDomain

#### A.3.1 Prompt Template

Formal problems can precisely extract the universal logical skeleton of a mathematical problem. Our strategy leverages this by transferring that structure to new domains to systematically create rigorous new problems. Our preset domains cover a range of topics from high school competition problems to undergraduate-level subjects. The prompt template format of EvolDomain is as follow:

#### A.3.2 Case Study

We select an example of EvolDomain from the evolved dataset. The original Lean 4 statement is as follows:

The evolved Lean 4 statement and its corresponding natural language description are as follows:

### A.4 DETAILS FOR EvolDifficulty

To generate problems of varying difficulty, we define a set of evolution strategies through deliberation and screening by a team of mathematics experts. These strategies fall into two categories: upward (to increase difficulty) and downward (to decrease difficulty), each with specific methods for implementation.

#### A.4.1 UpwardEvolution

The prompt tempalte for upward evolution is as follows:

The strategies and specific methods are as follows:

#### A.4.2 DownwardEvolution

The prompt template for downward evolution is as follows:

The strategies and specific methods are as follows:

#### A.4.3 Case Study

We select two examples of EvolDifficulty from evolved dataset. The original Lean 4 statement for upward evolution is as follows:

The evolved Lean 4 statement and its corresponding natural language description are as follows:

The original Lean 4 statement for downward evolution is as follows:

The evolved Lean 4 statement and its corresponding natural language description are as follows:

### A.5 DETAILS FOR Verification

The prompt template to judge consistency between natural language problem and formal statement is as follows:

The prompt template to judge mathematical correctness of formal statements and natural language problem is as follows:

The prompt template for filtering out low-difficulty problems is as follows:

Prompt template for fixing compilation errors in a formal statement is as follows:

### A.6 Case Study FOR EvolAST

We select an example of EvolAST from evolved dataset. The original Lean 4 statement is as follows:

The evolved Lean 4 statement is as follows:

### A.7 Use of Large Language Models

We utilized Large Language Models (LLMs) solely to refine the language and improve the clarity of this manuscript.

## Peer Reviews

confidence: 2
contribution: 2
initial_rating: 4
presentation: 3
questions: 1. What specifically distinguishes EvolDomain/EvolDifficulty from prior prompt-based data synthesis?
2. How often do EvolDomain/EvolDifficulty produce invalid or semantically incorrect statements before filtering?
3. The verification pipeline appears to be computationally expensive. What is the computational cost of running the full pipeline (LLM generation + filtering + AST evolution + proof synthesis)?
soundness: 3
strengths: The paper empirically demonstrates that diversified training data can improve robustness of formal theorem provers. The multi-stage verification (Lean compilation + LLM judging) appears carefully constructed, and the ablation study highlights the contribution of each augmentation component. Improvements are reported on several benchmark datasets (FormalMATH-Lite, MiniF2F-Test, and Ineq-Comp).  The paper’s focus on token-efficient, non-reasoning proving is practically important and timely, given the inference-time and cost problem of chain-of-thought systems.
summary: This paper introduces EvolProver, a 7B parameter non-reasoning LEAN theorem prover model. The model is fine-tuned using data generated from a new data augmentation pipeline. The pipeline consists of three components:

1. **EvolDomain**: Uses LLMs to reformulate the existing problem into different mathematical domains.
2. **EvolDifficulty**. Uses LLMs to adjust the difficulty of the theorem.
3. **EvolAST**: Applies syntactical rewrites using a small amount of equivalence rules.

Each transformed problem is filtered via a Lean syntactic check and an LLM semantic check. The pipeline is applied to existing theorem datasets, producing a larger and more diverse dataset used to fine-tune DeepSeek-Prover-V1.5. The resulting model, EvolProver, achieves strong performance outperforming both non-reasoning and some reasoning models.
weaknesses: My main concern is the novelty of the proposed data augmentation method. The individual techniques used in the pipeline appear to be adaptations of well-known ideas rather than new contributions. Using LLM prompting to evolve instructions or problems (EvolDomain, EvolDifficulty) closely resembles approaches such as WizardMath or MetaMath. The final model architecture and training recipe (SFT + RL) seem to follow existing pipelines from e.g. DeepSeek-Prover.

Reproducibility and community impact are constrained by unclear release plans: code, datasets, and model checkpoints appear contingent on institutional approval with no firm timeline or open-model replication, making it difficult for others to verify and build upon the work.

---

confidence: 3
contribution: 3
initial_rating: 4
presentation: 3
questions: 1. Could the authors provide token-length and proof-length statistics restricted to the intersection of solved problems between EvolProver and EvolProver-Base?
	2.	Can the authors further clarify how they ensured no data leakage between training and test dataset? A quantitative similarity or embedding-based overlap metric would help.
soundness: 2
strengths: 1.  The integration of symbolic AST transformations into the data-generation pipeline is novel and convincing. EvolAST guarantees semantic correctness and diversifies syntax without requiring additional verification.
2. MThe paper clearly outlines each augmentation stage and the verification loop, with Lean 4 compiler checks for both syntax and semantics.
3. Consistent and substantial improvements across benchmarksindicate that the augmented data meaningfully enhances formal reasoning ability.
summary: This paper presents EvolProver, a formal-reasoning LLM fine-tuned on a synthetically expanded dataset constructed through three evolution mechanisms: 

(1) EvolDomain, which performs cross-domain statement translation via LLMs;  
(2) EvolDifficulty, which adjusts statement complexity; and  
(3) EvolAST, which applies symbolic abstract-syntax-tree (AST) rewriting rules such as commutativity and De Morgan transformations to generate logically equivalent variants.  

The resulting dataset, comprising roughly 39 k verified (statement, proof) pairs in Lean 4, is used to SFT and RL-train a DeepSeek-Prover-V1.5-Base model. EvolProver achieves new state-of-the-art results on several formal benchmarks including FormalMATH-Lite, MiniF2F-Test, and Ineq-Comp, demonstrating the potential of AST-based symbolic augmentation to improve verifiable reasoning.
weaknesses: 1. Data contamination analysis: While the authors mention ensuring non-overlapping “initial states,” this safeguard is underspecified. It remains unclear whether evolved statements might still share logical content or minor transformations with the test set. A more thorough contamination study—quantifying overlap at the theorem or syntactic-similarity level—would strengthen the empirical claims.
2. Lack of output-length analysis: Table 1 reports that EvolProver generates substantially longer outputs than comparable non-reasoning models, yet the paper provides no interpretation. It is unclear whether performance gains arise from genuinely better reasoning or simply more verbose exploration, which turns the model into a "semi-reasoning" model.
    - I would appreciate it a follow-up would measure output length (or verified proof length) on the subset of problems solved by both EvolProver and its baseline, to see whether the improvement correlates with verbosity or genuine efficiency.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 3
questions: Addressing the questions mentioned in the weakness points should be enough.
soundness: 3
strengths: 1. Practical and well-motivated. They address a real problem on the fragility and poor generalization of theorem-proving LLMs, and the strategy they use (data-centric improvements) is simple but effective, much easier than building a reasoning model in practice.

2. Systematic pipeline design. The decomposition into syntactic (EvolAST), semantic (EvolDomain), and difficulty-based (EvolDifficulty) augmentations is both intuitive and well-structured.

3. Results are good. The model achieves consistent SOTA performance across diverse benchmarks, including non-reasoning categories where size-matched baselines are surpassed. They can achieve even pretty close performance compared to the SOTA reasoning model baselines. Ablations studies convince us into believing that the pipeline really helps, rather than overfitting to artifacts.
summary: The paper presents a data augmentation pipeline aimed at improving the robustness and generalization of large language models (LLMs) for formal theorem proving. The proposed system combines three key modules:

* EvolAST – syntactic augmentation using Abstract Syntax Tree-based transformations that preserve semantics while changing structure;

* EvolDomain – semantic augmentation by translating theorems across mathematical domains (e.g., geometry ↔ algebra) using LLMs;

* EvolDifficulty – difficulty modulation via evolutionary instructions to generate problems of varying complexity.

After automated verification, the augmented data is used to train EvolProver, a 7B-parameter non-reasoning model that achieves new SOTA performance on multiple formal math benchmarks (e.g., FormalMATH-Lite, MiniF2F, Ineq-Comp). Ablations confirm each augmentation’s benefit. The approach focuses on data diversity rather than architectural changes.
weaknesses: 1. The paper remains more empirical than theoretical, as there's no deeper analysis of why the augmentations help, or how they relate to reasoning robustness.

2. There comes concerns on whether or not the framework relies on LLM-generated data too much. EvolDomain and EvolDifficulty both depend on LLM quality, thus risk subtle semantic drift or spurious logic, which might not be fully detected by verification.

3. Only benchmarks with formal Lean-style problems are tested, how robust the framework is when generalizing to other theorem systems, or other symbolic reasoning datasets?

4. The term "evolutionary" may be overstated a little bit?

---

confidence: 4
contribution: 3
initial_rating: 4
presentation: 3
questions: 1. Can the three proposed augmentation methods be applied to chain-of-thought reasoning models? What obstacles might arise from directly applying them to CoT-style reasoning models? The paper claims that current provers are fragile to even minor transformations of problem statements — does this fragility persist in contemporary reasoning provers like Deepseek Prover v2 or Geodel Prover v2?

2. Line 142 states that EvolAST is introduced "to mitigate this issue (the inevitable introduction of syntactic or semantic errors)," yet Figure 2 places the EvolAST process after EvolDomain and EvolDifficulty. This ordering seems odd: errors can propagate, so a theorem that becomes semantically incorrect (e.g., unprovable) after EvolDomain or EvolDifficulty would not be fixed by applying EvolAST afterward. Please provide further explanation for this pipeline ordering and clarify how EvolAST mitigates syntactic/semantic errors introduced by earlier stages.
soundness: 2
strengths: 1. The proposed EvolAST method is novel: it leverages Lean 4 features in an intuitive and effective way. The results in Table 2 on the Ineq-Comp dataset show that this augmentation can substantially mitigate non-CoT provers’ fragility to the specific form of a statement.

2. From Figure 5, the EvolDomain approach appears to significantly alleviate the concentration of formal-statement datasets in algebra and number theory. This may be valuable for improving ATP generalization across different mathematical domains.

3. The ablation study is thorough. Table 4 presents multiple combinations of SFT, RL, and different augmentation methods, providing useful insight into which components are effective. The comparison between directly augmenting formal data and the more traditional approach of augmenting natural-language data first and then translating it is also a useful addition.

4. Figures and tables are clear and easy to understand, and the paper is well written overall.
summary: This paper proposes three data augmentation methods for formal mathematics statements based on symmetry and difficulty. EvolAST: apply seven prewritten transformation rules at random on the theorem’s AST to produce logically equivalent variants; EvolDomain: translate problems across different domains while preserving their core logic, guided by evolutionary instructions for the LLM to perform the conversions; EvolDifficulty: use an LLM with instructions to adjust the difficulty of existing theorems and generate statements at varying difficulty levels. Using this pipeline to augment public datasets (e.g., STP and DeepSeek Prover V1) and training on DeepSeek Prover V1.5 base, the authors build EvolProver. Experiments show strong performance the proposed model among non-CoT 7B ATP models.
weaknesses: 1. Choice of an old base model and non-CoT approach, which appears unnecessary and hard to justify. The paper trains EvolProver on a non-CoT DeepSeek V1.5 7B model. The three proposed data-augmentation methods should in principle be directly applicable to CoT-style models (e.g., DeepSeek Prover v2 or Goedel Prover v2), so restricting experiments to a non-CoT, relatively old base model limits the relevance of the work given that much of the recent ATP community has shifted to CoT-capable reasoning models. EvolProver’s performance is still substantially weaker than contemporary reasoning models. The authors should further explain why they chose a non‑CoT model and an older base model.
2. Small amount of synthesized data and no cost analysis. The amount of augmented/synthesized data is relatively small and the paper does not discuss the cost of data synthesis. Line 653 states that the pool of publicly available datasets used is 3.3 million examples, but only 39.2k examples were synthesized (Line 665). The authors do not explain the roughly two-order-of-magnitude gap (e.g., due to cost or filtering?), nor do they provide analysis of synthesis cost, token usage, or API expenses.
3. Missing proportions of original vs. augmented data in SFT and RL. The paper does not report the ratio of original to augmented examples during supervised fine-tuning (SFT) and reinforcement learning (RL), which hurts reproducibility. Given the large disparity in size between the original and augmented datasets, the mixing ratio is an important experimental detail and should be provided.
4. Minor writing and presentation issues (do not affect readability but should be fixed to improve manuscript quality)

- Line 124: missing space before a citation.
- Lines 143, 153, 227: inconsistent capitalization of “Lean4” vs. “Lean 4”; terms should be made consistent.
- Table 4 and Table 5 appear to contain the same content and may be duplicated.
- Related work: the survey of data-augmentation methods focuses on informal mathematics; the authors should also cover data-augmentation methods specific to formal mathematics. (eg., STP and Ineq-Comp)

##

---

confidence: 4
contribution: 2
initial_rating: 4
presentation: 3
questions: 1. Why wasn't DeepSeek-Prover-V2-7B-non-CoT included in the comparisons for FormalMATH and Ineq-Comp benchmarks, given its strong performance on MiniF2F-Test? Including these comparisons would provide a more comprehensive evaluation of EvolProver's capabilities across different benchmarks.​
2. The example shown in Figure 1 appears to involve relatively minor tactic changes in Lean that may not significantly affect the proof difficulty. Could you provide more case studies demonstrating specific instances where the augmented dataset enabled EvolProver to solve problems that the baseline model (EvolProver-Base) or other state-of-the-art models could not solve?
soundness: 2
strengths: 1. The proposed data augmentation pipeline demonstrates a novel and systematic approach to improving model generalizability by addressing both syntactic and semantic symmetry, as well as difficulty variation, which is a comprehensive solution to the fragility issue in formal theorem proving.​
2. The ablation studies and controlled experiments effectively validate the contribution of each component in the pipeline, showing consistent performance improvements across multiple benchmarks and training stages.
summary: This paper presents EvolProver, a 7B-parameter non-reasoning theorem prover enhanced through a novel data augmentation pipeline that addresses both symmetry and difficulty aspects of formalized mathematical problems. The pipeline consists of three complementary methods: EvolAST for syntactic symmetry transformation, EvolDomain for cross-domain semantic symmetry, and EvolDifficulty for generating problems with varying difficulty levels. Experimental results demonstrate that EvolProver achieves good performance on multiple benchmarks, including FormalMATH-Lite (53.8% pass@32), MiniF2F-Test (69.8% pass@32), and Ineq-Comp datasets, outperforming comparable non-reasoning models and even some reasoning-based models while using significantly fewer tokens.
weaknesses: 1. The performance advantage of EvolProver over DeepSeek-Prover-V2-7B-non-CoT on MiniF2F-Test is relatively modest (69.8% vs 68.0±0.5%), while DeepSeek-Prover-V2-7B-non-CoT uses fewer average tokens, raising questions about the practical significance of the improvement.​
2. The case study in Figure 1 does not clearly demonstrate how the augmented dataset helps solve problems that were previously unsolvable, making it difficult to assess the qualitative impact of the data augmentation.​
3. The ablation experiments do not include a detailed analysis of how each component contributes to performance on different mathematical domains, which would help understand the specific strengths of each augmentation method.


Decision: Accept (Poster)