PaperlayerView exact revision on arXiv

Source-linked AI summary

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty

Yuchen Tian, Ruiyuan Huang, Xuanwu Wang, Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, Lun Du

arXiv:2510.00732v1cs.AI

TL;DR

Formal theorem provers face scarce high-quality training data, and LLMs can be fragile to minor changes in problem statements. The paper augments formal problems through domain, difficulty, and AST-based evolution, then trains EvolProver, which reports state-of-the-art results across several benchmarks.

  • Problem

    LLM theorem provers can be fragile to minor problem transformations, while formal proofs require scarce, expert-produced training data.

    Source: §1 · pp. 1–2

  • Method

    The paper combines LLM-guided cross-domain and difficulty evolution with AST-based equivalence rewrites, then trains EvolProver on the augmented data.

    Source: §1 · p. 2

  • Results

    EvolProver sets comparable-size-model SOTA on FormalMATH-Lite at 53.8% pass@32 and non-reasoning-model SOTA on MiniF2F-Test, Ineq-Comp-Seed, and Ineq-Comp-Transformed.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The results show that a non-reasoning model trained on evolved data achieves leading performance across multiple formal-theorem benchmarks.

    Source: §1 · p. 3, §6 · p. 10

Abstract

from arXiv · show

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

Formal theorem proving needs scarce expert-produced data, and LLM provers can be fragile to minor problem transformations. The paper introduces symmetry- and difficulty-based data evolution and reports strong benchmark results for EvolProver.

1 INTRODUCTION

  • The work addresses the scarcity of high-quality formal-proof training data, which requires substantial expertise and time to create.Lean, Coq, and Isabelle encode proofs as formal code requiring syntactic precision, logical soundness, and compiler verification.Source: §1 · p. 1
  • Minor problem transformations can sharply degrade model performance, motivating augmentation that addresses both symmetry and difficulty.The introduction gives transforming f(x) > g(x) into f(x) + f(y) > g(x) + g(y) as an example of a fragile transformation.Source: §1 · p. 2
  • EvolAST applies equivalence transformations to formal statements’ ASTs, producing syntactically diverse but semantically identical problems.Its transformation rules are based on mathematical axioms and theorems, and can be extended by encoding additional equivalences.Source: §1 · pp. 2–3
  • EvolDomain translates theorems across mathematical domains, while EvolDifficulty evolves them to broaden the range of problem difficulty.Both methods use LLM-guided evolutionary instructions.Source: §1 · p. 2
  • EvolProver reaches 53.8% pass@32 on FormalMATH-Lite, surpassing comparable-size models including reasoning models, and sets non-reasoning-model records on three other benchmarks.The reported rates are 69.8% on MiniF2F-Test, 52.2% on Ineq-Comp-Seed, and 34.0% on Ineq-Comp-Transformed; ablations show gains over unaugmented or partially augmented data, in some cases over 10 percentage points.Source: §1 · p. 3

2 RELATED WORKS

Prior work generates mathematical problems through rewriting, difficulty variation, and other synthesis strategies, while LLM robustness to small perturbations has been documented mainly for informal mathematics. The paper positions EvolAST as a formal, equivalence-preserving alternative to error-prone LLM rewrites.

Data Augmentation in Mathematical Reasoning

  • Prior mathematical data synthesis includes question rewriting, complexity variation, and expert-inspired generation, while EvolDomain and EvolDifficulty target formal statements and domain coverage.MetaMath, WizardMath, and PromptCoT are cited as examples of the informal-mathematics approaches.Source: §2 · p. 3
  • LLM-based problem evolution can introduce syntactic or semantic errors, whereas EvolAST rewrites Lean 4 statements at the AST level to preserve correctness and equivalence.The authors describe the AST approach as increasing data diversity and precision.Source: §2 · p. 3

Robustness of LLMs in Mathematical Reasoning

  • LLM performance drops under small mathematical perturbations, but robustness in formal systems such as Lean4 and Coq remains largely underexplored.PutnamGAP reports average accuracy declines of 3–10%, and MATH-P-Hard reports drops of 10–25% for models such as o1-mini.Source: §2 · pp. 3–4
  • Ineq-Comp measures prover performance drops between original problems and perturbed counterparts.The benchmark is cited as addressing the gap in formal-reasoning robustness evaluation.Source: §2 · pp. 3–4

3 METHOD

The method expands formal theorem data through LLM-driven domain and difficulty evolution, verifies generated examples, and then applies deterministic AST rewrites. EvolProver is trained on the resulting augmented dataset.

3 METHOD

  • The pipeline applies EvolDomain and EvolDifficulty, verifies generated data, diversifies syntax with EvolAST, and uses the augmented dataset to train EvolProver.The phases are ordered: LLM-based evolution, verification, AST-based transformation, then model training.Source: §3 · p. 4

3.1 EVOLDOMAIN AND EVOLDIFFICULTY

  • Existing formal statements from Deepseek-Prover-V1 and STP-Lean serve as seeds, allowing theorem generation directly from formal statements without natural-language intermediaries.The paper notes that these datasets often lack natural-language descriptions.Source: §3.1 · p. 4
  • EvolDomain guides an LLM to transfer a theorem’s logical skeleton into target domains, producing new propositions with formal statements and natural-language descriptions.A single function call can instantiate the skeleton in 3–5 distinct domains.Source: §3.1 · pp. 4–5
  • EvolDifficulty applies five strategies, including changing logical structure, mathematical depth, abstraction, constraints, and parameters, to adjust theorem difficulty.Its framework aims to provide fine-grained control and a smooth difficulty gradient.Source: §3.1 · p. 5
  • Generated statements first undergo Lean 4 syntax validation, with one LLM repair attempt for failures, then an LLM judge checks consistency, correctness, and difficulty appropriateness.Only data passing both the compiler and semantic-judgment filters enters the final dataset.Source: §3.1 · p. 5

3.2 EVOLAST

  • EvolAST parses statements into ASTs and applies equivalence-based rewrite rules before recompiling them, yielding diverse syntax without further verification.The current rule set has seven rules, and additional mathematical or logical equivalences can be added.Source: §3.2 · p. 5

3.3 TRAINING EVOLPROVER

  • EvolProver is fine-tuned from DeepSeek-Prover-V1.5-Base on augmented data using supervised fine-tuning followed by reinforcement learning.The paper also trains an EvolProver-Base baseline on original, unaugmented public data for comparisons and ablations.Source: §3.3 · p. 5

4 EXPERIMENTS

The experiments compare formal provers across model types and benchmarks, using metrics reported by original authors. EvolProver achieves top results among comparable-size models on FormalMATH-Lite and non-reasoning models on MiniF2F-Test and Ineq-Comp.

4.1 BASELINES

  • The comparisons distinguish end-to-end non-reasoning proof generation, chain-of-thought reasoning, and tree-search models guided by heuristic scores; published-author metrics are used for consistency.The paper notes that reasoning models can use more than 6,000 tokens per proof, versus fewer than 700 for non-reasoning models.Source: §4.1 · p. 6

4.2 RESULTS

  • 53.86%: EvolProver sets a new FormalMATH-Lite SOTA among comparable-size models, above the previous best of 51.76% and top reasoning models.It exceeds EvolProver-Base by 9.14 percentage points; the 425-problem FormalMATH-Lite subset was held out exclusively for final evaluation.Source: §4.2 · p. 6, Table 1 · p. 7
  • 69.80% pass@32: EvolProver sets a comparable-size non-reasoning SOTA on MiniF2F-Test, with performance comparable to or sometimes above reasoning models at nearly 10-fold fewer tokens.Figure 3 compares pass rate and average token length across non-CoT and CoT models.Source: §4.2 · p. 6, Figure 3 · p. 7
  • 30.61 percentage points: EvolProver’s robustness ratio exceeds EvolProver-Base’s, while EvolProver sets non-reasoning SOTA across seed, transformed, and ratio metrics.Ineq-Comp evaluates robustness to minor perturbations using seed problems and transformed variants.Source: §4.2 · pp. 6–7

5 ANALYSIS

The analysis compares direct theorem evolution with natural-language-first alternatives and examines domain diversity and component ablations. Direct evolution performs best among the tested methods, while EvolProver improves results across most FormalMATH-Lite domains.

Evolution Strategy

  • The analysis compares direct formal evolution with three natural-language-first routes: a specialized formalizer, and general-purpose LLM formalization in zero-shot or few-shot settings.The experiment uses four branches to evaluate direct evolution against those alternatives.Source: §5 · p. 8
  • Direct EvolDomain and EvolDifficulty evolution significantly outperforms the tested natural-language-based methods after equal candidate generation and verification.Each branch starts with 400 seed problems and generates an equal number of candidates; the direct approach can yield more than 400 verified statements because a seed may produce multiple variants.Source: §5 · p. 8, Figure 4 · p. 8

Domain Diversity

  • EvolProver improves over EvolProver-Base across most FormalMATH-Lite domains and proves 3 Calculus problems where the baseline proves 0.Table 3 reports proved-problem counts across domains under 32 generation trials.Source: §5 · p. 8, Table 3 · p. 9

Ablation Experiments

  • Ablations isolate the proposed components and report consistent benefits across multiple benchmarks and training stages.Table 4 covers FormalMATH-Lite, MiniF2F-Test, and Ineq-Comp; its results are pass@32 rates.Source: §5 · p. 9, Table 4 · p. 9

6 CONCLUSION AND FUTURE WORK

EvolProver combines EvolDomain, EvolDifficulty, and EvolAST in an augmentation pipeline designed to improve generalizability. The paper reports new SOTA results on several benchmarks, including surpassing comparable models on FormalMATH-Lite, and plans to add synthetic Chain-of-Thought data in future work.

Conclusion

  • EvolProver achieves new SOTA results on several benchmarks and surpasses all comparable models on FormalMATH-Lite.The authors plan to enhance its reasoning capabilities by incorporating synthetically generated Chain-of-Thought data into training.Source: §6 · p. 10
  • The pipeline combines EvolDomain, EvolDifficulty, and EvolAST to improve generalizability from semantic and syntactic perspectives.The paper describes the pipeline as highly extensible.Source: §6 · p. 10

Future Work

  • Future work will incorporate synthetically generated Chain-of-Thought data into training to enhance EvolProver’s reasoning capabilities.Source: §6 · p. 10

REPRODUCIBILITY STATEMENT

The authors describe EvolAST as extensible and invite expansion of its applicable axioms and theorems. They plan to release code and models publicly after institutional approval.

Reproducibility

A.1 DETAILS OF TRAINING EVOLPROVER

The training-data pipeline evolves and verifies formal statements, diversifies them with EvolAST, and retains verified proofs. EvolProver is then trained with supervised fine-tuning and reinforcement learning.

Data Curation

  • From approximately 3.3 million verified statements, the curation pipeline samples 70k for evolution and produces a final dataset of 39.2k unique statement-proof pairs.Verification yields 57.4k statement-description pairs before EvolAST expands them to about 96.7k entries; proof generation and Lean 4 verification precede duplicate removal.Source: §A.1 · p. 13

Supervised Fine Tuning

  • Full-parameter SFT trains DeepSeek-Prover-V1.5-Base for one epoch on a mixture of self-evolved and public data, with a global batch size of 32.The initial learning rate is 1.0 × 10^-5 with cosine decay and 5% warmup; sequences are capped at 4096 tokens.Source: §A.1 · p. 13

Reinforcement Learning

  • RL follows SFT and uses a binary reward: 1 for a correct Lean proof and 0 otherwise.The training set retains 2,718 problems with SFT-checkpoint pass@1 strictly above 0 and below 1/2, and PPO training runs for 10 epochs.Source: §A.1 · p. 13

A.2.1 ABLATION MODEL TRAINING

The ablation models vary the augmentation data and training stages to compare the baseline, partial augmentation, and the full pipeline. An EvolAST-only model was omitted because EvolAST operates on outputs from EvolDomain and EvolDifficulty.

A.2.1 ABLATION MODEL TRAINING

  • EvolProver-Base uses the original, unaugmented public dataset for both SFT and RL.Source: §A.2.1 · p. 13
  • EvolProver-Ablation-SFT uses EvolDomain- and EvolDifficulty-augmented data and undergoes SFT only.Source: §A.2.1 · p. 13
  • EvolProver-Ablation-RL uses the same EvolDomain- and EvolDifficulty-augmented data but undergoes both SFT and RL, isolating EvolAST against the final model.Source: §A.2.1 · p. 13
  • EvolProver-SFT is the final model’s checkpoint after SFT on the fully augmented dataset, including EvolAST.Source: §A.2.1 · p. 14
  • No EvolAST-only model was created because EvolAST operates on outputs from EvolDomain and EvolDifficulty.Source: §A.2.1 · p. 14

A.2.2 ABLATION EXPERIMENT RESULTS

This section covers ablation evidence on data augmentation alongside examples and supporting material for EvolDomain, EvolDifficulty, and EvolAST.

A.2.2 ABLATION EXPERIMENT RESULTS

  • Partial augmentation outperforms EvolProver-Base across all benchmarks, often by more than 10%, and EvolAST adds gains in both SFT and RL.The authors note that EvolProver’s performance ratio is slightly lower than EvolProver-Ablation-RL, but attribute this to denominator growth despite absolute gains in both numerator and denominator.Source: Table 5 · p. 14, §A.2.2 · p. 14

A.3.1 PROMPT TEMPLATE

  • EvolDomain abstracts a formal problem’s logical structure, transfers it to an analogous mathematical domain, then packages the result as a natural-language description and formal statement.The prompt lists target domains ranging from algebra and number theory to calculus, geometry, and discrete mathematics.Source: §A.3.1 · p. 15

A.3.2 CASE STUDY

  • The EvolDomain case study illustrates transferring a number-theory statement into geometry and integral problem variants.The examples include a geometry statement about squared distances and an integral statement about continuous functions on [0, 1].Source: §A.3.2 · p. 16

A.4 DETAILS FOR EVOLDIFFICULTY

  • EvolDifficulty uses expert-screened strategies to generate problems with increased or decreased difficulty.The strategies are divided into upward evolution and downward evolution.Source: §A.4 · pp. 16–17

A.4.1 UPWARDEVOLUTION

  • Difficulty can be increased by complicating logical structure, deepening mathematical reasoning, elevating abstraction, adding stricter constraints, or introducing parameters; each evolved variant must be rigorous, meaningful, distinct, and a valid Lean 4 statement.Source: §A.4.1 · pp. 17–18

A.4.2 DOWNWARDEVOLUTION

  • Downward evolution reduces difficulty by simplifying logic, mathematical depth, abstraction, constraints, or parametric complexity.Its strategies include specializing general propositions and reducing the number of variables or simplifying functional relationships.Source: §A.4.2 · pp. 19–20

A.4.3 CASE STUDY

  • The upward-evolution case study presents a divisibility problem involving the greatest common divisor of expressions built from powers of 11 and 12.The example’s natural-language description states that the gcd of the expression for n and its counterpart for n+1 is divisible by 133.Source: §A.4.3 · p. 20
  • A sequence-divisibility example is labeled as an increase-difficulty evolution, with initial values 133 and 3059 and recurrence u_{n+2} = 155u_{n+1} - 1584u_n.The stated goal is to prove every term is divisible by 133.Source: §A.4.3 · p. 20
  • Two decrease-difficulty examples present nonnegative-real square-root and positive-real AM-GM inequalities.The first asks to bound the square of the sum of square roots by twice the sum; the second states that the arithmetic mean is at least the geometric mean.Source: §A.4.3 · p. 21

A.5 DETAILS FOR VERIFICATION

  • Verification prompts ask LLMs to judge whether natural-language and formal statements are consistent and whether their mathematics is correct.The correctness prompt asks judges to assess provability, well-formedness, and logical contradictions or inconsistencies.Source: §A.5 · pp. 21–22
  • The low-difficulty filter flags simple calculations, algebra, one-step linear equations, and easy sum-of-squares inequalities, while excluding several more complex problem types.Its exclusions include square-root inequalities, more complex inequalities, limits, integrals, number theory, and problems involving higher roots, matrices, polynomials, groups, finite sums, or functional equations.Source: §A.5 · pp. 22–23

A.6 CASE STUDY FOR EVOLAST

  • An EvolAST example shows a formal variant with reordered hypotheses, a reversed inequality, and commuted multiplication operands in an equality.The evolved statement retains the target 233 = y^2 + x^2.Source: §A.6 · p. 24

Related papers

Loading 2510.00732v1…