LLMs preserve functional behavior in over 91% of generated VeriFast specifications and source code but achieve only 31.4% verification success, with 94% of failures due to separation logic domain knowledge errors.
LLMSTEP: LLM proofstep suggestions in Lean
4 Pith papers cite this work, alongside 3 external citations. Polarity classification is still indexing.
4
Pith papers citing it
3
external citations · Pith
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.
representative citing papers
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
A hierarchical attention regularizer improves pass@64 on Lean theorem proving benchmarks by about two percentage points, while its proof-complexity reduction is computed on a small subset and is less robust.
Deepseek-R1 can usually distinguish intended behavior from buggy implementations when writing ACSL specs, and augmenting prompts with Frama-C tool outputs measurably changes the type and focus of generated annotations.
citing papers explorer
-
An Empirical Study of LLM-Generated Specifications for VeriFast
LLMs preserve functional behavior in over 91% of generated VeriFast specifications and source code but achieve only 31.4% verification success, with 94% of failures due to separation logic domain knowledge errors.
-
Automating Formal Verification with Agent-Guided Tree Search
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.