arXiv cs.CL· Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang·· 11 小时前AI 评分34
DAPS：面向 LLM 定理证明的依赖感知前提选择方法
DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
AI 导读
DAPS 是一种依赖感知的前提选择器，在 Mathlib4-Heldout 上达到 89.25 的平均 Recall@32，比强基线 LeanHammer 高出 11.41，并在两个分布外基准上保持领先。
正文 · 原文
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), and maintains this lead on two out-of-distribution benchmarks. Further experiments demonstrate that DAPS premises improve theorem proving on miniF2F and IMO-ProofBench. Project page: this https URL.
| Subjects: | Logic in Computer Science (cs.LO); Computation and Language (cs.CL); Machine Learning (cs.LG) |
| Cite as: | arXiv:2610.41536 [cs.LO] |
| (or arXiv:2610.41536v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2610.41536 arXiv-issued DOI via DataCite (pending registration) |
|
| Journal reference: | NeurIPS 2026 |
Submission history
From: Yinya Huang [view email]
[v1]
Fri, 30 Oct 2026 10:28:34 UTC (2,065 KB)
来源：arXiv cs.CL · arxiv.org