DeepSeek Unveils DeepSeek-Prover-V2: Advancing Neural Theorem Proving with Recursive Proof Search and a New Benchmark

DeepSeek AI has announced the release of DeepSeek-Prover-V2, a groundbreaking open-source large language model specifically designed for formal theorem proving within the Lean 4 environment. This latest iteration builds upon previous work by introducing an innovative recursive theorem-proving pipeline, leveraging the power of DeepSeek-V3 to generate its own high-quality initialization data. The resulting model achieves state-of-the-art performance in neural theorem proving and is accompanied by the introduction of ProverBench, a new benchmark for evaluating mathematical reasoning capabilities.

Pioneering Cold-Start Reasoning Data Generation

A key innovation of DeepSeek-Prover-V2 lies in its unique cold-start training procedure. This process begins by prompting the powerful DeepSeek-V3 model to decompose complex mathematical theorems into a series of more manageable subgoals. Simultaneously, DeepSeek-V3 formalizes these high-level proof steps in Lean 4, effectively creating a structured sequence of sub-problems.

To handle the computationally intensive proof search for each subgoal, the researchers employed a smaller 7B parameter model. Once all the decomposed steps of…