DeepSeek-Prover-V1.5: Использование обратной связи доказательного помощника для обучения с подкреплением и поиска дерева Монте-Карло.

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

August 15, 2024

Авторы: 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

Аннотация

Мы представляем DeepSeek-Prover-V1.5, открытую языковую модель, разработанную для доказательства теорем в Lean 4, которая улучшает DeepSeek-Prover-V1 путем оптимизации процессов как обучения, так и вывода. Обученная на DeepSeekMath-Base с специализацией на формальных математических языках, модель проходит надзорное дообучение с использованием улучшенного формального набора данных для доказательства теорем, полученного из DeepSeek-Prover-V1. Дальнейшее совершенствование достигается с помощью обучения с подкреплением на основе обратной связи от помощника по доказательствам (RLPAF). Помимо подхода к генерации целого доказательства за один проход, присущего DeepSeek-Prover-V1, мы предлагаем RMaxTS, вариант поиска по дереву Монте-Карло, который использует стратегию исследования, основанную на внутренней награде, для генерации разнообразных путей доказательства. DeepSeek-Prover-V1.5 демонстрирует значительные улучшения по сравнению с DeepSeek-Prover-V1, достигая новых результатов на тестовом наборе данных школьного уровня miniF2F (63.5%) и на уровне бакалавриата 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%).