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