GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

• Formal languages such as Lean and Coq make intermediate mathematical reasoning steps verifiable, but mastering them requires expertise in complex type matching and constrained functions.Source: §1 · p. 1
• Prior RL and expert-iteration methods mostly optimize the prover on fixed statement sets, wasting effort on trivial or unsolvable tasks and lacking adaptive difficulty for complex theorems.Source: §1 · p. 2
• GAR jointly trains the statement fuser and prover adversarially: the fuser is rewarded for difficult yet solvable statements, while the prover is rewarded for proving medium- and high-difficulty problems.Its two stages are statement generation and adversarial RL, creating an implicit curriculum that adjusts difficulty as the prover develops.Source: §1 · pp. 2–3
• GAR yields 4.20% average relative improvement on MiniF2F-Test (Zheng et al., 2021) and raises DeepSeek-Prover-8B pass@32 on ProofNet-Test (Azerbayev et al., 2023) from 22.58% to 25.81%.Source: §1 · p. 3
• Statement Fusion creates novel formal statements beyond direct formalization of natural-language problems, producing theorems better aligned with model capability.The fuser synthesizes harder statements from existing solvable ones.Source: §1 · pp. 2–3
• GAR is presented as a general RL paradigm for co-evolving problem generation and solving in verifiable environments, with potential relevance to other reasoning-intensive domains.Source: §1 · p. 3

2.1 GENERATION STAGE

• The generation stage combines statement fusion, which produces new statements, with proof writing, which generates and evaluates candidate proofs.Source: §2.1 · p. 3

2.1.1 STATEMENT FUSION

• Statement fusion samples two natural-language statements from a 793,243-statement repository, combines their key ideas, then formalizes the result in Lean and checks compilation.The fuser is trained in the prior iteration, or initialized from a base model at iteration zero; fusing natural-language statements first addresses general LLMs’ limited understanding of formal language.Source: §2.1.1 · pp. 3–4

2.1.2 PROOF WRITING

• For each fused natural-language/formal-language pair, the prover generates 16 candidate proofs, which Lean4 verifies to compute the statement’s empirical pass rate.That pass rate is used for reward assignment.Source: §2.1.2 · p. 4

2.2 ADVERSARIAL REINFORCEMENT LEARNING

• The adversarial reinforcement-learning stage optimizes the fuser to reduce prover pass rates and the prover to increase them using generated statements.Both models use variants of GRPO.Source: §2.2 · p. 4, §2.2.1 · p. 5, §2.2.2 · p. 5

2.2.1 STATEMENT FUSER TRAINING

• The fuser is rewarded for producing challenging but solvable statements, with zero reward when the prover cannot solve a problem and a soft penalty for statement modifications.The implementation generates N = 1024 statements per step; the modification penalty balances reward hacking risk against preserving self-correction.Source: §2.2.1 · pp. 4–5

2.2.2 PROVER TRAINING

• The prover maximizes its pass rate on generated statements, while training excludes unsolvable problems and those with pass rates above 0.5.Statement modifications are penalized but not prohibited, and the retained problems are hard or medium-level.Source: §2.2.2 · pp. 5–6

2.3 SUMMARY

• Across iterations, the fuser makes statements harder while the prover improves proof generation, creating an implicit curriculum matched to evolving capability.GAR loops generation and reinforcement learning to drive this mutual improvement.Source: §2.3 · p. 6

3.1.1 DATASET AND TASK

• MiniF2F-Test covers 244 Lean4 statements from competition through undergraduate level, while ProofNet-Test has 186 textbook theorems; GAR trains Lean4 proof generation from NL-FL statement pairs.The evaluation manually configures imports and namespaces to avoid overloading the model.Source: §3.1.1 · pp. 6–7

3.3 RESULTS

• MiniF2F-Test pass@32 reaches 80.33% for Goedel-Prover-V2 (3.16% relative gain) and 74.18% for DeepSeek-Prover-V2 (5.23% increase); ProofNet-Test rises from 22.58% to 25.81%.The authors attribute gains to an implicit curriculum that adapts problem difficulty to prover capability, with stronger effects on harder theorems.Source: Table 1 · p. 7, §3.3 · p. 8

3.4 STATEMENT FUSER STUDY

• Base-prover correctness on generated statements falls from 29.16% to 7.69% across iterations, while the GAR-trained prover stabilizes around 21%, supporting progressively harder statement generation.The study samples 50 statements per iteration and evaluates their average proof correctness with the base and iteration-matched GAR-trained provers.Source: Table 2 · p. 7, §3.4 · p. 8

3.5.1 EFFECT OF STATEMENT MODIFICATION PENALTY

• Without the statement modification penalty, 74% of statements are modified at least once by the fourth step; with the penalty, the modification rate stays below 40% throughout.The authors interpret the unpenalized behavior as reward hacking through statement simplification.Source: Table 3 · p. 7, §3.5.1 · p. 8

3.1.2 BASELINES

• GAR is compared with eight open-source provers; Long-CoT baselines are capped at 16,384 tokens, so reported Goedel and DeepSeek results differ from original 40,960-token evaluations.Baselines include Lean-STaR, InternLM-2.5-StepProver, Kimina-Prover-Preview-Distill-7B, DeepSeek-Prover-V1.5-RL, STP-Lean, MA-LoT, Goedel-Prover-V2, and DeepSeek-Prover-V2.Source: §3.1.2 · p. 7, §3.2 · p. 7

3.2 IMPLEMENTATION DETAILS

• GAR uses a 793,243-statement repository and samples 1,024 theorems with 16 proofs per theorem per step; training runs three/five iterations at about 140 H100 hours each.Qwen3-8B fuses statements, Kimina-Autoformalizer-7B formalizes them, and Goedel-Prover-V2 and DeepSeek-Prover-V2 generate proofs; GRPO uses learning rate 2E-6, ε = 0.2, and β = 0.01. Modified statements and proofs using sorry or admit count as incorrect.Source: §3.2 · pp. 7–8

3.5.2 COMPARE TO DIRECT RL TRAINING

• With the same sampling budget and formalized NL base dataset, GAR outperforms three additional GRPO iterations on Goedel-Prover-V2-8B, while further RL on static data degrades performance.The authors conclude that jointly evolving the prover and statement fuser helps when standard RL no longer provides benefits.Source: Table 4 · p. 8, §3.5.2 · pp. 8–9

4.1 LLM FOR FORMAL THEOREM PROVING

• Existing theorem provers moved from SFT to RL but still use fixed statement collections, whereas GAR trains a statement fuser alongside the prover.The passage notes that SFT systems require repeated large-scale annotation with formal solvers, while fixed statements cannot adapt to the prover’s evolving skill.Source: §4.1 · p. 9

4.2 RL METHODS FOR LLM

• Verifier-based RL has enabled complex reasoning strategies, but prior work generally optimizes only the solver; GAR trains both the statement fuser and prover to create an implicit curriculum.The curriculum adapts task difficulty and supports step-by-step acquisition of more complex reasoning skills.Source: §4.2 · p. 9

5 CONCLUSION

• GAR yields an average relative improvement of 4.20% on MiniF2F-Test for DeepSeek-Prover-V2 and Goedel-Prover-V2, and raises DeepSeek-Prover-V2 on ProofNet-Test from 22.58% to 25.81%.The paper also frames GAR as a way to improve models that have already undergone heavy RL training by letting them explore more difficult statements.Source: §5 · p. 9
• Statement fusion formulates statements during RL to avoid having the prover annotate problems beyond its capability range.Implicit curriculum learning then enables provers to explore further and solve more advanced problems.Source: §5 · p. 9
• GAR offers a general RL paradigm for co-evolving problem generation and solving under verifiable environments, with a foundation for adversarial co-training in other reasoning-intensive domains.Source: §5 · p. 9

ETHICS STATEMENT

• The research uses publicly available mathematical datasets without human subjects, private data, or sensitive content, and LLMs only for writing polish and grammar fixes.The authors state that the work focuses exclusively on formal theorem proving.Source: ETHICS STATEMENT · p. 10

REPRODUCIBILITY STATEMENT

• The paper documents GAR’s pseudocode, data source, rewards, and training objectives, describes benchmarks, baselines, base model, and hyperparameters, and plans to open-source the code.Framework details are in Section 2; experimental setup is in Sections 3.1 and 3.2.Source: REPRODUCIBILITY STATEMENT · p. 10

B DETAILS OF THE METRICS

• The metrics appendix provides definitions omitted from Section 3 due to space limitations.Source: B DETAILS OF THE METRICS · p. 13

B.1 PASS RATE

• Pass@x is a widely used metric for evaluating formal theorem provers.Source: §B.1 · p. 13
• For each theorem statement, the model generates x candidate proofs.Source: §B.1 · p. 13
• The generated candidate proofs are checked by the Lean4 verifier.Source: §B.1 · p. 13
• A theorem counts as proved if at least one of the x candidate proofs is correct.Source: §B.1 · p. 13
• Pass@x is the fraction of dataset theorems for which the prover generates at least one correct proof.Source: §B.1 · p. 13

B.2 AVERAGE PROOF CORRECTNESS RATE

• The average proof correctness rate is the number of verified proofs among 16 samples per theorem, averaged over a dataset of m theorems; higher values indicate an easier dataset for that prover.For this experiment, the authors trained Goedel-Prover-V2-8B for two extra rounds to better demonstrate GAR’s significance.Source: §B.2 · p. 13

B.3 STATEMENT MODIFICATION RATE

• Statement modification rate is the share of dataset theorems with at least one statement modification across 16 generated proofs.This measures how often a prover modifies problems during long-CoT reasoning, which can indicate potentially severe reward hacking.Source: §B.3 · p. 13
• The statement modification measure is intended to assess whether problem changes during long-CoT reasoning occur often enough to cause severe reward hacking.The motivating behaviors include self-reflection, backtracking, and self-correction; a prover may alter a statement to a simplified variant and prove that modified version.Source: §B.3 · p. 13

C DIRECT COMPARISON WITH RELATED WORKS

• GAR continuously updates its statement fuser through adversarial RL, keeping generated statements challenging and aligned with the prover’s evolving skill, unlike Goedel-Prover-V2’s static RL statement set.Goedel-Prover-V2 uses a frozen large model to synthesize SFT data (Lin et al., 2025b); the passage says GAR’s approach leads to better empirical performance.Source: C DIRECT COMPARISON WITH RELATED WORKS · pp. 13–14
• GAR’s online RL cycle lets its fuser and prover update continuously, achieving superior performance without STP’s large per-iteration data-generation burden.STP uses expert iteration based on offline SFT and generates 75,000 conjectures per iteration, according to Dong & Ma (2025b).Source: C DIRECT COMPARISON WITH RELATED WORKS · p. 14

D ADDITIONAL EXPERIMENTS

• The appendix contains additional experiments omitted from the main paper because of space limitations.Source: D ADDITIONAL EXPERIMENTS · p. 14

D.1 RESULTS ON PUTNAMBENCH

• GAR-trained DeepSeek-Prover solves four additional PutnamBench problems compared with the base model under pass@32.The evaluation compares DeepSeek-Prover-V2-7B with the GAR-trained model on this challenging benchmark.Source: §D.1 · p. 14
• The authors describe the improvement across MiniF2F, PutnamBench, and ProofNet as evidence of GAR’s robust implicit curriculum.Source: §D.1 · p. 14

D.2 EFFICIENCY STUDY

• GAR-trained Goedel-Prover-V2-8B achieved more improvement in three iterations than Kimina-Prover’s approximately 2% gain after 25 iterations.Kimina-Prover starts from an SFT model, whereas GAR starts from a heavily RL-trained model; the paper describes GAR’s gains on RL-optimized models in 3–5 iterations as evidence of sample efficiency.Source: §D.2 · p. 14
• The paper leaves GAR’s scalability for future work because resource constraints prevented exhaustive experimentation.Source: §D.2 · p. 15

D.3 STATEMENT MODIFICATION RATE STUDY

• In MiniF2F-Test pass@32, higher statement-modification rates accompanied Goedel’s performance gains, while GAR raised low rates and controlled high rates through a soft penalty.The authors attribute Goedel’s increased modification rate to stronger self-correction and say the penalty discourages simplifying problems to triviality.Source: §D.3 · p. 15

D.4.1 FROZEN FUSER STUDY

• After three iterations on Goedel-Prover-V2-8B, frozen-fuser GAR yielded no performance improvement over the base model, supporting the need for co-evolution.The study trained the prover while keeping the statement fuser untrained.Source: §D.4.1 · p. 15

D.4.2 SINGLE PROBLEM ENHANCEMENT FUISER

• Replacing the statement fuser with MagicCoder’s single-problem restating strategy caused a 2.46% performance drop compared with the base model.The experiment replaced fusion of two problems with restating one problem to make it more advanced.Source: §D.4.2 · p. 15
• The authors attribute the single-problem strategy’s failure to Qwen3-8B’s limited ability to create advanced problems from one reference, whereas fusion combines concepts to form an implicit curriculum.Source: §D.4.2 · p. 15

D.5.1 CASE 1:

• The GAR-trained model solves the case theorem, whereas the base model fails to produce a successful proof.The example concerns proving that for prime p = 4t + 1, a is a primitive root modulo p iff -a is a primitive root modulo p.Source: §D.5.1 · pp. 15, 16, 20
• GAR relies more on early structural framing than brute simplification, producing shorter, steadier traces that remain faithful to the statement and are more likely to pass verification.Its long chain of thought is described as shorter and more focused.Source: §D.5.1 · pp. 15–16
• The base model’s longer chain of thought cycles through general identities and simplifications without stabilizing on a closing invariant.The passage contrasts this with GAR’s clearer, more verifiable trace.Source: §D.5.1 · pp. 15–16
• For prime p = 4*t + 1, IsPrimitiveRoot a p holds iff IsPrimitiveRoot (-a) p.The section states the result in Lean 4 as theorem exercise_4_4.Source: §D.5.1 · p. 22
• The Lean proof presents the forward and converse implications, then combines them to establish the biconditional.Source: §D.5.1 · pp. 22, 24

D.5.2 CASE 2:

• GAR proves that x^4 + 4x^3 + 6x^2 + 2x + 1 is irreducible in Z[x], succeeding where the base prover fails.The example is presented as illustrating how GAR mitigates useless simplifications.Source: §D.5.2 · p. 25
• The base model searches faster but takes longer to prove, spending effort on low-yield algebra and producing lengthy, fragile derivations.Source: §D.5.2 · p. 25
• GAR uses natural-language steps to form a comprehensive proof plan and carry out the proof relatively simply, illustrating more efficient reasoning and greater verification robustness.The paper attributes these qualities to GAR's implicit curriculum.Source: §D.5.2 · p. 25
• A proposed quadratic factorization yields a+c=4, ac+b+d=6, ad+bc=2, and bd=1, leaving only (b,d)=(1,1) or (-1,-1).These equations follow by expanding the factors and comparing coefficients.Source: §D.5.2 · p. 31
• For (b,d)=(1,1), the equations force a=c=2 and ad+bc=4, not 2; for (-1,-1), the resulting quadratic has discriminant -16.Both cases contradict the coefficient conditions or admit no integer roots.Source: §D.5.2 · p. 31
• The exhaustive search finds no factorization of the polynomial into two nonconstant integer polynomials, so it is irreducible.The analysis checks the possible quadratic factor cases and finds neither satisfies the coefficient conditions.Source: §D.5.2 · p. 31
• The Lean proof evaluates the factorization at 0, 1, -1, 2, and -2, then derives that both factors have degree at most 2.The code uses those evaluation constraints to enumerate the possible factor forms and derive a contradiction.Source: §D.5.2 · pp. 32, 34
• The proof-script fragment applies `norm_num at *` and `aesop`, then closes the goal with `exact h_main`.The excerpt ends with `norm_num at * <;> aesop exact h_main`.Source: §D.5.2 · p. 35