NeurIPS 2026

DAPS: Dependency-Aware Premise Selection
for LLM Theorem Proving

Zixuan Chen1, Wenyuan Jiang1, Junling Wang1,2, Mrinmaya Sachan1, Yinya Huang1,2,*

1 ETH Zurich 2 ETH AI Center

* Corresponding author

Paper Models & Datasets Code
Figure 1. Mathlib4 dependencies on the left and Lean Blueprint dependencies on the right, connecting Lean declarations, formal proofs, and informal mathematical statements.
Figure 1. One dependency graph spanning Mathlib4 (left) and a representative Blueprint project (right). The two resources differ in density and composition. Mathlib4 averages 24 edges per node with strong directional asymmetry across node types, while Blueprint dependencies are much sparser, averaging 1.2, but carry research-level out-of-Mathlib4 declarations and informal LaTeX signals. Click the figure to view the original PDF.

Abstract

LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the right premises buried among hundreds of thousands of candidates. Existing neural selectors rank candidates by semantic similarity, with three intrinsic limitations: frequency-skewed retrieval, isolated pairwise ranking, and degradation on out-of-distribution queries such as competition problems and informal language. Given that mathematics is structured by dependencies rather than similarities, we restore this signal to both the training data and the model. We curate two underused dependency resources. We conduct the first systematic mining of 53 Lean Blueprint projects, a previously untapped corpus of 3,805 manually curated informal+formal nodes that capture rare, research-level premises absent from Mathlib4. We further pair it with the extraction of comprehensive, typed, multi-level Mathlib4 dependencies. We then introduce DAPS, a dependency-aware premise selector with a structural neighborhood encoder, a group-level contrastive objective, and a Mathlib-then-Blueprint adaptation procedure. DAPS reaches mean Recall@32 of 89.25 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer) across three runs, maintains this lead on two out-of-distribution benchmarks, improves four general-purpose LLMs on the informal IMO-ProofBench, and raises Goedel-Prover-V2-8B Pass@4 on miniF2F-test from 49.90 to 54.03 when its selected premises are supplied.

BibTeX