DeepSeek-Prover: Avançando a Demonstração de Teoremas em LLMs por meio de Dados Sintéticos em Larga Escala

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

May 23, 2024

Autores: Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang

cs.AI

Resumo

Assistentes de prova como o Lean revolucionaram a verificação de provas matemáticas, garantindo alta precisão e confiabilidade. Embora os grandes modelos de linguagem (LLMs) mostrem potencial no raciocínio matemático, seu avanço na prova formal de teoremas é limitado pela escassez de dados de treinamento. Para abordar essa questão, introduzimos uma abordagem para gerar dados extensivos de provas no Lean 4 derivados de problemas de competições matemáticas de nível médio e superior. Essa abordagem envolve a tradução de problemas em linguagem natural para declarações formais, a filtragem de declarações de baixa qualidade e a geração de provas para criar dados sintéticos. Após ajustar o modelo DeepSeekMath 7B nesse conjunto de dados sintéticos, que compreende 8 milhões de declarações formais com provas, nosso modelo alcançou acurácias de geração de provas completas de 46,3% com 64 amostras e 52% cumulativamente no teste Lean 4 miniF2F, superando o GPT-4 de referência em 23,0% com 64 amostras e um método de aprendizado por reforço com busca em árvore em 41,0%. Além disso, nosso modelo provou com sucesso 5 de 148 problemas no benchmark Lean 4 Formalized International Mathematical Olympiad (FIMO), enquanto o GPT-4 não conseguiu provar nenhum. Esses resultados demonstram o potencial de aproveitar dados sintéticos em larga escala para aprimorar as capacidades de prova de teoremas em LLMs. Tanto o conjunto de dados sintéticos quanto o modelo serão disponibilizados para facilitar pesquisas adicionais nesse campo promissor.

English

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.