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

Overview

• Proof assistants like Lean have greatly improved the accuracy and reliability of mathematical proof verification.
• While large language models (LLMs) show promise in mathematical reasoning, they struggle with formal theorem proving due to a lack of training data.
• This paper introduces an approach to generate extensive Lean 4 proof data from high-school and undergraduate-level math competition problems.
• The 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, the model achieved improved whole-proof generation accuracies on the Lean 4 miniF2F and FIMO benchmarks, outperforming other baselines.

Plain English Explanation

Computers have become incredibly adept at verifying the accuracy of mathematical proofs, thanks to specialized "proof assistant" software like Lean. However, large language models (LLMs) - the powerful AI systems that can understand and generate human-like text - have struggled to match this level of formal mathematical reasoning. The key issue is that LLMs lack sufficient training data in the specialized language and techniques of mathematical proofs.

To address this, the researchers developed a clever way to generate a large synthetic dataset of Lean 4 proofs. They started with high-school and college-level math competition problems, translated them into formal mathematical statements, filtered out low-quality ones, and then automatically generated proofs for the remaining statements. This resulted in a dataset of over 8 million formal statements with proofs.

The researchers then fine-tuned their DeepSeekMath 7B language model on this synthetic dataset. The results were impressive - the fine-tuned model outperformed other state-of-the-art approaches on standard benchmarks for generating complete mathematical proofs. It even managed to solve a handful of the challenging Lean 4 Formalized International Mathematical Olympiad (FIMO) problems, which previous models had failed.

This work demonstrates the power of leveraging large-scale synthetic training data to enhance the theorem-proving capabilities of LLMs. By creating a custom dataset tailored to the unique challenges of formal mathematics, the researchers were able to significantly boost the performance of their AI system. Both the dataset and the improved model will be made publicly available, paving the way for further advancements in this exciting field.

Technical Explanation

The paper introduces a novel approach to generate extensive Lean 4 proof data from high-school and undergraduate-level mathematical competition problems. This is motivated by the fact that while large language models (LLMs) have shown promise in mathematical reasoning, their advancement in formal theorem proving has been hindered by a lack of training data.

The key steps of the approach are:

1. Translating natural language problems: The researchers start by translating natural language math competition problems into formal Lean 4 statements.
2. Filtering low-quality statements: They then filter out low-quality or ill-formed statements using a combination of manual and automated methods.
3. Generating proofs: Finally, they generate proofs for the remaining high-quality statements using a combination of automated theorem proving and manual intervention.

This process results in a synthetic dataset of over 8 million formal statements with proofs, which the researchers use to fine-tune their DeepSeekMath 7B model.

When evaluated on the Lean 4 miniF2F and FIMO benchmarks, the fine-tuned DeepSeekMath model achieves impressive results:

• On the miniF2F test, it achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively, outperforming the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%.
• On the FIMO benchmark, the model successfully proved 5 out of 148 problems, while GPT-4 failed to prove any.

These results demonstrate the potential of leveraging large-scale synthetic data to enhance the theorem-proving capabilities of LLMs. The researchers make both the synthetic dataset and the improved DeepSeekMath model publicly available to facilitate further research in this promising field.

Critical Analysis

The researchers have made a significant contribution by addressing a key challenge in the field of mathematical reasoning with large language models - the lack of high-quality training data for formal proof verification and generation.

However, the paper does not provide a detailed analysis of the types of mathematical problems or proof techniques covered in the synthetic dataset. It would be useful to know the distribution of topics, difficulty levels, and proof strategies represented, as this could inform the strengths and limitations of the approach.

Additionally, while the model's performance on the Lean 4 benchmarks is impressive, it is still far from human-level mastery of formal theorem proving. The researchers acknowledge that the model only solved a small fraction of the FIMO problems, and further work is needed to expand its capabilities.

One potential concern is the reliance on automated proof generation, which may introduce biases or errors into the synthetic dataset. The researchers do mention manual intervention, but it is unclear how extensive this process was and how it affected the quality of the proofs.

Overall, this work represents an important step forward in the quest to develop LLMs that can excel at formal mathematical reasoning. The availability of the synthetic dataset and the improved DeepSeekMath model will undoubtedly spur further research and innovation in this exciting field.

Conclusion

This paper presents a novel approach to generate large-scale synthetic data for training large language models in the domain of formal mathematical proof verification and generation. By translating natural language math competition problems into formal Lean 4 statements and automatically generating proofs, the researchers were able to create a dataset of over 8 million formal statements with proofs.

When the researchers fine-tuned their DeepSeekMath 7B model on this synthetic dataset, it demonstrated significant improvements in whole-proof generation accuracy on standard benchmarks, outperforming other state-of-the-art approaches. The model even managed to solve a handful of challenging Lean 4 Formalized International Mathematical Olympiad (FIMO) problems, showcasing its potential in formal theorem proving.

This work highlights the power of leveraging large-scale synthetic data to enhance the capabilities of large language models in specialized domains like mathematics. By creating a custom dataset tailored to the unique challenges of formal proof verification and generation, the researchers were able to push the boundaries of what is possible with these powerful AI systems. Both the dataset and the improved DeepSeekMath model will be made publicly available, paving the way for further advancements in this exciting field of research.