Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

Authors: huajian  xin
daya  guo
zhihong  shao
z z ren
bo  liu
chong  ruan
wenda  li
xiaodan  liang
  deepseek
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-24 11:55:07

Abstract: Proof assistants like Lean have revolutionized mathematical proof verification by providing high levels of accuracy and reliability. Although large language models (LLMs) have demonstrated potential in mathematical reasoning, their advancement in formal theorem proving is hindered by the scarcity of large, high-quality training datasets. To address this challenge, we present a novel approach to generate extensive Lean 4 proof data from natural language mathematical problems at the high school and undergraduate levels. Specifically, we synthesize 8 million formal statements with corresponding proofs, leveraging this dataset to fine-tune the DeepSeekMath 7B model. The resulting model, DeepSeek-Prover, achieves a pass rate of 50\% on the Lean 4 miniF2F benchmark, surpassing the previous state-of-the-art result of 41.0\%. These findings underscore the potential of large-scale synthetic data in significantly enhancing the theorem-proving capabilities of LLMs.

Main paper: 
 introduction: 
 Formal mathematical languages, such as Lean [Moura and Ullrich, 2021] , Isabelle [Paulson, 1994] , and Coq [The Coq Development Team], have enabled the development of computer-verifiable proofs [Avigad, 2023] . However, constructing formal proofs remains a labor-intensive process that requires both substantial effort and specialized expertise-often challenging even for experienced mathematicians. To ease the burden of writing formal proofs, recent approaches [Polu and Yang et al., 2023] have explored the use of language models to automatically generate proofs for given formal statements. Despite this progress, the performance of these methods has been constrained by the limited availability of high-quality formal proof data.To address this limitation, we propose an iterative methodology for generating large-scale Lean 4 proof data from natural language mathematical problems. Our approach utilizes large language models to translate competition-level problems from high school and undergraduate mathematics into formal statements, followed by the generation of verifiable proofs using the Lean 4 prover. The model is fine-tuned with this synthetic data, and the data generation process is repeated to further refine the model. This iterative pipeline, executed with the continuously enhanced DeepSeekMath 7B model [Shao et al., 2024] , continues until no further improvement in model performance is observed. Ultimately, our final dataset comprises 8 million formal statements paired with corresponding proofs. Figure 1 : Overview of our approach. Our pipeline starts by autoformalizing a broad range of mathematical problems into formal statements. Inconsistent or overly simplistic statements are discarded. The remaining high-quality statements are then iteratively processed, attempting either to prove or refute them (i.e., prove their negation), until one is verified by the Lean 4 prover. The verified pairs of natural language problems and their formalization, formal statements (or their negations) and their corresponding proofs are used to fine-tune the model, enhancing its theorem-proving ability. This process repeats until no further performance gains are observed.We evaluate the theorem proving performance in Lean 4 of the resulting model, DeepSeek-Prover, using the miniF2F benchmark [Zheng et al., 2022] . DeepSeek-Prover achieves a pass rate of 50% on the test set of the miniF2F, surpassing the previous state-of-the-art result of 41.0%. Ablation studies reveal that our iterative training process progressively enhances the model's problem-solving ability with each iteration, further demonstrating the effectiveness of our approach. 
approach: 
 Our approach consists of an iterative cycle of dataset synthesis and model training, as shown in Figure 1 . Each phase is described in detail below.Informal Data Curation. We collect mathematical problems in natural language by scraping online resources containing high school and undergraduate exercises, exams, and competitions. After cleaning the data, we curated a dataset of 869,659 high-quality math problems, focusing on algebra and number theory.Model Initialization. The model, initialized from DeepSeekMath-Base 7B [Shao et al., 2024] , is fine-tuned on MMA dataset [Jiang et al., 2023] , which includes formal statements from Mathlib, the standard mathematical library for Lean 4. This enhances the model's basic autoformalization capabilities. Additionally, we include theorem-proving data from LeanDojo [Yang et al., 2023] , adapted from a next-tactic prediction task to full-proof generation. We refer to the resulting model and its further improved versions as DeepSeek-Prover.Model Scoring and Hypothesis Rejection. Initially, many autoformalized statements were low quality. To improve this, we introduced a scoring mechanism that prompts DeepSeek-Prover to assess each statement using a chain-of-thought approach. Statements are categorized as "excellent," "good," "above average," "fair," or "poor." Statements rated "fair" or "poor" are discarded. Additionally, some provable statements contained inconsistent hypotheses leading to vacuous conclusions. To filter these, DeepSeek-Prover attempts to prove the statement with False as the conclusion. Successful proofs of these transformed statements reveal inconsistent hypotheses, and these statements are discarded. This process refines the dataset, leaving 712,073 high-quality formal statements for proof generation.Statement Proving. With a large corpus of high-quality formal statements, DeepSeek-Prover attempts to generate proofs. Since some synthesized statements may be semantically incorrect and therefore unprovable, brute-force search would be inefficient. To optimize this, we exploit the logical symmetry between a statement and its negation. Dual concurrent proof searches are initiated for each statement-one for Γ ⊢ P and another for Γ ⊢ ¬P . DeepSeek-Prover samples up to k times for each statement until a valid proof for either is found. All validated proofs, whether for the statement or its negation, are used to further train DeepSeek-Prover. This method enriches the dataset with both propositions and their negations, even if the original propositions were incorrectly formalized.Iterative Enhancement. Since the pipeline relies on DeepSeek-Prover, improving its performance after each iteration is crucial. Verified pairs of formal statements (or their negations) and their corresponding proofs are used to enhance the model's theorem-proving capabilities. Pairs of natural language problems and their formalized counterparts, when correctly proved, are also collected to improve the model's autoformalization abilities. With each cycle of refinement, DeepSeek-Prover's performance in both autoformalization and theorem proving incrementally improves, contributing to better dataset synthesis. This iterative process continues until no further performance gains are observed.3 Experiments 
main results: 
 Benchmark and metric. We assess the theorem-proving capabilities of DeepSeek-Prover using the miniF2F benchmark [Zheng et .7% COPRA (GPT-3.5) [13] 60 9.0% COPRA (GPT-4) [13] 60 26.6% Llemma-7B [2] 3200 26.2% Llemma-34B [2] 3200 25.8% ReProver [16] -26.5% LLMStep [15] 3200 27.9% GPT-f [11] 64 × 4096 36.6% Hypertree Proof Search [7] 64 × 5000 41.0% We performed ablation studies to evaluate the contributions of different components of DeepSeek-Prover, using pass@128 as the evaluation metric on the miniF2F-test dataset. The results are summarized in Table 2 . Effectiveness of Large-Scale Autoformalization. We conducted a comparative analysis between our autoformalized synthetic dataset and the human-written Mathlib dataset (the standard mathematical library of Lean 4), as shown in Table 2a . The models trained on our synthetic data substantially outperformed those trained solely on Mathlib data. This process employed an expert iteration strategy [Polu and Sutskever, 2020] , where formal proofs were iteratively generated and used to fine-tune the model until performance improvements plateaued.Effectiveness of Formal Statement Scoring. We evaluated the impact of formal statement quality on model performance by training on both high-and low-scoring proofs. As shown in Table 2b , models trained on high-score proofs outperformed those trained on low-score proofs by 4.5%. This result highlights the importance of accurate statement scoring for filtering lower-quality statements and improving overall performance.Effectiveness of Iterative Enhancement. The results in Table 2c show a clear correlation between the number of iterations in data synthesis and improved theorem-proving performance. Each iteration refines the model's ability to handle increasingly complex proofs, resulting in significant performance gains. This iterative enhancement approach contributes to the generation of higher-quality synthetic data and bolsters the model's theorem-proving capabilities.Effectiveness of Scaling Synthetic Theorem-Proving Data. As illustrated in Table 2d , there is a clear relationship between the size of the synthetic dataset and the model's performance on the miniF2F benchmark. Performance increases consistently with the size of the dataset, highlighting the critical role of large-scale data in advancing automated theorem proving. This underscores the necessity of systematic, large-scale data generation for further progress in the field. 
conclusion: 
 In this paper, we introduced a method for generating extensive synthetic proof data from high-school and undergraduate-level mathematical competition problems. This approach significantly improved the performance of the DeepSeekMath 7B model in automated theorem proving (ATP) when trained on this synthetic dataset. Our model surpasses all previous state-of-the-art methods on the miniF2Ftest benchmark for theorem proving in Lean 4. While our current work primarily focuses on algebra and number theory problems at the middle school and undergraduate levels, future work will aim to broaden the scope of mathematical domains, enhancing the general applicability of our approach to a wider range of theorem proving tasks. 
 
 Appendix: The research presented in this paper has the potential to significantly advance automated theorem proving through the use of large-scale synthetic proof data generated from informal mathematical problems. This progress can facilitate the development of tools for formalizing mathematical reasoning, supporting the broader mathematical and educational communities. 



Reviews: review: title: title: Great work on the creation and usage of synthetic data for formal theorem proving
main_review: main_review: ### Summary:

This work shows a method for effectively utilizing synthetic data for formal theorem proving by providing a pipeline to autoformalize informal proofs, maintain a high quality of synthetic data, and iteratively fine-tune models to achieve state-of-the-art results.

### Strengths:

This work achieves state-of-the-art results on miniF2F by a significant margin.

The ablation studies are comprehensive and show the effectiveness of each part of the methodology.

Data scarcity is a significant problem for formal theorem proving, and this work shows an effective method for using synthetic data in this domain.

### Limitations:

The resources (compute/time) needed to replicate the work are not shown.
title: title: Use data synthesis and model training cycles to improve theorem proving
main_review: main_review: This paper is technically solid and very complete for a workshop submission. The general structure of writing makes sense (There are still some typos in this paper though. I would suggest the authors to polish their writing a bit. E.g. line 37, "cycle" v.s. "circle", "model" v.s. "mode".). The method is detailed clearly. Using a cycle of data synthesis plus model training sounds promising, and is along the same line as most state-of-the-art works in the field such as AlphaProof. Sources of model initialization and data curation sound reasonable too. Overall, the method design and evaluation are in good quality. I would recommend acceptance of this work, and would be curious to see it scaled up.
title: title: A Good Iterative Pipeline for Autoformalization and Formal Theorem Proving
main_review: main_review: This paper introduces DS-prover, an iterative pipeline that employs LLMs to autoformalize natural language problems, filters high-quality autoformalizations, and fine-tunes LLMs for formal theorem proving in Lean. The proved statements generated by the LLMs are then added to the dataset to train the LLMs for autoformalization further. Experiments on miniF2F demonstrate that large-scale formal data derived from natural problems can significantly enhance the theorem-proving capabilities of LLMs.

The paper is well-written and easy to follow. Leveraging large-scale informal data to improve formal theorem proving is both intuitive and practical. While the high-level idea of an iterative pipeline is not novel and has been adopted in various existing works, this paper contributes by providing extensive experiments that convincingly demonstrate the effectiveness of their method.