title: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale
    Synthetic Data
summary: 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.
paper_authors._id: 66501a035a78417f01f909db
paper_authors.name: Huajian Xin
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-05-24T10:51:50.072Z
paper_authors._id: 6532a060a78e70d19c669103
paper_authors.avatarUrl: /avatars/3cc9309b0e31da0fb83f1c3ef87dbe9f.svg
paper_authors.fullname: HuajianXin
paper_authors.type: user
paper_authors.user: HuajianXin
paper_authors._id: 66501a035a78417f01f909dc
paper_authors.name: Daya Guo
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-05-24T10:51:56.647Z
paper_authors._id: 653df20eaa1f487614da4db1
paper_authors.avatarUrl: /avatars/12b27ce2c59f53b7e464039deab36a5d.svg
paper_authors.fullname: Daya Guo
paper_authors.type: user
paper_authors.user: guoday
paper_authors._id: 66501a035a78417f01f909dd
paper_authors.name: Zhihong Shao
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-05-24T10:52:09.659Z
paper_authors._id: 65db64f8b62d242ed8711701
paper_authors.avatarUrl: /avatars/753e9f980eb6786c6b53b2f1becbf745.svg
paper_authors.fullname: Zhihong Shao
paper_authors.type: user
paper_authors.user: ZhihongShao
paper_authors._id: 66501a035a78417f01f909de
paper_authors.name: Zhizhou Ren
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-05-24T10:52:16.474Z
paper_authors._id: 62a8008aac97233f161e3ffe
paper_authors.avatarUrl: /avatars/c5e759275c82823301780fb0504ef5d9.svg
paper_authors.fullname: Zhizhou Ren
paper_authors.type: user
paper_authors.user: Stilwell
paper_authors._id: 66501a035a78417f01f909df
paper_authors.name: Qihao Zhu
paper_authors.status: admin_assigned
paper_authors.statusLastChangedAt: 2024-05-24T10:52:27.016Z
paper_authors._id: 63cd76b4374057a338e8e703
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/63cd76b4374057a338e8e703/i4Qk5-0aYx3oRhC8b50aJ.jpeg
paper_authors.fullname: zhuqihao
paper_authors.type: user
paper_authors.user: zqh11
paper_authors._id: 66501a035a78417f01f909e0
paper_authors.name: Bo Liu
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2024-05-27T07:19:50.799Z
paper_authors._id: 635e3a76106f984574c36409
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/1667120725800-635e3a76106f984574c36409.png
paper_authors.fullname: Bo Liu
paper_authors.type: user
paper_authors.user: Benjamin-eecs
paper_authors._id: 66501a035a78417f01f909e1
paper_authors.name: Chong Ruan
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2024-08-17T05:38:40.409Z
paper_authors._id: 6398203609f12714ed1935c2
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/6398203609f12714ed1935c2/uXgl0LgKnFYjq1Wz39-a6.jpeg
paper_authors.fullname: Chong Ruan
paper_authors.type: user
paper_authors.user: Chester111
paper_authors._id: 66501a035a78417f01f909e2
paper_authors.name: Wenda Li
paper_authors._id: 66501a035a78417f01f909e3
paper_authors.name: Xiaodan Liang
paper_title: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale
    Synthetic Data
paper_summary: 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.
paper_ai_summary: Generating extensive Lean 4 proof data from mathematical competition problems improved DeepSeekMath 7B's theorem-proving capabilities over GPT-4 and other methods.
paper_ai_keywords: Lean 4 DeepSeekMath 7B formal theorem proving natural language problems formal statements synthetic data whole-proof generation Lean 4 miniF2F test FIMO benchmark