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
Published: 2024-08-15 13:40:03

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