Elamur Research
☰
home / papers / 2024 / DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

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

Written for the Research library (claude-opus-5-5) from the paper text. Original — arxiv.org/pdf/2405.14333v1

Summary

LLMs struggle with formal theorem proving because there is very little training data in languages such as Lean 4. Few mathematicians write formal proofs, so the available corpora stay small. The authors built a pipeline that turns informal competition problems from high school and undergraduate level, mostly algebra and number theory, into Lean 4 statements. A quality-scoring model removes trivial statements, and a hypothesis-rejection step removes inconsistent ones. The remaining statements go to the prover, and the Lean 4 verifier checks every candidate proof. Verified theorem–proof pairs are used to fine-tune the prover again, and the cycle repeats until gains level off. To save compute, the negation of each statement is attacked at the same time, so unprovable statements are dropped early. Built on DeepSeekMath 7B, DeepSeek-Prover writes complete proofs and solves 46.3% of miniF2F-test with 64 samples. That is about twice GPT-4's score and higher than a tree-search RL prover. The work shows that large synthetic formal datasets can make up for the shortage of human-written proofs. The dataset and model are released openly.

Key points

  • Synthetic dataset: roughly 8 million Lean 4 statements, each with a verified proof (8,066,621 in the largest training set), generated over several rounds of self-training.
  • miniF2F-test: 46.3% whole-proof accuracy at 64 samples and 52% cumulatively. GPT-4 scores 23.0%, and a tree-search reinforcement-learning method scores 41.0%.
  • FIMO (148 formalized IMO problems): 4 problems solved with 100 samples and 5 with 4096 samples. GPT-4 solved none.
  • Iterations help steadily: pass@128 on miniF2F-test rose from 34.0% at iteration 0 to 46.3% at iteration 4. On miniF2F-valid it rose from 38.1% to 59.4%.
  • Scaling the data: pass@128 goes up roughly in step with each tenfold increase in training data. Going from 1K to about 8M examples raised miniF2F-test from 24.18% to 40.16%.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Fields: Mathematics & statistics

Cited by

105 papers of our library cite it (of the 140673 whose bibliographies we read); 4 of them have a page here, 101 not yet.

Cite

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2405.14333 · arXiv 2405.14333

@misc{xin2024deepseek,
  title = {{DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data}},
  author = {Xin, Huajian and Guo, Daya and Shao, Zhihong and Ren, Zhizhou and Zhu, Qihao and Liu, Bo and Ruan, Chong and Li, Wenda and Liang, Xiaodan},
  year = {2024},
  doi = {10.48550/arxiv.2405.14333},
  eprint = {2405.14333},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2405.14333}
}

References

38 references, 11 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. J. Achiam, S. Adler, S. Agarwal, L. Ahmad, I. Akkaya, F. L. Aleman, D. Almeida, J. Altenschmidt, S. Altman, S. Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023. find our card
  2. J. Avigad. Mathematics and the formal turn, 2023. find
  3. Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. McAleer, A. Q. Jiang, J. Deng, S. Biderman, and S. Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023. find our card
  4. K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pages 454–463. PMLR, 2019. find
  5. W. Bibel. Automated theorem proving. Springer Science & Business Media, 2013. find
  6. M. Crouse, I. Abdelaziz, B. Makni, S. Whitehead, C. Cornelio, P. Kapanipathi, K. Srinivas, V. Thost, M. Witbrock, and A. Fokoue. A deep reinforcement learning approach to first-order logic theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 6279–6287,… find
  7. L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. find
  8. E. First, M. N. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-proof generation and repair with large language models, 2023. find
  9. J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021. find
  10. Y. Huang, X. Lin, Z. Liu, Q. Cao, H. Xin, H. Wang, Z. Li, L. Song, and X. Liang. Mustard: Mastering uniform synthesis of theorem and proof data. arXiv preprint arXiv:2402.08957, 2024. find
  11. A. Q. Jiang, W. Li, J. M. Han, and Y. Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392, 2021. find
  12. A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygóźdź, P. Miłoś, Y. Wu, and M. Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:8360–8373, 2022a. find
  13. A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022b. find our card
  14. A. Q. Jiang, W. Li, and M. Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023. find
  15. C. Kaliszyk, J. Urban, H. Michalewski, and M. Olšák. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018. find
  16. L. Kovács and A. Voronkov. First-order theorem proving and vampire. In International Conference on Computer Aided Verification, pages 1–35. Springer, 2013. find
  17. G. Lample, T. Lacroix, M.-A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349, 2022. find our card
  18. C. Liu, J. Shen, H. Xin, Z. Liu, Y. Yuan, H. Wang, W. Ju, C. Zheng, Y. Yin, L. Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023. find
  19. S. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017. find
  20. L. d. Moura and S. Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. find our card
  21. L. C. Paulson. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. find
  22. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. find our card
  23. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022. find our card
  24. A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, I. Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019. find
  25. S. Schulz. E–a brainiac theorem prover. Ai Communications, 15(2-3):111–126, 2002. find
  26. Z. Shao, P. Wang, Q. Zhu, R. Xu, J. Song, M. Zhang, Y. Li, Y. Wu, and D. Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024. find our card
  27. M. Shulman. Strange new universes: Proof assistants and synthetic foundations, 2024. find
  28. A. Thakur, Y. Wen, and S. Chaudhuri. A language-agent approach to formal theorem-proving. arXiv preprint arXiv:2310.04353, 2023. find
  29. The Coq Development Team. Coq. URL https://coq.inria.fr. A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017. ↗
  30. M. Wang and J. Deng. Learning to prove theorems by learning to generate theorems. Advances in Neural Information Processing Systems, 33:18146–18157, 2020. find
  31. M. Wu, M. Norrish, C. Walder, and A. Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34: 9330–9342, 2021. find
  32. Y. Wu, A. Q. Jiang, J. Ba, and R. Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arXiv:2007.02924, 2020. find
  33. Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022. find our card
  34. H. Xin, H. Wang, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023. find
  35. J. Xiong, J. Shen, Y. Yuan, H. Wang, Y. Yin, Z. Liu, L. Li, Z. Guo, Q. Cao, Y. Huang, et al. Trigo: Benchmarking formal mathematical proof reduction for generative language models. arXiv preprint arXiv:2310.10180, 2023. find
  36. K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024. find our card
  37. X. Zhao, W. Li, and L. Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023. find
  38. K. Zheng, J. M. Han, and S. Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. find our card