PROMISE: Proof Automation as Structural Imitation of Human Reasoning

TL;DR

PROMISE introduces a structure-aware framework for automated proof generation that leverages structural patterns in proof states, significantly improving scalability and performance over prior methods in formal verification tasks.

Contribution

It presents PROMISE, a novel proof mining approach that uses structural embeddings to enhance proof search and adaptation, outperforming existing LLM-based systems.

Findings

PROMISE achieves up to +26 points (186% relative gain) over prior methods.

It maintains robustness across multiple LLM backends.

PROMISE outperforms systems like Selene and Rango on the seL4 benchmark.

Abstract

Automated proof generation for formal software verification remains largely unresolved despite advances in large language models (LLMs). While LLMs perform well in NLP, vision, and code generation, formal verification still requires substantial human effort. Interactive theorem proving (ITP) demands manual proof construction under strict logical constraints, limiting scalability; for example, verifying the seL4 microkernel required decades of effort. Existing LLM-based approaches attempt to automate this process but remain limited. Most rely on single-shot generation or shallow retrieval, which may work for small proofs but fail to scale to large, interdependent verification tasks with deep structural dependencies. We present PROMISE (PROof MIning via Structural Embeddings), a structure-aware framework that reframes proof generation as a stateful search over proof-state transitions. Instead of surface-level retrieval, PROMISE mines structural patterns from proof states and tactic transitions, enabling retrieval and adaptation of compatible proof fragments during iterative search. We evaluate PROMISE on the seL4 benchmark across multiple LLM backends and compare it with prior systems such as Selene and Rango. PROMISE consistently outperforms prior methods, achieving up to +26 point improvements (186% relative gain) while maintaining robustness across models, demonstrating the effectiveness of structure-aware proof mining for scalable theorem proving.