DeepSeek-Prover-V1.5: Nutzen von Beweisassistenten-Feedback für Verstärkendes Lernen und Monte-Carlo-Baumsuche

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

August 15, 2024

Autoren: Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan

cs.AI

Zusammenfassung

Wir stellen DeepSeek-Prover-V1.5 vor, ein Open-Source-Sprachmodell, das für den Beweis von Theoremen in Lean 4 entwickelt wurde und DeepSeek-Prover-V1 durch die Optimierung sowohl des Trainings- als auch des Inferenzprozesses verbessert. Das Modell wird vorab auf DeepSeekMath-Base vortrainiert und auf formale mathematische Sprachen spezialisiert. Anschließend erfolgt ein überwachtes Feintuning unter Verwendung eines erweiterten formalen Datensatzes für den Theorembeweis, der aus DeepSeek-Prover-V1 abgeleitet ist. Eine weitere Verfeinerung wird durch Reinforcement-Learning aus dem Feedback des Beweishelfers (RLPAF) erreicht. Über den Einzeldurchlauf-Ansatz zur Generierung des gesamten Beweises von DeepSeek-Prover-V1 hinaus schlagen wir RMaxTS vor, eine Variante der Monte-Carlo-Baumsuche, die eine erkundungsgesteuerte Strategie mit intrinsischer Belohnung zur Generierung verschiedener Beweiswege verwendet. DeepSeek-Prover-V1.5 zeigt signifikante Verbesserungen gegenüber DeepSeek-Prover-V1 und erzielt neue Spitzenwerte auf dem Testset des Benchmark für die Mittelstufe miniF2F (63,5%) und dem Benchmark für die Grundstufe ProofNet (25,3%).

English

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