DeepSeek-Prover-V1.5: Aproveitando o Feedback do Assistente de Prova para Aprendizado por Reforço e Busca em Árvore de Monte Carlo

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

August 15, 2024

Autores: 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

Resumo

Apresentamos o DeepSeek-Prover-V1.5, um modelo de linguagem de código aberto projetado para demonstração de teoremas no Lean 4, que aprimora o DeepSeek-Prover-V1 otimizando tanto os processos de treinamento quanto de inferência. Pré-treinado no DeepSeekMath-Base com especialização em linguagens matemáticas formais, o modelo passa por ajustes supervisionados usando um conjunto de dados aprimorado de demonstração de teoremas formais derivado do DeepSeek-Prover-V1. Um refinamento adicional é alcançado por meio de aprendizado por reforço a partir do feedback do assistente de demonstração de teoremas (RLPAF). Além da abordagem de geração de prova única do DeepSeek-Prover-V1, propomos o RMaxTS, uma variante da busca de árvore Monte Carlo que emprega uma estratégia de exploração orientada por recompensa intrínseca para gerar caminhos de prova diversos. O DeepSeek-Prover-V1.5 demonstra melhorias significativas em relação ao DeepSeek-Prover-V1, alcançando novos resultados de ponta no conjunto de testes do benchmark miniF2F de nível escolar (63,5%) e no benchmark ProofNet de nível universitário (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%).