DeepSeek-Prover: Vooruitgang in Stellingen Bewijzen binnen LLM's door Grootschalige Synthetische Data

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

May 23, 2024

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

cs.AI

Samenvatting

Proof assistants zoals Lean hebben een revolutie teweeggebracht in de verificatie van wiskundige bewijzen, waardoor een hoge nauwkeurigheid en betrouwbaarheid worden gegarandeerd. Hoewel grote taalmodellen (LLMs) veelbelovend zijn in wiskundig redeneren, wordt hun vooruitgang in formeel bewijzen van stellingen belemmerd door een gebrek aan trainingsdata. Om dit probleem aan te pakken, introduceren we een aanpak om uitgebreide Lean 4-bewijsdata te genereren, afgeleid van wiskundige competitieproblemen op middelbare school- en bachelor-niveau. Deze aanpak omvat het vertalen van problemen in natuurlijke taal naar formele uitspraken, het filteren van kwalitatief slechte uitspraken en het genereren van bewijzen om synthetische data te creëren. Na het fine-tunen van het DeepSeekMath 7B-model op deze synthetische dataset, die bestaat uit 8 miljoen formele uitspraken met bewijzen, behaalde ons model een nauwkeurigheid van 46,3% bij het genereren van volledige bewijzen met 64 samples en 52% cumulatief op de Lean 4 miniF2F-test, wat de baseline GPT-4 overtreft met 23,0% bij 64 samples en een tree search reinforcement learning-methode met 41,0%. Daarnaast bewees ons model met succes 5 van de 148 problemen in de Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, terwijl GPT-4 geen enkel probleem kon bewijzen. Deze resultaten tonen het potentieel aan van het gebruik van grootschalige synthetische data om de stellingbewijsvaardigheden van LLMs te verbeteren. Zowel de synthetische dataset als het model zullen beschikbaar worden gesteld om verder onderzoek in dit veelbelovende veld te faciliteren.

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.