GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

## Abstract

Abstract Solving math problems through verifiable languages such as Lean has significantly impacted both the mathematics and computer science communities. Current state-of-the-art models are often trained with expensive online Reinforcement Learning (RL) or expert iteration. However, these approaches rely on fixed problem sets, which causes inefficient training and limits the model to tackle complex problems. To overcome these limitations, we propose GAR : G enerative A dversarial R einforcement learning , a comprehensive RL training framework that jointly trains the problem composer and solver in an adversarial loop. GAR introduces an implicit curriculum learning mechanism, which aligns task difficulty with the prover’s evolving capability. It thereby improves the training efficiency and enables stronger performance of proving advanced theorems. Experiments show that with GAR training, Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B achieve an average relative improvement in pass@32 of 4.20% on MiniF2F-Test benchmark, while DeepSeek-Prover-V2’s pass@32 on ProofNet-Test increases from 22.58% to 25.81% . Beyond formal proving, GAR establishes a general RL paradigm for co-evolution of problem generation and solving under verifiable environments.

## 1 Introduction

The capability to perform formal mathematical reasoning has long been regarded as both a hallmark of human intelligence and a key objective of machine learning (Newell & Simon, 1956). The ability is typically assessed through rigorous mathematical derivations (Yang et al., 2024b). With the emergence of Large Language Models (LLMs), developing accurate and reliable reasoning has become an active area of research. Recent progress in ZERO RL training (Guo et al., 2025) has further advanced reasoning systems by introducing Long Chain-of-Thought (CoT) thinking models that have self-reflection and self-correction capability.

However, the inherent ambiguity of Natural Language (NL) makes it challenging to verify intermediate reasoning steps. This problem is more severe in advanced mathematics, where the task is to prove theorems rather than give a numerical or formulaic answer.
The increasing complexity of modern math compounds this difficulty, as illustrated by the prolonged verification of Fermat’s Last Theorem (Wang et al., 2024). To address this issue, researchers have grounded reasoning in formal logical systems, enabling automatic verification through Formal Language (FL). Based on this idea, some researchers model the reasoning process formally with dependent type languages like Lean (De Moura et al., 2015; Moura & Ullrich, 2021) and Coq (Coq, 1996). Other uses higher-order logic to build language like Isabelle (Paulson, 1994) and HOL (Harrison, 2009). All the above languages make every intermediate step of math reasoning verifiable.

Nevertheless, mastering FLs requires considerable expertise, particularly in dependent-type systems like Lean, where proofs often demand complex type matching and the use of functions with limited data (Wang et al., 2025c). Thus, many works have sought to leverage advances in LLMs to solve FL problems and train specialized FL provers (Polu et al., 2022; Jiang et al., 2022; Xin et al., 2024a; Wang et al., 2024; Lin et al., 2025a; Dong & Ma, 2025b). The verifiability of FLs also motivates large-scale synthesis of new statements, which enables extensive expert iteration (Polu et al., 2022; Xin et al., 2025) or Reinforcement Learning (RL) (Ren et al., 2025; Wang et al., 2025a; Lin et al., 2025b) to further enhance perver’s performance.

Figure: Figure 1: GAR Training Framework: Each iteration of GAR consists two stages. (a) Generation Stage: Pairs of NL statements are sampled from the base repository and combined by the statement fuser to create more challenging problems that fit the current model’s capability. Then, these statements are autoformalized and submitted to the prover to write multiple proofs. Subsequently, the proofs are checked by the Lean verifier for reward assignments. (b) Adversarial Reinforcement Learning: The prover is rewarded for producing correct proofs on medium and high-difficulty statements, while the statement fuser is rewarded for generating harder but solvable problems. This adversarial dynamic drives both models to evolve together.
Refer to caption: x1.png

However, most prior approaches in RL or expert iteration rely on fixed theorem statement sets and optimize only the prover. The statement dataset is unchanged during the process. It also leads to wasted computation on trivial or unsolvable tasks. In expert iteration, datasets often require repeated annotation. On the other hand, advanced RL methods suffer from the absence of an adaptive difficulty level of statements during rollouts, which restricts concentrated exploration and limits progress on complex theorems. More broadly, only a few works discuss a systematic way to align problem difficulty with the prover’s growing skill.

To address this limitation, we propose GAR: Generative Adversarial Reinforcement Learning, a comprehensive RL training framework as presented in Figure [1](https://arxiv.org/html/2510.11769v1#S1.F1). GAR jointly optimizes the prover and the problem composer, termed as the statement fuser, through adversarial training. This process establishes an implicit curriculum learning that dynamically adjusts statement difficulty to match the prover’s development. Each iteration of the GAR framework consists of two stages: the generation and the adversarial RL stage. In the generation stage, the statement fuser synthesizes harder statements from existing solvable ones, and the prover attempts to solve them. In the RL training stage, the fuser is rewarded for producing difficult yet solvable statements, while the prover is rewarded for correctly proving medium and high-difficulty problems. This adversarial setup ensures that statement complexity evolves alongside the prover’s capabilities, resulting in more efficient and effective training.

We summarize our contributions as follows: (1) We introduce GAR, a comprehensive RL training framework that establishes implicit curriculum learning, improving the prover’s reasoning ability while preventing wasted effort on trivial or unsolvable statements. (2) We present Statement Fusion technique, which enables the creation of novel formal statements beyond direct formalization of NL problems, producing theorem statements better aligned with model capability. (3) We demonstrate the effectiveness of the GAR through extensive experiments by training two base models using GAR. We achieve an average of 4.20% relative improvement on MiniF2F-Test (Zheng et al., 2021) and raise DeepSeek-Prover-8B’s pass@32 on the more challenging ProofNet-Test (Azerbayev et al., 2023) from 22.58% to 25.81%. It highlights the effectiveness and generality of GAR.

Furthermore, the GAR contributes a general RL paradigm for the co-evolution of problem generation and solving in verifiable environments, which offers new directions for adversarial co-training in other reasoning-intensive domains. To facilitate the advancement of the field, we will open-source the training and inference code of GAR in the near future in [here](https://github.com/RickySkywalker/GAR-Official/tree/main).

## 2 Methodology

In this section, we introduce the GAR framework in detail. The prover’s task is to produce Lean4 proofs from NL-FL statement pairs. Our framework trains the prover to improve at the task by adapting theorem difficulty to the prover’s evolving capabilities through adversarial training of both the prover and the statement fuser. Each iteration of GAR consists of two stages: the Generation stage (Section [2.1](https://arxiv.org/html/2510.11769v1#S2.SS1)) and the Adversarial Reinforcement Learning stage (Section [2.2](https://arxiv.org/html/2510.11769v1#S2.SS2)).
We first describe the behavior of each stage in a single iteration in detail, then present the complete procedure in Section [2.3](https://arxiv.org/html/2510.11769v1#S2.SS3).

### 2.1 Generation Stage

The generation stage of GAR consists of two processes, namely statement fusion, which produces new statements, and proof writing, which generates and evaluates candidate proofs.

#### 2.1.1 Statement Fusion

This process generates harder statements from existing ones. It aims to mitigate the mismatch between the fixed datasets and the prover’s evolving ability. This process first samples two NL statements from the base dataset, formally: $\bm{s}_{base}=(s_{1}^{(NL)},s_{2}^{(NL)})\sim\mathcal{D}_{stat}$, where $\mathcal{D}_{stat}$ is a repository consists of 793,243 NL statements collect from Lean-Workbook (Wu et al., 2024b) and Numina-Math (LI et al., 2024). The sampled pair is then passed to the statement fuser trained in the previous iteration of GAR. The fuser is instructed to synthesize a more challenging statement by combining the key ideas of the two inputs, namely:

$$ $s^{(NL)}=Fuser_{i-1}(\bm{s}_{base})$ $$

where $i$ denotes the current iteration index, $s^{(NL)}$ is the generated NL statement, and $Fuser_{i-1}$ is the fuser from the prior step (initialized as base model when $i=0$).

In particular, we chose thinking models like Qwen3 (Team, 2025) or DeepSeek-R1 (Guo et al., 2025) as the base model for the statement fuser because of its outstanding performance.
However, direct use of their native Long CoT capability often results in overthinking and degraded quality of the generated statement. To mitigate this, we reinitialize the thinking process by passing the default thinking stage and restarting it with a dedicated indicator token named $<$analysis$>$. This trick yields more focused and task-specific reasoning. The full prompt for the statement fusion is shown in Figure [2](https://arxiv.org/html/2510.11769v1#S2.F2). Subsequently, the generated NL statement is passed to the autoformalizer, which converts the NL statement into Lean statement $s^{(FL)}$. The formalized statement is then passed to Lean4 for compilation check. This step filters out statements with grammatical errors.

Figure: Figure 2: Prompt for the Statement Fuser to generate harder statements from existing ones and restart thinking using a new indicator in GAR generation stage

In the statement fusion stage, they deliberately separate the fusion of NL statements from the formalization of FL statements. Two key insights guide this design. First, prior studies (Wang et al., 2024; Xin et al., 2024b) have shown that NL statements play a crucial role in supporting formal reasoning.
Secondly, current 8B-scale general LLMs exhibit only a limited understanding of FL. This causes them to fail to capture essential relations, which hinders the generation of more robust statements. Consequently, the fuser produces statements that have a high likelihood of failing the compilation check if we directly fuse formal statements, as seen in Dong & Ma (2025b).
Thus, GAR firstly fuses the statement in NL and formalizes it to FL, ensuring the fused statements are adaptively more challenging than the base problems to fit prover performance evolution.

#### 2.1.2 Proof Writing

Utilizing the NL-FL statement pair generated by the fusion process, the prover from the last iteration generates $n$ candidate proofs (with $n=16$ in our implementation), denoted as $\{o_{k}\}_{k=1}^{n}$, specifically:

$$ $o_{k}=Prover_{i-1}(s^{(NL)},s^{(FL)}),\forall k\in[1,n]$ $$

When $i=0$, it is the base prover model like deepSeek-Prover-V2 (Ren et al., 2025) or Goedel-Prover-V2 (Lin et al., 2025b).

The set of candidate proofs $\{o_{k}\}_{k=1}^{n}$ is then passed to the Lean4 verifier to check correctness. Based on the verification results, we compute the empirical pass rate $p$ of this statement for reward assignment as $p=\frac{n_{pass}}{n}$, where $n_{pass}$ is the number of proofs that pass verification.

### 2.2 Adversarial Reinforcement Learning

This section outlines the training process of GAR, where the prover and statement fuser are optimized in competition, deriving adversarial learning and mutual improvement.

#### 2.2.1 Statement Fuser Training

The statement fuser is trained to synthesize problems that are slightly beyond the prover’s current capability, thereby creating an implicit curriculum. To achieve this, we assign rewards to the generated NL statements that encourage the production of more challenging but solvable problems. We adopt a variant of Group Relative Policy Optimization (GRPO) (Shao et al., 2024) for this optimization. Specifically, for each step $i$, the fuser generates $N$ statements (with $N=1024$ in our implementation). Formally, generated statement set is: $\left\{s_{i,j}^{(NL)}\right\}_{j=1}^{N}$, and base statement set is represented as: $\left\{\bm{s}^{(base)}_{i,j}=\left(s_{i,j,1}^{(NL)},s_{i,j,2}^{(NL)}\right)\right\}_{j=1}^{N}$. The statement fuser $Fuser_{i-1}$ is then updated by maximizing the following objective.

$$ $\displaystyle\mathcal{J}_{GRPO}^{(F)}(\theta)=$ $\displaystyle\mathbb{E}_{\left[\left\{\bm{s}_{i,j}^{(base)}\right\}_{j=1}^{N}\sim\mathcal{D}_{stat};\,\left\{s_{i,j}^{(NL)}\sim\pi_{\theta_{old}}\left(\bm{s}_{i,j}^{(base)}\right)\right\}\right]}$ (1) $\displaystyle\frac{1}{N}\sum_{j=1}^{N}\left(\min\left\{\delta_{i,j}^{(stat)}A_{i,j}^{(stat)},\text{clip}\left\{\delta_{i,j}^{(stat)},1\pm\varepsilon\right\}A_{i,j}^{(stat)}\right\}-\beta\mathbb{D}_{KL}(\pi_{\theta}\|\pi_{\theta_{ref}})\right),$ $$

$$ $\delta_{i,j}^{(stat)}=\frac{\pi_{\theta}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)}{\pi_{\theta_{old}}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)},$ (2) $$

$$ $\mathbb{D}_{KL}(\pi_{\theta}\|\pi_{\theta_{ref}})=\frac{\pi_{\theta_{ref}}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)}{\pi_{\theta}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)}-\log\frac{\pi_{\theta_{ref}}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)}{\pi_{\theta}\left(s_{i,j}^{(NL)}|\bm{s}_{i,j}^{(base)}\right)}-1$ (3) $$

where $\pi_{\theta}$ denotes the policy model with parameter $\theta$. It represents the statement fuser here. $\theta_{ref}$ is the parameter for base statement fuser, $\theta_{old}$ is the parameter for the fuser in the previous step, $\varepsilon$ and $\beta$ are hyper-parameters, and $A_{i,j}$ is the advantage, computed from the reward set $\bm{r}_{i}^{(stat)}=\{r_{i,j}^{(stat)}\}_{j=1}^{N_{i}}$ by:

$$ $A_{i,j}^{(stat)}=\frac{r_{i,j}^{(stat)}-\text{mean}(\bm{r}_{i}^{(stat)})}{\text{std}(\bm{r}_{i}^{(stat)})},\;r_{i,j}^{(stat)}=(1-p_{i,j})\cdot(1-m_{i,j})\cdot\mathbb{I}\{p_{i,j}\neq 0\}$ (4) $$

where $p_{i,j}$ is the prover’s empirical pass rate on $s_{i,j}^{(FL)}$, and $m_{i,j}$ is the statement modification rate, which indicates the portion of proofs that the prover tries to modify its statement. The reward is set to 0 if the prover fails to solve the problem, which indicates the statement is too difficult or unsolvable.

We introduce the term $1-m_{i,j}$ as a soft statement modification penalty to balance the risk between reward hacking and the need to preserve model capability. Because of Long CoT training, current expert provers often acquire strong self-correction capability. While valuable, this ability can lead the model to change formal statements during proof writing. This may lead to serious reward hacking if unconstrained. Conversely, a strict ban on such modifications would suppress self-correction and reduce proofreading accuracy. Our soft penalty discourages excessive statement change without too much harm to the result.

In summary, the training design for the statement fuser rewards the model to lower the prover’s pass rate by composing more challenging statements.

#### 2.2.2 Prover Training

To achieve adverasrial training, the prover is optimized to maxmize the pass rate on generated statements. We employ a variant of the GRPO algorithm for such training. Specifically, for each theorem statement $\bm{s}_{i,j}=(s_{i,j}^{(NL)},s_{i,j}^{(FL)})$, we update the prover model $Prover_{i-1}$ by maximizing the following objective function:

$$ $\displaystyle\mathcal{J}_{GRPO}^{(P)}(\omega)$ $\displaystyle=\mathbb{E}_{\left[\{o_{i,j,k}\}_{k=1}^{n}\sim\pi_{\omega_{old}}(\bm{s}_{i,j})\right]}$ (5) $\displaystyle\frac{1}{n}\sum_{k=1}^{n}\left(\min\left\{\delta_{i,j,k}^{(pr)}A_{i,j,k}^{(pr)},\text{clip}\left\{\delta_{i,j,k}^{(pr)},1\pm\varepsilon\right\}A_{i,j,k}^{(pr)}\right\}-\beta\mathbb{D}_{KL}(\pi_{\omega}\|\pi_{\omega_{ref}})\right),$ $$

$$ $\delta_{i,j,k}^{(proof)}=\frac{\pi_{\omega}\left(o_{i,j,k}|\bm{s}_{i,j}\right)}{\pi_{\omega_{ref}}\left(o_{i,j,k}|\bm{s}_{i,j}\right)}$ (6) $$

where $\pi_{\omega}$ is the prover as policy model, $\omega$ is the parameter of prover, and $A_{i,j,k}$ is the advantage of proof $o_{i,j,k}$, computed from the reward set $\bm{r}_{i,j}^{(proof)}=\{r_{i,j,k}^{(proof)}\}_{k=1}^{n}$ by:

$$ $A_{i,j,k}^{(proof)}=\frac{r_{i,j,k}^{(proof)}-\text{mean}(\bm{r}_{i,j}^{(proof)})}{\text{std}(\bm{r}_{i,j}^{(proof)})},\;r_{i,j,k}=1-0.5\cdot m_{i,j,k}$ (7) $$

where $m_{i,j,k}$ is a binary indicator of whether a statement modification occurred in proof $o_{i,j,k}$. Similar to the training of the statement fuser, modifications are penalized but not strictly prohibited. Furthermore, to ensure the prover is trained on high-quality data, we exclude statements with an empirical pass rate of 0 (unsolvable) or above $0.5$ (too easy) following experience in Wang et al. (2025a); Dong & Ma (2025b). It make sure the prover is only trained with hard and medium-level problems. This optimization scheme drives the prover to compete with the statement fuser by continually enhancing its proof-generation capability.

### 2.3 Summary

The GAR is an iterative framework that loops the generation stage and the RL stage details above. To provide a clear overview, we present the complete framework in the form of pseudo-code as follows:

Figure: Algorithm 1 GAR

When trained in multiple iterations, the GAR establishes an implicit curriculum by aligning statement difficulty with the prover’s evolving capability. The statement fuser is trained to reduce the pass rate by generating more challenging statements, while the prover is optimized to increase it by producing more valid proofs. Together, their adversarial interaction drives progressive improvement.

## 3 Experiments

We conduct comprehensive experiments on the MiniF2F-Test (Zheng et al., 2021) and ProofNet-Test (Azerbayev et al., 2023) benchmarks to assess the performance of the GAR framework in formal proof writing. Specifically, we show in Section [3.3](https://arxiv.org/html/2510.11769v1#S3.SS3) that the models trained with GAR achieve better empirical results, confirm in Section [3.4](https://arxiv.org/html/2510.11769v1#S3.SS4) that adversarial training induces an implicit curriculum by generating progressively harder statements, and report ablation study results in Section [3.5](https://arxiv.org/html/2510.11769v1#S3.SS5). Due to space limitations, we have included the efficiency study and case study in Appendix [B](https://arxiv.org/html/2510.11769v1#A2).

### 3.1 Experiment Setup

#### 3.1.1 Dataset and Task

We measure the Lean4 reasoning capability of the GAR trained model by MiniF2F-Test (Zheng et al., 2021) and ProfNet-Test (Azerbayev et al., 2023) benchmarks. They are challenging benchmarks and adopted in nearly all major studies in the field (Xin et al., 2024b; Lin et al., 2024; Wang et al., 2024; Wu et al., 2024a; Polu et al., 2022; Dong & Ma, 2025a; Lin et al., 2025b; Wang et al., 2025c).

**Table 1: Main experimental results of GAR trained models compared to recent provers models.**
| Method | Sample budget | MiniF2F-Test | ProofNet-Test |
| --- | --- | --- | --- |
| Lean-STaR (Lin et al., 2024) | $64\times 1\times 50$ | 46.31% | - |
| InternLM-2.5-StepProver (Wu et al., 2024a) | $4\times 32\times 600$ | 50.70% | 18.80% |
| DeepSeek-Prover-V1.5-RL (Xin et al., 2024b) | 128 | 50.00% | 18.20% |
| STP-Lean (Dong & Ma, 2025b) | 128 | 56.15% | 19.50% |
| MA-LoT (Wang et al., 2025c) | 32 | 61.07% | 15.47% |
| Kimina-Prover-Distill-7B (Wang et al., 2025a) | 32 | 63.10% | - |
| DeepSeek-Prover-V2-7B (Ren et al., 2025) | 32 | 70.49% | 22.58% |
| Geodel-Prover-V2-8B (Lin et al., 2025a) | 32 | 77.87% | - |
| Our models |  |  |  |
| GAR on Deepseek-Prover-V2 | 32 | 74.18% | 25.81% |
| GAR on Goedel-Prover-V2 | 32 | 80.33% | - |

**Table 2: Average proof correctness rate for Goedel-Prover-V2-8B (base model) and GAR model trained on base model.**
| Step idx | Base Model | GAR model |
| --- | --- | --- |
| 0 | 29.16% | 29.16% |
| 1 | 16.50% | 23.71% |
| 2 | 11.58% | 20.53% |
| 3 | 7.61% | 20.08% |
| 4 | 7.69% | 21.79% |

The MiniF2F-Test benchmarks comprise 244 Lean4 statements, spanning from high school competition problems to elementary undergraduate-level theorem proofs. Specifically, MiniF2F-Test comprises problems formalized from the MATH dataset (Hendrycks et al., 2021), high school competitions such as AMC, AIME, and IMO, as well as self-crafted problems. ProofNet-Test consists of 186 theorems formalized from standard undergraduate textbooks on advanced topics such as real and complex analysis, linear algebra, abstract algebra, and topology. In our setting, we train the LLM with GAR to generate Lean4 proofs from the NL-FL statement pair. To avoid overloading the model, all the imports and namespaces are manually configured.

#### 3.1.2 Baselines

To evaluate the effectiveness of GAR, we compare it against strong open-source baselines, including Lean-STaR (Lin et al., 2024), InternLM-2.5-StepProver (Wu et al., 2024a), Kimina-Prover-Preview-Distill-7B (Wang et al., 2025a), DeepSeek-Prover-V1.5-RL (Xin et al., 2024b), STP-Lean (Dong & Ma, 2025a), MA-LoT (Wang et al., 2025c), Goedel-Prover-V2 (Lin et al., 2025b), and DeepSeek-Prover-V2 (Ren et al., 2025). For baseline models that require Long CoT reasoning (Kimina-Prover, MA-LoT, DeepSeek-Prover-V2, and Goedel-Prover-V2), we restrict the reasoning length to 16,384 tokens to conserve computational resources.(^1^11Because of this restriction, our reported results for DeepSeek-Prover-V2 and Goedel-Prover-V2 differ from those in the original papers, where the evaluations used a context length of 40,960.)

### 3.2 Implementation Details

In the generation stage, we construct a repository of 793,243 NL statements from Numina-Math (LI et al., 2024) and Lean-Workbook (Ying et al., 2024) datasets. For statement fusion, we employ Qwen3-8B (Team, 2025) as the base model for the statement fuser because of its skip-thinking capability. We apply Kimina-Autoformalizer-7B (Wang et al., 2025a) as the autoformalizer. For proof generation, we use DeepSeek-Prover-V2-7B (Ren et al., 2025) and Goedel-Prover-V2 (Lin et al., 2025b) as base models for provers.
We sample 1,024 theorems per step and generate 16 proofs per theorem following (Wang et al., 2025a). We also restrict the sequence length to 16,384 tokens for both models. The GRPO hyperparameters are set with a learning rate of 2E-6, $\varepsilon=0.2$, and $\beta=0.01$.
We perform three iterations of GAR training on Goedel-Prover-V2 and five iterations on DeepSeek-Prover-V2, which costs around 140 H100 hours for each training. On average, DeepSeek-Prover-V2 costs fewer hours per iteration due to average shorter thinking. In verification, any proof involving statement modification or relying on the “sorry” or “admit” tactic is counted as incorrect to ensure fairness.

### 3.3 Results

Table [1](https://arxiv.org/html/2510.11769v1#S3.T1) demonstrates the empirical results of applying GAR to train base prover models. For Goedel-Prover-V2, MiniF2F-Test pass@32 raises to 80.33%, indicating a 3.16% relative gain. For DeepSeek-Prover-V2, the MiniF2F-Test score improves to 74.18%, corresponding to a 5.23% increase. On the more challenging ProofNet-Test benchmark, which targets advanced mathematics topics, GAR enhances DeepSeek-Prover-V2’s pass@32 rate from 22.58% to 25.81%.(^2^22We do not report Goedel-Prover-V2’s accuracy on ProofNet due to the absence of the reference results in Lin et al. (2025b).)

Compared with other baselines, both the base model and the GAR-trained models achieve consistent and substantial gains, highlighting that GAR can contribute to models that already have outstanding performance. Compared to base models, the improvements suggest that the adversarial method proposed in GAR enables provers to tackle increasingly difficult problems by establishing an implicit curriculum.
Such a curriculum can progressively adapt problem difficulty to the model’s capability, allowing the prover to explore deeper reasoning strategies and solve more advanced theorems. This behavior becomes more significant as the theorems get harder.

### 3.4 Statement Fuser Study

To show that GAR produces increasingly more difficult statements across iterations and thereby establishes an implicit curriculum learning, we examine the difficulty of problems generated by the statement fuser. In each iteration, we randomly sample 50 generated statements and compute their average proof correctness rate using both the base prover and GAR-trained prover at that iteration. Details of the metric we used are provided in Appendix [A.2](https://arxiv.org/html/2510.11769v1#A1.SS2). The result of this experiment is reported in Table [3](https://arxiv.org/html/2510.11769v1#S3.T3).

From the results, we can observe that the base model exhibits a consistent performance degradation, with accuracy falling from 29.16% at the first iteration’s data to 7.69% by the fifth. In contrast, the GAR-trained model shows only a minor initial decline due to the statement matching but stabilizes at around 21% across later iterations. These findings confirm that GAR progressively generates harder statements, as evidenced by the base model’s decline. The maintained trained model’s performance demonstrates the adversarial training strength of the prover’s performance over time.

### 3.5 Ablation Studies

#### 3.5.1 Effect of statement modification penalty

We evaluate the impact of the statement modification penalty by monitoring statement modification rates across by the provers during training rounds. Details of this metric are provided in Appendix [A.3](https://arxiv.org/html/2510.11769v1#A1.SS3). We trained a variant of GAR on Goedel-Prover-V2-8B without the penalty in both the statement fuser and prover, and compared it with the full GAR.

**Table 4: Pass@32 results on MiniF2F-Test for Goedel-Prover-V2-8B and its GRPO and GAR trained version.**
| Method | MiniF2F-Test |
| --- | --- |
| Base model | 77.87% |
| GRPO trained | 77.46% |
| GAR trained | 80.33% |

Table [3](https://arxiv.org/html/2510.11769v1#S3.T3) shows that without the modification penalty, the prover exploits its self-correction ability by simplifying statements.
Such behavior worsens as the training progresses; by the fourth step, 74% of statements were modified at least once, which is a clear signal of reward hacking.
In contrast, with the penalty enabled, the modification rate remains below 40% throughout. This study confirms the effectiveness of our statement penalty in preventing reward hacking.

#### 3.5.2 Compare to Direct RL training

This experiment tests whether jointly evolving the prover and statement fuser is more effective than training the prover alone using existing data. We conducted three additional GRPO iterations on Goedel-Prover-V2-8B using the same sampling budget and formalized NL base dataset as GAR. The results are shown in Table [4](https://arxiv.org/html/2510.11769v1#S3.T4).
The GAR-tained model outperforms the variant trained with traditional GRPO. We conclude that such an improvement to GAR progressively raises problem difficulty, enabling the prover to handle more complex statements. In contrast, further RL training on static dataset degrades performance, as the base model is already heavily RL trained. These findings further support the generality of GAR, demonstrating is ability to enhance model’s performance while standard RL no longer provides benefits.

## 4 Related Work

### 4.1 LLM for Formal Theorem Proving

Recently, applying LLMs to support formal theorem proving has become a prominent research direction. Training approaches can be broadly divided into two categories: model trained solely with Supervised Fine-Tuning (SFT) and those combining SFT with Reinforcement Learning (RL). Early SFT-based provers include Expert Iteration (Polu & Sutskever, 2020), Re-Prover (Yang et al., 2024c), TheoremLlama (Wang et al., 2024), DeepSeek-Prover-V1 (Xin et al., 2024a), InternLM-2.5-StepProver (Wu et al., 2024a), MA-LoT (Wang et al., 2025c), and Goedel-Prover-V1 (Lin et al., 2025a). These models typically require multiple rounds of large-scale annotation with existing formal solvers, which demands a significant amount of computational resources and limits exploration. To further advance the prover, researchers began incorporating advanced RL techniques. For instance, DeepSeek-Prover-V1.5 (Xin et al., 2024b) employs DPO. After the ”ZERO” RL technique that enables Long CoT thinking developed by Guo et al. (2025), provers like Kimina-Prover (Wang et al., 2025a), DeepSeek-Prover-V2 (Ren et al., 2025), and Goedel-Prover-V2 (Lin et al., 2025b) enable models to produce better formal proof after thinking. However, existing RL approaches still rely on a fixed collection of statements, preventing statements from adapting to the prover’s evolving skill. In contrast, GAR jointly trains a statement fuser and a prover, ensuring that generated theorems remain suitably challenging as the model improves.

### 4.2 RL methods for LLM

RL has been central to the development of reasoning LLMs (Xiong et al., 2025). Early efforts such as DeepSeek-Math (Shao et al., 2024) and Qwen-2.5-Math (Yang et al., 2024a) applied reward modeling with GRPO algorithm to enhance exploration. The release of OpenAI-O1 (OpenAI, 2024) and DeepSeek-R1 (Guo et al., 2025) demonstrated that verifier-based rewards in RL can enable complex reasoning strategies, including backward search and self-correction. Such techniques have been widely adopted in systems like Qwen3 (Team, 2025) and Kimi-K2 (Team et al., 2025). Nevertheless, nearly all prior work uses the verification signal only to optimize the problem solver, leaving the problem composer untrained. On the other hand, GAR simultaneously improves both statement fuser and the prover, creating an implicit curriculum that adapts task difficulty and allows the model to acquire more complex reasoning skills step-by-step.

## 5 Conclusion

This paper presents GAR, a comprehensive training framework for formal theorem proving. GAR aims to resolve the inefficient and suboptimal performance caused by traditional expert iteration and online RL in prover training.
GAR achieves more efficient training by using statement fusion to formulate statements in the RL process to avoid the prover from annotating problems beyond its capability range. After GAR training, provers can solve more advanced problems through the implicit curriculum learning that enables the model to explore further.
Furthermore, GAR can improve the performance of models that have been through heavy RL training by letting the model explore more difficult statements during the training process.
Experiments of applying GAR to DeepSeek-Prover-V2 and Goedel-Prover-V2 yield an average relative improvement of 4.20% on the MiniF2F-Test dataset and improve the DeepSeek-Prover-V2’s performance on ProofNet-Test from 22.58% to 25.81%.
Beyond theorem proving, GAR offers a general RL paradigm of co-evolution of the problem generation and solving under a verifiable environment. It provides a foundation for adversarial co-training in other reasoning-intensive domains.

## References

- Azerbayev et al. (2023)
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad.
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.
*arXiv preprint arXiv:2302.12433*, 2023.
- Coq (1996)
Projet Coq.
The coq proof assistant-reference manual.
*INRIA Rocquencourt and ENS Lyon, version*, 5, 1996.
- De Moura et al. (2015)
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer.
The lean theorem prover (system description).
In *Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25*, pp. 378–388. Springer, 2015.
- Dong & Ma (2025a)
Kefan Dong and Tengyu Ma.
Beyond limited data: Self-play llm theorem provers with iterative conjecturing and proving.
*arXiv preprint arXiv:2502.00212*, 2025a.
- Dong & Ma (2025b)
Kefan Dong and Tengyu Ma.
Stp: Self-play llm theorem provers with iterative conjecturing and proving.
*arXiv preprint arXiv:2502.00212*, 2025b.
- Guo et al. (2025)
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al.
Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning.
*arXiv preprint arXiv:2501.12948*, 2025.
- Harrison (2009)
John Harrison.
Hol light: An overview.
In *International Conference on Theorem Proving in Higher Order Logics*, pp. 60–66. Springer, 2009.
- Hendrycks et al. (2021)
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt.
Measuring mathematical problem solving with the math dataset.
*arXiv preprint arXiv:2103.03874*, 2021.
- Jiang et al. (2022)
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample.
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.
*arXiv preprint arXiv:2210.12283*, 2022.
- LI et al. (2024)
Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu.
Numinamath.
[[https://huggingface.co/AI-MO/NuminaMath-CoT](https://github.com/project-numina/aimo-progress-prize/blob/main/report/numina_dataset.pdf)](%5Bhttps://huggingface.co/AI-MO/NuminaMath-CoT%5D(https://github.com/project-numina/aimo-progress-prize/blob/main/report/numina_dataset.pdf)), 2024.
- Lin et al. (2024)
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck.
Lean-star: Learning to interleave thinking and proving.
*arXiv preprint arXiv:2407.10040*, 2024.
- Lin et al. (2025a)
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin.
Goedel-prover: A frontier model for open-source automated theorem proving, 2025a.
URL [https://arxiv.org/abs/2502.07640](https://arxiv.org/abs/2502.07640).
- Lin et al. (2025b)
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*, 2025b.
- Moura & Ullrich (2021)
Leonardo de Moura and Sebastian Ullrich.
The lean 4 theorem prover and programming language.
In *Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28*, pp. 625–635. Springer, 2021.
- Newell & Simon (1956)
Allen Newell and Herbert Simon.
The logic theory machine–a complex information processing system.
*IRE Transactions on information theory*, 2(3):61–79, 1956.
- OpenAI (2024)
OpenAI.
Learning to reason with llms.
[https://openai.com/index/learning-to-reason-with-llms/](https://openai.com/index/learning-to-reason-with-llms/), September 13 2024.
Accessed: 2024-11-24.
- Paulson (1994)
Lawrence C Paulson.
*Isabelle: A generic theorem prover*.
Springer, 1994.
- Polu & Sutskever (2020)
Stanislas Polu and Ilya Sutskever.
Generative language modeling for automated theorem proving.
*arXiv preprint arXiv:2009.03393*, 2020.
- Polu et al. (2022)
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever.
Formal mathematics statement curriculum learning.
*arXiv preprint arXiv:2202.01344*, 2022.
- 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.
- Shao et al. (2024)
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al.
Deepseekmath: Pushing the limits of mathematical reasoning in open language models.
*arXiv preprint arXiv:2402.03300*, 2024.
- Team et al. (2025)
Kimi Team, Yifan Bai, Yiping Bao, Guanduo Chen, Jiahao Chen, Ningxin Chen, Ruijue Chen, Yanru Chen, Yuankun Chen, Yutian Chen, et al.
Kimi k2: Open agentic intelligence.
*arXiv preprint arXiv:2507.20534*, 2025.
- Team (2025)
Qwen Team.
Qwen3, April 2025.
URL [https://qwenlm.github.io/blog/qwen3/](https://qwenlm.github.io/blog/qwen3/).
- 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, et al.
Kimina-prover preview: Towards large formal reasoning models with reinforcement learning.
*arXiv preprint arXiv:2504.11354*, 2025a.
- Wang et al. (2024)
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang.
Theoremllama: Transforming general-purpose llms into lean4 experts.
*arXiv preprint arXiv:2407.03203*, 2024.
- Wang et al. (2025b)
Ruida Wang, Yuxin Li, Yi R Fung, and Tong Zhang.
Let’s reason formally: Natural-formal hybrid reasoning enhances llm’s math capability.
*arXiv preprint arXiv:2505.23703*, 2025b.
- Wang et al. (2025c)
Ruida Wang, Rui Pan, Yuxin Li, Jipeng Zhang, Yizhen Jia, Shizhe Diao, Renjie Pi, Junjie Hu, and Tong Zhang.
Ma-lot: Model-collaboration lean-based long chain-of-thought reasoning enhances formal theorem proving.
*arXiv preprint arXiv:2503.03205*, 2025c.
- Wu et al. (2024a)
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.
*arXiv preprint arXiv:2410.15700*, 2024a.
- Wu et al. (2024b)
Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen.
Lean-github: Compiling github lean repositories for a versatile lean prover.
*arXiv preprint arXiv:2407.17227*, 2024b.
- 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.
*arXiv preprint arXiv:2502.03438*, 2025.
- Xiong et al. (2025)
Wei Xiong, Jiarui Yao, Yuhui Xu, Bo Pang, Lei Wang, Doyen Sahoo, Junnan Li, Nan Jiang, Tong Zhang, Caiming Xiong, et al.
A minimalist approach to llm reasoning: from rejection sampling to reinforce.
*arXiv preprint arXiv:2504.11343*, 2025.
- Yang et al. (2024a)
An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, Keming Lu, Mingfeng Xue, Runji Lin, Tianyu Liu, Xingzhang Ren, and Zhenru Zhang.
Qwen2.5-math technical report: Toward mathematical expert model via self-improvement.
*arXiv preprint arXiv:2409.12122*, 2024a.
- Yang et al. (2024b)
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song.
Formal mathematical reasoning: A new frontier in ai.
*arXiv preprint arXiv:2412.16075*, 2024b.
- Yang et al. (2024c)
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar.
Leandojo: Theorem proving with retrieval-augmented language models.
*Advances in Neural Information Processing Systems*, 36, 2024c.
- Ying et al. (2024)
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen.
Lean workbook: A large-scale lean problem set formalized from natural language math problems.
*arXiv preprint arXiv:2406.03847*, 2024.
- 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 Details of the metrics

For completeness, this section provides the metric definitions that were omitted due to space limitations in Section [3](https://arxiv.org/html/2510.11769v1#S3).

### A.1 Pass Rate

Pass@$x$ is a widely used metric for evaluating formal theorem provers (Polu et al., 2022; Jiang et al., 2022; Wang et al., 2024; Xin et al., 2024a; Dong & Ma, 2025b; Wang et al., 2025b; Lin et al., 2025b; Wu et al., 2024a; Wang et al., 2025a; b). For each theorem statement, the model generates $x$ candidate proofs, which are further checked by the Lean4 verifier. If at least one of the $x$ candidates is correct, the theorem is counted as a proved theorem. The pass@$x$ of the LLM is the fraction of theorems in the dataset with at least one correct proof generated by the prover.

### A.2 Average proof correctness rate

This metric measures the relative difficulty of a set of statements for a given prover, which is used in Section [3.4](https://arxiv.org/html/2510.11769v1#S3.SS4)). Let $\mathcal{D}$ be a dataset of size $m$. For each theorem $t_{i}\in\mathcal{D}$, we sample 16 proofs from the prover and record the number of proofs that pass the verification, which is $p_{i}$. The average proof correctness rate is calculated by

$$ $\frac{\sum_{i=1}^{m}p_{i}}{16\cdot m}$ $$

A high value indicates the dataset is easier for the given prover.

Note that in this experiment, to demonstrate the significance of GAR better, we train two extra rounds of Goedel-Prover-V2-8B model.

### A.3 Statement modification rate

Since current advanced provers have Long Chain-of-thought (CoT) capability, which enables self-reflection, backtracking, and self-correction. In the Long CoT process, a prover may alter the original statement into a simplified variant in its reasoning trace and ultimately produce a proof for the modified version. To quantify this behavior, we define statement modification rate as the portion of theorems in a dataset that have at least one statement modification across 16 generated proofs. This metric helps assess how often the prover attempts to modify the problem and whether such a behavior may be too significant to cause severe reward hacking.

## Appendix B Additional experiments

This appendix section provides additional experiments that are omitted in the main paper due to space limitations.

### B.1 Efficiency Study

We analyze the computational efficiency of the GAR framework, as training from scratch demands substantial resources, to evaluate this, we compare our approach with Kimina-Prover (Wang et al., 2025a), selected for its transparent reporting of training details. The number of roll-out theorems and proofs per iteration in  Wang et al. (2025a) matches our configuration. From Figure 4 in their work, we observe that Kimina-Prover achieves approximately 2% of performance gains after 25 training iterations, where GAR trained Goedel-Prover-V2-8B reaches more improvements in merely three iterations. This comparison demonstrates the computational efficiency of our adversarial training paradigm. However, since current Long CoT provers have already undergone extensive RL optimization, prolonged additional RL training could degrade their performance. Given resource constraints preventing exhaustive experimentation, we leave the discussion of scalability of GAR to future works.

### B.2 Case study

#### B.2.1 Case 1:

In this section, we demonstrate an example of how the GAR trained model successfully solves the problem while the base models fail. Compared to the base prover, the GAR trained model relies less on brute simplification and more on early structural framing, producing shorter, steadier proof traces that remain faithful to the statement and are more likely to pass the verification. If we dig deeper into the Long CoT of two models, we can find that GAR-trained prover writes a shorter and more focused long CoT. While the base model’s CoT is longer but less directed, it cycles among general identities and simplifications without stabilizing on a closing invariant. The result that GAR’s trace is both and clearer and more verifiable, which leads to the successful proof.

GAR-trained model generated result:

Base model generated result:

#### B.2.2 Case 2:

In another ProofNet example, GAR again succeeds where the base prover fails. This instance more clearly illustrates how GAR mitigates useless simplifications. It uses NLs to reach a comprehensive proof plan and effectively conduct the proof in a relatively simple manner. However, the base model conducts a quicker search but a prolonged proof. It expends effort on low-yield algebra and yields lengthy, fragile derivations. These observations highlight that the implicit curriculum in GAR fosters more efficient reasoning paths and greater verification robustness.

GAR-trained model generated result:

Base model generated result:

## Peer Reviews

confidence: 4
contribution: 2
initial_rating: 6
presentation: 3
questions: N/A
soundness: 3
strengths: * The paper addresses a critical bottleneck in current neural theorem provers, i.e., the reliance on a fixed and limited set of theorem statement. Having the model conjecturing and proving new statement is a promising direction. The design space here is quite big, and GAR represents one reasonable method in this space.
* Experiments show good improvements on MiniF2F and ProofNet.
summary: The paper introduces GAR (Generative Adversarial Reinforcement Learning) for formal theorem proving in Lean. Unlike traditional expert iteration or RL for theorem proving with a fixed statement set, GAR dynamically generate new statements at the right difficulty level for the prover, forming an implicit curriculum. The method consists of a composer that generates new statements by fusing existing statements and a prover. Both components are trained with RL. The composer is incentivized to generate statements that are challenging but provable for the current prover. Experiments on MiniF2F and ProofNet shows improvements to the prover's capability.
weaknesses: * GAR is not the first attempt to augment the set of formal statements. For example, the scaffolded data synthesis in Goedel-Prover-V2 tries to generate simpler variants of hard problems and harder variants of simple problems. STP also generates new statements based on existing statements. The fuser in this paper is different from those methods, but it would be great if the authors can make the comparison more explicit. 
* MiniF2F is already saturated. SOTA methods are close to 100%. Experiments on PutnamBench would make this paper much stronger.

---

confidence: 5
contribution: 3
initial_rating: 8
presentation: 4
questions: - Can you expand on the issue of <analysis> ?
- Why the statement modification loss and not simply freezing the statement (and punishing any modifications as fully incorrect)? Doesn't this give an optimal policy that is not intended? Why doesn't that happen in practice?

Nits:
eq 7: r_{ijk} needs a correctness term instead of 1?
Alg. 1: typo in line 7
soundness: 4
strengths: The method is sensible, the numbers are very good, the paper is very clearly written.
The scope is limited because there are many ways of generating synthetic statements and there was no comparison to other synthetic data methods (STP, Magicoder), but it appears that the authors have found a particularly effective method for this.
summary: The paper proposes a variant of self-play theorem proving (conjecturer-prover adversarial training) where the conjecturer fuses two statements to create a statement with higher difficulty "Composability" is a frequently observed problem in LLMs, and the method directly tackles this issue. With small budgets of additional training, the method improves the initial already highly optimized models by a significant margin.
weaknesses: No comparisons to other synthetic data generation methods.

---

confidence: 3
contribution: 2
initial_rating: 6
presentation: 3
questions: Regarding Table 1, could you please explain why your reported results for previous works (Kimina, Deepseek, Goedel) are all significantly lower than those in their original papers? Did you encounter any issues with your experimental setup, such as a different Lean version, that might account for this mismatch?
soundness: 3
strengths: The overall quality and clarity of this work are good. Its motivation and methodology are described in detail. The proposed method also demonstrates significance, as it is potentially applicable to domains beyond automated theorem proving.
summary: This work introduces a novel RL framework (GAR) that trains not only a solver, but also a fuser designed to generate new problems suitable for the solver's current training stage. To be specific, in the context of automated theorem proving, the prover (solver) is trained to solve problems. Concurrently, the fuser attempts to generate problems that are provable in Lean (by the current provers) but possess a relatively low pass rate, thus making them "difficult but approachable." The fuser is also trained during the RL process, creating an adversarial environment. The experimental results demonstrate the effectiveness of this method.
weaknesses: Regarding novelty, the idea of generating problems with appropriate difficulty levels has been explored by prior works, such as STP and Goedel-Prover-V2. STP, in particular, also trained a model to generate new problems in an adversarial way. The main difference appears to be that this work uses RL, whereas STP used expert iteration (SFT). This overlap weakens the originality and significance of the current paper.

Additionally, some experimental results in Table 1 are questionable. It appears that the reported results for prior works are all much lower than those originally published in their respective papers.

---

confidence: 4
contribution: 2
initial_rating: 6
presentation: 3
questions: The reported statement-modification rate under full GAR (around 30–50%) seems unreasonably high. Since this behavior reflects an instruction-following failure rather than a Lean reasoning limitation, and your prover prompt is identical to the official prompts of DeepSeek-Prover-V2 and Goedel-Prover-V2, there is no prompt-shift factor that could explain it.
   
Please therefore report:
   - the modification rates of DeepSeek-Prover-V2 and Goedel-Prover-V2 under their original prompts (no GAR); and
   - the corresponding rate of the GAR-trained prover under the same prompts.

Such a comparison is important, because a statement-modification rate this high, combined with a relatively small sample size (pass@32), yet still achieving strong benchmark performance, is highly questionable.
soundness: 2
strengths: * Novel formulation: The paper introduces a clear and well-motivated adversarial training paradigm for formal theorem proving, aligning problem difficulty with prover capability.
* Empirical gains: GAR achieves measurable and consistent improvements on competitive baselines, even when those baselines are already heavily RL-trained.
* Clarity and reproducibility: The training procedure, algorithmic structure, and implementation details are well described, with clear experimental setups and evaluation metrics.
* Significance: The proposed paradigm is general and could influence future work on co-evolving reasoning models in other verifiable domains.
summary: This paper presents Generative Adversarial Reinforcement learning, a framework for adversarial co-training of theorem provers and problem generators in the Lean environment.
GAR jointly optimizes a statement fuser that composes new mathematical statements and a prover that attempts to prove them, forming a self-improving loop. In each iteration, the fuser generates new, harder statements by combining two natural-language problems from a large dataset from Numina-Math and Lean-Workbook, which are then automatically formalized into Lean. The prover produces proofs for these statements, and Lean verification provides reward signals to both models.

Through this interaction, the fuser learns to propose “hard but solvable” problems while the prover learns to solve increasingly challenging ones. The framework yields consistent improvements over strong RL-trained baselines on MiniF2F and ProofNet, and demonstrates that jointly evolving generators and solvers can outperform direct reinforcement learning on static datasets.
weaknesses: 1. Lack of a frozen-fuser control:
   The paper always updates both the fuser and the prover in each GAR iteration. A variant that keeps the fuser fixed (for example, using the initial fuser) while training only the prover is missing. This is necessary to determine whether the gains derive from adversarial co-adaptation or simply from exposure to more generated data.

2. Absence of an SFT-only baseline:
   All experiments start from provers that have already undergone heavy RL fine-tuning. It remains unclear whether GAR would still provide improvement if applied directly to a purely SFT-trained prover. This limits understanding of GAR’s generality and its effectiveness from weaker starting points.

3. No comparison with single-input statement generation:
   The current fuser fuses two NL statements into one new problem. There is no experiment showing what happens if the model generates or rewrites new statements from a single input problem (similar to iterative conjecturing). This ablation would clarify whether the two-input fusion design is critical to the observed gains.

4. Ambiguity in the Statement Fuser study:
   The difficulty analysis (Table 2) evaluates only problems produced by the evolving fuser—the same distribution used to train the GAR prover. The observed decline in base-prover accuracy might reflect distributional or stylistic shift rather than genuine difficulty increase. A control using random samples from Dstat would help validate the claimed implicit curriculum effect.

5. Limited exploration of the statement-modification penalty:
   The ablation in Table 3 removes penalties from both the fuser and the prover simultaneously, but does not include one-sided removals or a hard-ban condition. The paper would benefit from a more granular investigation of these choices.

6. Unfair efficiency comparison:
   The efficiency discussion (Appendix B.1) compares GAR, built upon already RL-trained long-CoT provers, with Kimina-Prover, which is trained from SFT. Because the starting points differ significantly, the efficiency claim is not directly justified.


Decision: Accept (Poster)