mlsanityData to 7 Oct 2026

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

arXiv 2408.08152 ↗First posted 15 Aug 2024cs.CL cs.AI cs.LGcited by 189

Not on the map. Why?

Cited by 93 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark (63.5%) and the undergraduate level ProofNet benchmark (25.3%).

Key facts. Cited by 189 papers in the map (data through 7 Oct 2026). Builds on 36 of its 60 references that are in the map. First posted on arXiv 15 Aug 2024.

Builds on

36 of 60 references.

References · 36

  1. 2017Attention Is All You Needcited by 59,932
  2. 2023GPT-4 Technical Reportcited by 18,132
  3. 2017Proximal Policy Optimization Algorithmscited by 14,441
  4. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  5. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  6. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  7. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  8. 2019Mastering Atari, Go, Chess and Shogi by Planning with a Learned Modelcited by 1,327
  9. 2017Curiosity-driven Exploration by Self-supervised Predictioncited by 1,173
  10. 2018Exploration by Random Network Distillationcited by 966
  11. 2016Unifying Count-Based Exploration and Intrinsic Motivationcited by 632
  12. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
24 more
  1. 2023Llemma: An Open Language Model For Mathematicscited by 385
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  3. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  4. 2024DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligencecited by 325
  5. 2023Towards Revealing the Mystery behind Chain of Thought: A Theoretical Perspectivecited by 293
  6. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  9. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  10. 2020Reward-Free Exploration for Reinforcement Learningcited by 177
  11. 2018RUDDER: Return Decomposition for Delayed Rewardscited by 162
  12. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  13. 2019The Lean mathematical librarycited by 127
  14. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  15. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  16. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  17. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  18. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  19. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  20. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  21. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  22. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  23. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  24. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 16; 2025: 108; 2026: 65.

189 papers.

Sort:

By area:

  1. 2025Vision-R1: Incentivizing Reasoning Capability in Multimodal Large Language Modelscited by 653
  2. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  4. 2025GPG: A Simple and Strong Reinforcement Learning Baseline for Model Reasoningcited by 147
  5. 2025SoTA with Less: MCTS-Guided Sample Selection for Data-Efficient Visual Reasoning Self-Improvementcited by 144
  6. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  7. 2025Can We Generate Images with CoT? Let's Verify and Reinforce Image Generation Step by Stepcited by 130
  8. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  9. 2025A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systemscited by 108
  10. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  11. 2025SPIRAL: Self-Play on Zero-Sum Games Incentivizes Reasoning via Multi-Agent Multi-Turn Reinforcement Learningcited by 89
  12. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
38 more
  1. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  2. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  3. 2025Tree Search for LLM Agent Reinforcement Learningcited by 73
  4. 2024Interpretable Contrastive Monte Carlo Tree Search Reasoningcited by 62
  5. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  6. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  7. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  8. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  9. 2025Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modelingcited by 44
  10. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  11. 2024InfiMM-WebMath-40B: Advancing Multimodal Pre-Training for Enhanced Mathematical Reasoningcited by 36
  12. 2025Jigsaw-R1: A Study of Rule-based Visual Reinforcement Learning with Jigsaw Puzzlescited by 36
  13. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  14. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  15. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  16. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoningcited by 34
  17. 2025Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoningcited by 33
  18. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 32
  19. 2025We-Math 2.0: A Versatile MathBook System for Incentivizing Visual Mathematical Reasoningcited by 32
  20. 2026Group-Evolving Agents: Open-Ended Self-Improvement via Experience Sharingcited by 32
  21. 2025Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspectivecited by 29
  22. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 28
  23. 2025R2R: Efficiently Navigating Divergent Reasoning Paths with Small-Large Model Token Routingcited by 28
  24. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  25. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  26. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  27. 2026Scalable Power Sampling: Unlocking Efficient, Training-Free Reasoning for LLMs via Distribution Sharpeningcited by 27
  28. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  29. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  30. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  31. 2025Reward Models in Deep Reinforcement Learning: A Surveycited by 24
  32. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  33. 2025Attention Illuminates LLM Reasoning: The Preplan-and-Anchor Rhythm Enables Fine-Grained Policy Optimizationcited by 23
  34. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  35. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  36. 2025Introducing LongCat-Flash-Thinking: A Technical Reportcited by 21
  37. 2026Large Language Model Reasoning Failurescited by 20
  38. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19

50 most cited of 189 All 189 (JSON)