Elamur Research⌕
☰
home / papers / 2023 / LLMSTEP: LLM proofstep suggestions in Lean

LLMSTEP: LLM proofstep suggestions in Lean

Paper · 2023 · Sean Welleck and Rahul Saha

Summary

Picking the next tactic is one of the hardest parts of writing formal proofs. Earlier language-model helpers for Lean, such as the gpt-f tactic for Lean 3, relied on a closed API that has since been shut down. LLMSTEP replaces this with an open-source Lean 4 tactic. The user writes llmstep with an optional prefix. The current proof state goes to a Python server hosting a language model. Lean then executes each returned tactic, labels it as proof-closing, valid or invalid, and lists it as a clickable item in the VS Code Infoview.

The tool works with any model. The authors provide a default Pythia 2.8b model fine-tuned on state/next-tactic pairs from Mathlib (via LeanDojo Benchmark 4), code for fine-tuning and best-first-search evaluation, and servers for CPU, CUDA GPU, Google Colab and vLLM. The default model closes slightly more theorems than ReProver on mathlib4 and clearly more on miniF2F. With vLLM on a GPU, suggestions arrive almost instantly. This makes LLM help practical on a user's own hardware and gives neural theorem proving research a reusable base.

Key points

  • Architecture: a Lean 4 metaprogram (the tactic) talks to a Python model server. The default model is trained in the proofstep format [GOAL]…[PROOFSTEP]…, and ReProver plus other Huggingface models are supported directly.
  • Proof search used best-first search with a 10-minute timeout. Pythia 2.8b at 2×32 samples reached 50.1% on mathlib4-test, versus 48.6% for ReProver without retrieval at 1×64.
  • miniF2F-test: Pythia 2.8b proved 27.9% (68/244) of theorems, versus 22.1% (54/244) for ReProver.
  • Runtime was averaged over 17 examples, with times given for one and for ten suggestions:
    • vLLM on a GTX 1080Ti: 0.11 s and 0.25 s.
    • Colab T4 GPU: about 1.0 s for one suggestion.
    • Laptop CPU: Pythia took 8.39 s for one suggestion, while the small ReProver model took 0.95 s.
    • The authors therefore advise using ReProver on CPU-only machines and Pythia on machines with a GPU.
  • Availability: code is at github.com/wellecks/llmstep. The later LeanInfer tool reuses LLMSTEP's utilities for checking and displaying suggestions.

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, topics and concepts

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

🧭 Topics 1Research subjects and languages the work is about.Language models & pretraining · 4,145 works

Cite

Cite as Sean Welleck and Rahul Saha. 2023. LLMSTEP: LLM proofstep suggestions in Lean. arXiv:2310.18457.

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

@misc{welleck2023llmstep,
  title = {{LLMSTEP: LLM proofstep suggestions in Lean}},
  author = {Sean Welleck and Rahul Saha},
  year = {2023},
  doi = {10.48550/arxiv.2310.18457},
  eprint = {2310.18457},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.18457}
}

References

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

  1. Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, and Yuriy Brun. Proofster: Automated Formal Verification. In Proceedings of the Demonstrations Track at the 45th International Conference on Software Engineering (ICSE), pages 26–3… — [doi:10.1109/icse-companion58688.2023.00018](https://doi.org/10.1109/icse-companion58688.2023.00018) find
  2. Jeremy Avigad. Mathematics and the formal turn. Bulletin (New Series) of the American Mathematical Society, Received by the editors October 2, 2023., 2023. URL https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdf. ↗
  3. 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.06786, 2023.
  4. Stella Rose Biderman, Hailey Schoelkopf, Quentin G. Anthony, Herbie Bradley, Kyle O’Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, Usvsn Sai Prashanth, Edward Raff, Aviya Skowron, Lintang Sutawika, and Oskar van der Wal. Pythia: A suite for analyzing large language models across train… find
  5. 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
  6. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models, 2023.
  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. Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles, 2023.
  9. mathlib. The lean mathematical library. In CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020, 2020. ISBN 9781450370974. doi: 10.1145/3372885.3373824.
  10. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
  11. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
  12. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at large: A survey of engineering of formally verified software. Foundations and Trends in Programming Languages, 2019. ISSN 23251131. doi: 10.1561/2500000045. — [doi:10.1561/2500000045](https://doi.org/10.1561/2500000045) find
  13. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Leaninfer: Neural network inference in lean 4. https://github.com/lean-dojo/LeanInfer, 2023. ↗
  14. The Coq Development Team. The coq proof assistant, oct 2019. URL https://doi.org/10. 5281/zenodo.3476303. find
  15. Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach to formal theorem-proving. ArXiv, abs/2310.04353, 2023. URL https://api.semanticscholar.org/CorpusID:263829101. ↗
  16. Sean Welleck. Neural theorem proving tutorial. ntptutorial, 2023. https://github.com/wellecks/ ↗
  17. Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow. The isabelle framework. In Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21, pages 33–38. Springer, 2008.
  18. Kaiyu Yang. Leandojo benchmark 4, jun 2023. URL https://doi.org/10.5281/zenodo. 8040110. — [doi:10.5281/zenodo](https://doi.org/10.5281/zenodo) ↗
  19. 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.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-lean/