Elamur Research⌕
☰
home / papers / 2024 / miniCTX: Neural Theorem Proving with (Long-)Contexts

miniCTX: Neural Theorem Proving with (Long-)Contexts

Paper · 2024 · Jiewen Hu, Thomas Zhu and Sean Welleck

Summary

Most neural theorem provers see only the current proof state. They are tested on self-contained competition problems or on library theorems they may already have seen during training. Real formalization work is different: proofs rely on definitions, lemmas, notation and comments introduced earlier in the same project. The authors present miniCTX, a Lean 4 benchmark that measures whether a model can prove theorems whose required background was absent from its training data. Each item pairs a theorem with the file content preceding it, which can reach tens of thousands of tokens, plus metadata for rebuilding cross-file context. To limit contamination, the benchmark uses a temporal split and will be refreshed with newer projects through NTP-TOOLKIT, which extracts and annotates data from Lean repositories. Baselines include prompting, premise selection and "file-tuning", which trains on whole files rather than isolated states. Models that condition on preceding context clearly beat state-only provers, and miniF2F does not reveal this gap. The resource gives a more realistic picture of how provers would perform as assistants in live projects.

Key points

  • miniCTX contains 762 theorems, split evenly into 381 validation and 381 test items. They come from six sources: PrimeNumberTheoremAnd (PNT), PFR (plus a cross-file-heavy PFR extension), Mathlib theorems added after March 2024, the HTPI textbook, HepLean and SciLean.
  • The average context is about 18.7K tokens across all splits, against roughly 150 for miniF2F. HTPI contexts exceed 65K tokens.
  • The authors distinguish three levels of generalization (theorem, context and project) and evaluate both in-file context and cross-file context with retrieved premises.
  • NTP-TOOLKIT (GitHub: cmu-l3/ntp-toolkit, MIT license) and a Lean REPL-based evaluation harness are released. All miniCTX theorems target Lean 4.7.0, and the data is under Apache 2.0.
  • The contamination analysis finds public GitHub solutions for at least 84 of the 244 miniF2F-test problems, including 12 of the 19 IMO problems.

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

🎓Carnegie Mellon UniversityPittsburgh · United States633 works · 195,217 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Jiewen Hu, Thomas Zhu and Sean Welleck. 2024. miniCTX: Neural Theorem Proving with (Long-)Contexts. arXiv:2408.03350.

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

@misc{hu2024minictx,
  title = {{miniCTX: Neural Theorem Proving with (Long-)Contexts}},
  author = {Jiewen Hu, Thomas Zhu and Sean Welleck},
  year = {2024},
  doi = {10.48550/arxiv.2408.03350},
  eprint = {2408.03350},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2408.03350}
}

References

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

  1. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022.
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  3. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations, 2024. URL https://openrevi…
  4. Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts, 2024. URL https://arxiv.org/abs/2401.02949. ↗
  5. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models, 2023.
  6. Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. Deepseek-coder: When the large language model meets programming – the rise of code intelligence, 2024. find
  7. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. ↗
  8. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016. — DeepMath - Deep Sequence Models for Premise Selection
  9. Albert Qiaochu Jiang, Wenda Li, Jesse Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. https://aitp-conference.org/2021/abstract/paper_17.pdf, 2021. ↗
  10. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35: 8360–8373, 2022.
  11. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. URL…
  12. Alex Kontorovich. Prime number theorem and. https://github.com/AlexKontorovich/PrimeNumberTheoremAnd, 2024a. ↗
  13. Alex Kontorovich. Prime number theorem and; rectangle.lean. https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Rectangle.lean, 2024b. ↗
  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. Lean Prover Community. repl. https://github.com/leanprover-community/repl, 2024. ↗
  16. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, 2024.
  17. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023.
  18. Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 146… find
  19. Heather Macbeth. The mechanics of proof. https://github.com/hrmacbeth/math2001, 2023. ↗
  20. Mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. doi: 10.1145/3372885.3373824. URL http://dx.doi.org/10.1145/3372885.3373824. ↗
  21. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023.
  22. Kim Morrison. lean-training-data. https://github.com/semorrison/lean-training-data, 2023. ↗
  23. Leonardo de Moura and Sebastian 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, pp. 625–635.
  24. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
  25. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
  26. Tomáš Skřivan. Scientific computing in lean. https://github.com/lecopivo/SciLean, 2021. ↗
  27. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024. find
  28. Terence Tao. Pfr. https://github.com/teorth/pfr, 2023. ↗
  29. Joseph Tooby-Smith. Heplean: Digitalising high energy physics. arXiv preprint arXiv:2405.08863, 2024. — [arXiv:2405.08863](https://arxiv.org/abs/2405.08863) find
  30. Daniel J. Velleman. How to Prove It: A Structured Approach. Cambridge University Press, 3 edition, 2019. find
  31. Sean Welleck. Llmlean. https://github.com/cmu-l3/llmlean, 2024. ↗
  32. Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions in lean. arXiv preprint arXiv:2310.18457, 2023.
  33. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  34. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019.
  35. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023.
  36. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. Internlm-math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024.
  37. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/hu-2024-minictx-neural-theorem-proving-long/