mlsanityData to 7 Oct 2026

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

arXiv 2505.12031 ↗First posted 17 May 2025cs.AIcited by 1

On the map: Synthetic data and self-improvement for LLMs → Self-play RL for reasoning

Abstract (arXiv)

Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of 60.74% on MiniF2F and 21.18% on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.

Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs. Builds on 36 of its 45 references that are in the map. First posted on arXiv 17 May 2025.

Builds on

36 of 45 references.

Closest ancestors · 2

Same direction, newest first

  1. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data23 May

Other references · 34

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  3. 2025s1: Simple test-time scalingcited by 1,311
  4. 2024Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvementcited by 1,057
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  6. 2023Llemma: An Open Language Model For Mathematicscited by 385
  7. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  8. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  9. 2024Large Language Models for Mathematical Reasoning: Progresses and Challengescited by 283
  10. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  11. 2022Autoformalization with Large Language Modelscited by 252
  12. 2017Lexically Constrained Decoding for Sequence Generation Using Grid Beam Searchcited by 234
22 more
  1. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  2. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  3. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  4. 2024Large Language Model-Based Agents for Software Engineering: A Surveycited by 173
  5. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  6. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  7. 2019The Lean mathematical librarycited by 127
  8. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  9. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  10. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  11. 2025Towards System 2 Reasoning in LLMs: Learning How to Think With Meta Chain-of-Thoughtcited by 108
  12. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  13. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  14. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  15. 2023Natural Language Reasoning, A Surveycited by 61
  16. 2024Process-Driven Autoformalization in Lean 4cited by 45
  17. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  18. 2024Puzzle Solving using Reasoning of Large Language Models: A Surveycited by 44
  19. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  20. 2024Proving Theorems Recursivelycited by 25
  21. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  22. 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11

Built on by

Cited by year

Citing papers per year: 2025: 1.

1 paper.

  1. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3

Similar, not cited

Close in wording, no citation either way

  1. 2026Direct Optimization of Generators for Search in Automated Theorem Proving
  2. 2026On Reasoning-Centric LLM-based Automated Theorem Proving
  3. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
  4. 2025Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
  5. 2026AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
  6. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
  7. 2025Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
  8. 2026A Learning Method for Symbolic Systems Using Large Language Models ↗