LLMSTEP: LLM proofstep suggestions in Lean
This work addresses the challenge of making language model suggestions accessible and efficient for users of proof assistants like Lean, though it is incremental as it builds on existing methods.
The authors tackled the problem of integrating language models into proof assistants by developing LLMSTEP, a tool that provides proof step suggestions in Lean, resulting in a baseline model and server implementations for various hardware.
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.