Research map / Reinforcement learning / Visual and representation RL

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

ICLR 2025 · Reinforcement learning › Visual and representation RL · approach: Scalable RL systems and environments · 3 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces DeepSeek-Prover-V1.5, a 7B Lean 4 whole-proof generator trained with pre-training, CoT-augmented SFT, GRPO from Lean verifier feedback, and RMaxTS tree search using truncate-and-resume.

Problem

Whole-proof generation for formal theorem proving in Lean 4 suffers from long-horizon sequence prediction without intermediate tactic states, and proof-step search suffers from sparse rewards.

Approach

A truncate-and-resume mechanism unifies whole-proof generation and tree search by truncating generated proofs at the first Lean error and resuming generation with tactic-state comments; RMaxTS adds intrinsic (RMax-style) rewards and discounted UCB to explore the proof tree under sparse extrinsic rewards.

Key results

• Single-pass whole-proof generation reaches 60.2% pass rate on miniF2F-test with 16x6400 samples, vs 50.0% for DeepSeek-Prover-V1.
• With RMaxTS tree search, DeepSeek-Prover-V1.5-RL reaches 63.5% on miniF2F-test (32x6400), a new state of the art at publication.
• On ProofNet test, RL+RMaxTS reaches 25.3% pass rate with 4x6400 samples, vs 18.1% for InternLM2-StepProver.

Measured effects reported in the paper

Surprising findings

• RL gives genuine improvement in pass@K even at large sample budgets, unlike findings in natural-language math where RL mainly boosts top-K accuracy.
• Without tactic-state information in the prompt, the gain from tree search becomes moderate, especially on hard problems.

Limitations

• Proof search (exploitation/critic) remains unexplored; only exploration is addressed via RMaxTS.
• Evaluation limited to miniF2F and ProofNet; ProofNet validation set was used for expert iteration in SFT.

Experimental setup

Datasets: Mathlib4 DeepSeek-Prover-V1 synthetic theorems Lean Workbook miniF2F ProofNet

Benchmarks: miniF2F-test ProofNet

Metrics: pass@K

Baselines: DeepSeek-Prover-V1 InternLM2-StepProver Lean-STaR Hypertree Proof Search ReProver COPRA Llemma GPT-4 LLMStep GPT-f

Builds on: DeepSeek-Prover-V1 DeepSeekMath GRPO RMax LeanDojo

Closest papers by meaning

• Process-Verified Reinforcement Learning for Theorem Proving via Lean (ICLR 2026 · similarity 0.92)
• Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.89)
• Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.89)
• MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.89)
• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.89)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.88)