LLMSTEP: LLM proofstep suggestions in Lean

1 Introduction

• Choosing the next tactic at each proof state is a fundamental part of proof development, so in-environment suggestions could ease that work.Interactive proof assistants verify mathematics and software using specialized programming languages.Source: §1 · p. 1
• LLMSTEP sends a Lean proof state to a language-model server, then checks and displays the generated tactic suggestions in the development environment.The tool is agnostic to the model, learning framework, and evaluation framework.Source: §1 · p. 1
• Its baseline model is fine-tuned for standard tactic prediction and outperforms recent open-source tactic-prediction models [19].The tool also provides fine-tuning and evaluation code, with server options for CPU, GPU, and Google Colab.Source: §1 · p. 1

2 Related Work

• Unlike gpt-f, which suggests Lean 3 proof steps through a now-disabled OpenAI API, LLMSTEP uses open-source components and can run on a user's device.LLMSTEP also supports prefixed and checked suggestions, uses Lean 4 metaprogramming, and provides code for fine-tuning and evaluation.Source: §2 · p. 1
• LeanInfer supports CPU inference for supported models and uses LLMSTEP utilities to check, format, and display suggestions; LLMSTEP adds prefix support and fast GPU inference.LLMSTEP is also agnostic to the language-model implementation.Source: §2 · p. 2
• Proofster offers machine-learning proof synthesis in Coq through a web interface, whereas LLMSTEP provides Lean 4 language-model tactic suggestions in the development environment.Figure 1 depicts LLMSTEP's proof-state-and-prefix request, server-generated suggestions, and Lean checking.Source: §2 · p. 2, Figure 1 · p. 2

3 Approach

• A user calls `llmstep <prefix>` in a proof; LLMSTEP returns suggestions beginning with that prefix for display in the Lean 4 Infoview.The user can click a suggestion to place it in the proof and continue from the resulting state.Source: §3 · p. 2, §3.1 · p. 3

3.1 Implementation

• LLMSTEP sends the current proof state and prefix to a server, then checks each returned tactic and displays invalid, valid, and complete suggestions in different colors.A valid tactic leaves at least one goal without errors; a complete tactic leaves no goals and no errors.Source: §3.1 · p. 2
• The default model predicts the next tactic from the current tactic state and is fine-tuned on state-and-next-tactic examples from Lean Mathlib via LeanDojo Benchmark 4.The default is Pythia 2.8b; LLMSTEP also supports ReProver and other Huggingface models.Source: §3.1 · pp. 2–3
• The server hosts the model, handles requests from the Lean tactic, and relays responses; it is the key computational bottleneck.Server implementations support CPU, CUDA GPU, Google Colab GPU, and vLLM inference.Source: §3.1 · p. 3
• Users start a server suited to their hardware, import LLMSTEP as a Lean 4 package, and invoke it with a prefix to receive Infoview suggestions.Available server settings include CPU, CUDA GPU, and Google Colab notebooks.Source: §3.1 · p. 3

Proof search

• Proof search uses best-first search with LeanDojo interaction, a 10-minute timeout, and beam expansion size 32.The comparison includes ReProver without retrieval and a second Pythia attempt of 32 samples to match 64 expansions.Source: §4 · p. 3
• Pythia exceeds ReProver in closed theorems on Lean Dojo Benchmark 4 and miniF2F.Table 1 reports proof search on the Lean Dojo random evaluation splits and miniF2F.Source: Table 1 · p. 3, §4 · p. 3

Runtime

• GPU inference returns suggestions in 1 second or less, with vLLM reaching 0.11s; ReProver is much faster on CPU.Runtime was measured across 17 examples; Figure 2 compares compute environments and models, and vLLM remains fast as suggestion count increases.Source: Figure 2 · p. 3, Table 2 · p. 4, §4 · p. 4

Qualitative examples

• With an empty prefix, LLMSTEP returns five suggestions: three finish the proof and two are valid.Source: Figure 3 · p. 4

• LLMSTEP provides accessible Lean 4 tactic suggestions and a fine-tuned model with strong mathlib and miniF2F performance, while faster CPU inference, improved models, and broader tasks remain future work.Source: §5 · p. 4