LLMSTEP: LLM proofstep suggestions in Lean
By Sean Welleck, Rahul Saha. 2023
42 citations recorded by the source corpus.
We present LLMSTEP, a tool for integrating a language model into the Lean proof assistant. LLMSTEP is a Lean 4 tactic that sends a user's proof state to a server hosting a language model. The language model generates suggestions, which are checked in Lean and displayed to a user in their development environment. We provide a baseline language model, along with code for fine-tuning and evaluation to support further development. We provide server implementations that run on CPU, a CUDA GPU, or a Google Colab notebook, as a step towards fast, effective language model suggestions for any user.
Subfields: Natural Language Processing, LLM Agents & Tool Use
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Natural Language Processing
- Zhangir Azerbayev
- Hailey Schoelkopf
- Stella Biderman
- Albert Qiaochu Jiang
- Sean Welleck
- Marco Dos Santos
- Keiran Paster
- Michael R Douglas
Citations in the corpus
- Llemma: An Open Language Model For Mathematics (2023, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”