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

arXiv: https://arxiv.org/abs/2510.00732 · HTML: https://mlsanity.com/paper/2510.00732/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 29 references that are in the map.
- First posted on arXiv 1 Oct 2025.

## Builds on (most cited first, 21 of 21)

- [WizardLM: Empowering large pre-trained language models to follow complex instructions](https://mlsanity.com/paper/2304.12244/) (2023)
- [MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models](https://mlsanity.com/paper/2309.12284/) (2023)
- [WizardCoder: Empowering Code Large Language Models with Evol-Instruct](https://mlsanity.com/paper/2306.08568/) (2023)
- [WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct](https://mlsanity.com/paper/2308.09583/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Curriculum Reinforcement Learning from Easy to Hard Tasks Improves LLM Reasoning](https://mlsanity.com/paper/2506.06632/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [Leanabell-Prover: Posttraining Scaling in Formal Reasoning](https://mlsanity.com/paper/2504.06122/) (2025)
- [Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning](https://mlsanity.com/paper/2507.08649/) (2025)
- [PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2503.02324/) (2025)
- [Domain Generalization via Balancing Training Difficulty and Model Capability](https://mlsanity.com/paper/2309.00844/) (2023)
- [StepFun-Prover Preview: Let's Think and Verify Step by Step](https://mlsanity.com/paper/2507.20199/) (2025)
- [Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities](https://mlsanity.com/paper/2505.12680/) (2025)
- [An Investigation of Robustness of LLMs in Mathematical Reasoning: Benchmarking with Mathematically-Equivalent Transformation of Advanced Mathematical Problems](https://mlsanity.com/paper/2508.08833/) (2025)

## Built on by (most cited first, 7 of 7)

- [From Storage to Experience: A Survey on the Evolution of LLM Agent Memory Mechanisms](https://mlsanity.com/paper/2605.06716/) (2026)
- [AgentMath: Empowering Mathematical Reasoning for Large Language Models via Tool-Augmented Agent](https://mlsanity.com/paper/2512.20745/) (2025)
- [DiffCoT: Diffusion-styled Chain-of-Thought Reasoning in LLMs](https://mlsanity.com/paper/2601.03559/) (2026)
- [Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification](https://mlsanity.com/paper/2601.22642/) (2026)
- [FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization](https://mlsanity.com/paper/2603.19828/) (2026)
- [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026)
- [Testing LLM Arithmetic Reasoning Generalization with Automatic Numeric-Remapping Attacks](https://mlsanity.com/paper/2606.03606/) (2026)

## Abstract (arXiv)

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.