Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combining Textual and Structural Information for Premise Selection in Lean

Job Petrovčič, David Eliecer Narvaez Denis, Ljupčo Todorovski

TL;DR

Premise selection in Lean proof environments is hindered by ignoring library structure. The authors blend ByT5-based textual embeddings with a Relational Graph Convolutional Network over a heterogeneous Lean dependency graph to produce graph-aware representations for proof states and premises. On the LeanDojo Mathlib benchmark, the graph-augmented approach improves Recall@1, Recall@10, and MRR over a ReProver baseline, with additional gains from ensemble EMA, though ablations suggest training choices may drive much of the improvement. The work highlights the potential of incorporating structural dependencies into premise retrieval for tactic-based Lean proofs and points to future work on graph attention and alternative data splits.

Abstract

Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25\% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection.

Combining Textual and Structural Information for Premise Selection in Lean

TL;DR

Premise selection in Lean proof environments is hindered by ignoring library structure. The authors blend ByT5-based textual embeddings with a Relational Graph Convolutional Network over a heterogeneous Lean dependency graph to produce graph-aware representations for proof states and premises. On the LeanDojo Mathlib benchmark, the graph-augmented approach improves Recall@1, Recall@10, and MRR over a ReProver baseline, with additional gains from ensemble EMA, though ablations suggest training choices may drive much of the improvement. The work highlights the potential of incorporating structural dependencies into premise retrieval for tactic-based Lean proofs and points to future work on graph attention and alternative data splits.

Abstract

Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25\% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection.

Paper Structure

This paper contains 19 sections, 2 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction and related work
  2. State-premise dependency graph for Lean
  3. Augmented data extraction from the Mathlib Library
  4. Dataset statistics
  5. Methodology
  6. GNN-augmented premise retrieval
  7. Training objective
  8. Other optimizations
  9. Experiments and results
  10. Experimental setup
  11. Results
  12. Ablations
  13. Conclusion
  14. Acknowledgments
  15. Dataset statistic for Mathlib 4
  16. ...and 4 more sections

Figures (3)

  • Figure 1: A hypothetical Lean 4 theorem illustrating the extraction of the graph components. (a) The theorem premise_example becomes a premise node. (b) Signature hypotheses (with edges to premises Or, Not) and (c) the goal (with edges to premises And, Not) define signature dependency edges. (d) The tactic application creates a proof-dependency edge to premise not_or. The proof states (e.g., after the by keyword, Figure \ref{['lst:state1']}) become graph nodes linked to premises in their local hypotheses and goals.
  • Figure 2: Initial proof state immediately after by. State nodes are created for proof states. The initial state after by (in Figure \ref{['lst:state1']}) is linked to its local hypotheses ([Or, Not]) and goal premises ([And, Not]).
  • Figure 3: The updated proof state obtained after applying the tactic