Source note
PROMISE: Proof Automation as Structural Imitation of Human Reasoning
Summary
PROMISE targets automated proof generation for large formal verification projects, where current LLM-based methods lose accuracy on long, interdependent proofs. It guides proof search with structurally similar proof-state transitions instead of relying on surface text matches to prior lemmas or scripts.
Problem
- Formal verification can give machine-checked correctness guarantees for safety-critical software, but proof construction is still expensive and requires expert interactive theorem proving.
- Existing LLM-based proof systems often treat proving as single-shot generation, next-tactic prediction, or text-based retrieval over lemmas and proofs; these methods struggle when proofs have deep dependencies across modules and files.
- On system-scale benchmarks such as seL4 or FSCQ, the paper states that proof coverage for mid-level lemmas often stays below 30% for prior methods, which limits practical use on verified systems software.
Approach
- PROMISE models a proof as a sequence of proof states and tactic-induced transitions, then searches for prior transitions that evolve in a similar way to the current proof state.
- It retrieves structurally compatible proof fragments based on proof-state evolution patterns, not just lexical similarity between theorem statements or proof text.
- It combines this structural retrieval with context-aware lemma retrieval from the active proof environment, using available lemmas whose roles fit the current goal state.
- The system runs as an iterative, stateful proof search loop that proposes short tactic continuations, checks them with the proof assistant, and expands the search using retrieved transition traces.
- The method is model-agnostic and uses off-the-shelf LLMs without extra training; the paper evaluates it with GPT-3.5-Turbo, Qwen2.5-Coder-7B-Instruct, and also discusses GPT-4.1 settings.
Results
- On the seL4 microkernel verification benchmark, PROMISE reports improvements of up to +26 percentage points, which the paper describes as a 186% relative gain, over prior LLM-based proof automation approaches.
- The paper compares against Selene and Rango and says PROMISE outperforms prior approaches in the majority of settings under the same query budget.
- In the single exception named in the excerpt, GPT-4.1/P2, PROMISE remains competitive with the strongest baseline rather than leading it.
- PROMISE keeps performance strong across different model sizes and capabilities; the excerpt says the gap between Qwen2.5-Coder-7B-Instruct and GPT-3.5-Turbo is small within PROMISE, while other methods show larger model sensitivity.
- The excerpt does not provide the full result table, exact success-rate values for each model, or per-benchmark breakdown beyond the headline +26-point / 186% improvement claim.