DeepSeek-Prover-V1.5-Base

Evaluation Results | Model Download | License | Citation | Contact Paper Link 👁️ DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search 1. Introduction 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%). 2. Evaluation Results | | miniF2F-test | ProofNet | |--------|------------------|------------------| | **ReProver** | 26.5% | 13.8% | | **GPT-f** | 36.6% | - | | **Hypertree Proof Search** | 41.0% | - | | **InternLM2-StepProver** | 54.5% | 18.1% | | **DeepSeek-Prover-V1** | 50.0% | - | | **DeepSeek-Prover-V1.5-Base** | 42.2% | 13.2% | | **DeepSeek-Prover-V1.5-SFT** | 57.4% | 22.9% | | **DeepSeek-Prover-V1.5-RL** | 60.2% | 22.6% | | **DeepSeek-Prover-V1.5-RL + RMaxTS** | **63.5%** | **25.3%** | 3. Model Downloads We release the DeepSeek-Prover-V1.5 with 7B parameters, including base, SFT and RL models, to the public. | **Model** | **Download** | | :-----------------------------: | :----------------------------------------------------------: | | DeepSeek-Prover-V1.5-Base | 🤗 HuggingFace | | DeepSeek-Pr