← 研踪 PaperTrailarXiv:2610.41536 · v2
DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
首次提交 2026-10-30 18:28
版本更新 2026-11-07 23:07
雷达观测 2026-11-10 11:14
摘要
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 78.74 Recall@16 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer) and widens the margin to 7xrecall on competition-style queries. Downstream, its selected premises raise Goedel-Prover-V2-8B Pass@4 on miniF2F-test from 49.90 to 54.03 and improve all four general-purpose LLMs on the informal IMO-ProofBench (up to +11.4% relative). Project page: https://daps-eth.github.io/.
期刊信息：NeurIPS 2026
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-07 23:07 · 最新观测版本
DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
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 78.74 Recall@16 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer) and widens the margin to 7xrecall on competition-style queries. Downstream, its selected premises raise Goedel-Prover-V2-8B Pass@4 on miniF2F-test from 49.90 to 54.03 and improve all four general-purpose LLMs on the informal IMO-ProofBench (up to +11.4% relative). Project page: https://daps-eth.github.io/.
查看此版本解读 →查看此版本原文 ↗