DeepSeek-Prover: Avanzare nella dimostrazione di teoremi nei LLM attraverso dati sintetici su larga scala

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

May 23, 2024

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

cs.AI

Abstract

Gli assistenti di dimostrazione come Lean hanno rivoluzionato la verifica delle dimostrazioni matematiche, garantendo elevata accuratezza e affidabilità. Sebbene i modelli linguistici di grandi dimensioni (LLM) mostrino promettenti capacità nel ragionamento matematico, il loro progresso nella dimostrazione formale di teoremi è ostacolato dalla mancanza di dati di addestramento. Per affrontare questo problema, introduciamo un approccio per generare un ampio set di dati di dimostrazioni Lean 4 derivati da problemi di competizioni matematiche di livello scolastico e universitario. Questo approccio prevede la traduzione di problemi in linguaggio naturale in affermazioni formali, la filtrazione di affermazioni di bassa qualità e la generazione di dimostrazioni per creare dati sintetici. Dopo aver ottimizzato il modello DeepSeekMath 7B su questo dataset sintetico, che comprende 8 milioni di affermazioni formali con dimostrazioni, il nostro modello ha raggiunto accuratezze nella generazione di dimostrazioni complete del 46,3% con 64 campioni e del 52% cumulativamente nel test Lean 4 miniF2F, superando il baseline GPT-4 al 23,0% con 64 campioni e un metodo di apprendimento per rinforzo con ricerca ad albero al 41,0%. Inoltre, il nostro modello ha dimostrato con successo 5 su 148 problemi nel benchmark Lean 4 Formalized International Mathematical Olympiad (FIMO), mentre GPT-4 non è riuscito a dimostrarne alcuno. Questi risultati dimostrano il potenziale di sfruttare dati sintetici su larga scala per migliorare le capacità di dimostrazione di teoremi nei LLM. Sia il dataset sintetico che il modello saranno resi disponibili per facilitare ulteriori ricerche in questo promettente campo.

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.