Elamur Research⌕
☰
home / papers / 2024 / LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

Paper · 2024 · Zijian Wu, Jiayu Wang, Dahua Lin et al.

Summary

Large language models that write formal proofs are held back by a shortage of training data. Raw Lean code also omits the intermediate proof states a human sees while working in the prover. Beyond Mathlib, most public Lean 4 code had never been processed into usable training material. The authors built LEAN-GitHub by collecting nearly every Lean 4 repository on GitHub and compiling it with a custom, highly parallel pipeline. Instead of relying on Lake, they called the leanc compiler directly over a global import graph that includes loose, standalone files. They also adapted LeanDojo-based extraction so it runs on isolated files and wastes less computation. They then fine-tuned InternLM-math-plus on this data together with Mathlib and synthetic data, producing the 7B InternLM2-StepProver. The model reached state-of-the-art results on miniF2F, ProofNet and Putnam. Ablation experiments show that adding LEAN-GitHub improves accuracy, which indicates that diverse human-written formal corpora are valuable for automated theorem proving.

Key points

  • Data collection: The authors found 237 Lean 4 repositories and dropped 90 written in deprecated Lean versions, leaving 147. Of these, only 61 compiled without changes.
  • Dataset size: The final dataset holds 28,597 theorems and 218,866 tactics from 2,133 files, about 0.13B tokens. It is released on Hugging Face as InternLM/Lean-GitHub.
  • miniF2F results: InternLM2-StepProver scores 48.8% at pass@1 and 54.5% cumulative on miniF2F-test, beating DeepSeek-Prover's 52%. On miniF2F-valid it reaches 59.8% and 63.9%.
  • Other benchmarks: The model gets 18.1% pass@1 on ProofNet, compared with 13.8% for ReProver. It solves 5 of 640 Putnam problems, while DSP solved 4. Its solutions include Putnam 1988 B2 and IMO 1983 P6, neither previously reported as solved in Lean 4.
  • Ablation: Adding LEAN-GitHub to Mathlib-only training raises miniF2F-test pass@1 from 37.3% to 41.0%. Adding it on top of Mathlib plus synthetic data raises the score from 46.7% to 48.8%.

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

 Institutions

🎓Chinese University of Hong KongHong Kong · China176 works · 17,536 citations🔬Shanghai Artificial Intelligence LaboratoryShanghai · China164 works · 13,544 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Zijian Wu, Jiayu Wang, Dahua Lin and Kai Chen. 2024. LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover. arXiv:2407.17227.

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

@misc{wu2024lean,
  title = {{LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover}},
  author = {Zijian Wu, Jiayu Wang, Dahua Lin and Kai Chen},
  year = {2024},
  doi = {10.48550/arxiv.2407.17227},
  eprint = {2407.17227},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2407.17227}
}

References

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

  1. Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
  2. Jeremy Avigad. Mathematics and the formal turn, 2023. find
  3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023.
  4. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023.
  5. Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning approach to first-order logic theorem proving. In Proceedings of the AAAI Conference on Arti… find
  6. Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob 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. Springer, 2015. find
  7. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models, 2023.
  8. Thibault Gauthier, C. Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: Learning to prove with tactics. Journal of Automated Reasoning, 65:257 – 286, 2018.
  9. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021.
  10. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset, 2021.
  11. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving, 2018.
  12. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.
  13. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
  14. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349, 2022.
  15. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning, 2021.
  16. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving, 2024.
  17. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery.
  18. A. Newell and H. Simon. The logic theory machine–a complex information processing system. IRE Transactions on Information Theory, 2(3):61–79, 1956. — The logic theory machine: A complex information processing system
  19. Lawrence C. Paulson. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. find
  20. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  21. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  22. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  23. Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. arXiv preprint arXiv:2310.04353, 2023.
  24. The Coq Development Team. Coq, 2017. find
  25. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition, 2024.
  26. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts, 2024.
  27. Jason Wei, Maarten Bosma, Vincent Y. Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M. Dai, and Quoc V. Le. Finetuned language models are zero-shot learners, 2022.
  28. Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330–9342, 2021.
  29. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
  30. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data, 2024.
  31. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023.
  32. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. ArXiv, abs/1905.09381, 2019.
  33. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019.
  34. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
  35. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024.
  36. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open m… — InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning
  37. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023.
  38. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/