Llmstep: LLM Proofstep Suggestions in Lean
Abstract
We present $\texttt{llmstep}$, a tool for suggesting proof steps with a language model in the Lean 4 proof assistant. $\texttt{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.
Cite
Text
Welleck and Saha. "Llmstep: LLM Proofstep Suggestions in Lean." NeurIPS 2023 Workshops: MATH-AI, 2023.Markdown
[Welleck and Saha. "Llmstep: LLM Proofstep Suggestions in Lean." NeurIPS 2023 Workshops: MATH-AI, 2023.](https://mlanthology.org/neuripsw/2023/welleck2023neuripsw-llmstep/)BibTeX
@inproceedings{welleck2023neuripsw-llmstep,
title = {{Llmstep: LLM Proofstep Suggestions in Lean}},
author = {Welleck, Sean and Saha, Rahul},
booktitle = {NeurIPS 2023 Workshops: MATH-AI},
year = {2023},
url = {https://mlanthology.org/neuripsw/2023/welleck2023neuripsw-llmstep/}
}