DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for
  Reinforcement Learning and Monte-Carlo Tree Search
Authors: name: Huajian Xin, name: Z. Z. Ren, name: Junxiao Song, name: Zhihong Shao, name: Wanjia Zhao, name: Haocheng Wang, name: Bo Liu, name: Liyue Zhang, name: Xuan Lu, name: Qiushi Du, name: Wenjun Gao, name: Qihao Zhu, name: Dejian Yang, name: Zhibin Gou, name: Z. F. Wu, name: Fuli Luo, name: Chong Ruan
Organization: DeepSeek

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%).