Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
PROMISE is introduced, a structure-aware framework for automated proof generation that reframes the problem as a stateful search over proof-state transitions. It mines structural patterns from proof states and tactic transitions to retrieve and adapt compatible proof fragments during iterative search, addressing the limitations of single-shot or shallow retrieval methods. Evaluated on the seL4 benchmark, PROMISE achieves up to a 26-point improvement over prior methods, demonstrating the effectiveness of structure-aware proof mining for scalable theorem proving.
LLMs can now prove theorems at scale, thanks to a new structural mining approach that boosts performance by 26 points on the notoriously difficult seL4 verification benchmark.
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.