REVIEW 3 cited by
LLMSTEP: LLM proofstep suggestions in Lean
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 3 Pith papers
-
What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus
A user study of eight experts shows that specification-first planning, low active errors, and measured verifier use predict proof task success, informing an AI proof agent design.
-
Clarifying Before Reasoning: A Coq Prover with Structural Context
Enriching LLM theorem-proving prompts with Coq's internal type representations and natural-language explanations raises proof success from 21.8% to 45.8%, surpassing Graph2Tac's 33.2%.
-
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
The proposed Faithful-Refiner, combining syntactic parsing, quantifier and consistency checks, logical-relation guidance, and detailed proof feedback, raises explanation refinement rates on three NLI benchmarks by lar...
Discussion (0). Sign in to comment.