Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Premise Selection for a Lean Hammer

Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck

TL;DR

This work presents LeanPremise, a novel neural premise selection system, and combines it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant.

Abstract

Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a tool that integrates premise selection, translation to external automatic theorem provers, and proof reconstruction into one overarching tool to automate tedious reasoning steps. We present LeanPremise, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selectors, LeanPremise is specifically trained for use with a hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LeanPremise's training data as well as lemmas defined by the user locally. With comprehensive evaluations, we show that LeanPremise enables LeanHammer to solve 21% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.

Premise Selection for a Lean Hammer

TL;DR

This work presents LeanPremise, a novel neural premise selection system, and combines it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant.

Abstract

Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a tool that integrates premise selection, translation to external automatic theorem provers, and proof reconstruction into one overarching tool to automate tedious reasoning steps. We present LeanPremise, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selectors, LeanPremise is specifically trained for use with a hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LeanPremise's training data as well as lemmas defined by the user locally. With comprehensive evaluations, we show that LeanPremise enables LeanHammer to solve 21% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.

Paper Structure

This paper contains 29 sections, 2 equations, 4 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Hammers in interactive proof assistants
  4. Neural theorem proving
  5. Premise selection
  6. Methods
  7. LeanHammer pipeline
  8. Data extraction
  9. Signature extraction
  10. State and premise extraction
  11. Premise selection
  12. Model training
  13. API integration
  14. Variations and extensions
  15. Experiments
  16. ...and 14 more sections

Figures (4)

  • Figure 1: Overview of the LeanHammer pipeline. Phases that can neither fail nor produce a terminal proof are green, phases that can fail but cannot produce a terminal proof are yellow, and phases that can produce a terminal proof are blue. Black solid arrows indicate control flow, while red dashed arrows indicate the transfer of information between phases.
  • Figure 2: Analysis of proof rate and execution speed in different settings.
  • Figure 3: Proof rate on Mathlib-valid by number of retrieved premises under full setting.
  • Figure 4: Analysis of theorem statistics by difficulty, on Mathlib-test with the full setting, depending on if the theorem was proven.