DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
作者: Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang
分类: cs.LO, cs.CL, cs.LG
发布日期: 2026-10-30
期刊: NeurIPS 2026
🔗 代码/项目: PROJECT_PAGE
💡 一句话要点
提出DAPS以解决LLM定理证明中的前提选择问题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)
关键词: 定理证明 依赖关系 前提选择 机器学习 数学推理 神经网络 Lean 4 自动化
📋 核心要点
- 现有的定理证明方法在利用新引理时存在检索偏向和性能下降的问题，难以挖掘合适的前提。
- DAPS通过引入依赖关系信号，结合结构邻域编码器和对比目标，改善了前提选择的准确性。
- DAPS在Mathlib4-Heldout上达到了89.25的Recall@32，相较于LeanHammer提升了11.41，并在多个分布外基准上保持领先。
📝 摘要（中文）
基于LLM的定理证明在Lean 4中取得了快速进展，但现有方法难以有效利用新贡献的引理，因为检索偏向于流行的基础引理，导致合适的前提被埋没在数十万个候选中。现有的神经选择器通过语义相似性对候选进行排名，但存在频率偏倚检索、孤立的成对排名以及在分布外查询（如竞赛问题和非正式语言）上的性能下降等三大内在局限。鉴于数学是由依赖关系而非相似性构成的，本文恢复了这一信号，提出了DAPS，一个依赖感知的前提选择器，显著提升了定理证明的效果。
🔬 方法详解
问题定义：本文旨在解决LLM定理证明中前提选择的有效性问题，现有方法在检索时偏向流行引理，导致合适前提被忽视。
核心思路：DAPS通过引入依赖关系信号，强调数学结构中的依赖性，而非单纯的相似性，从而提高前提选择的准确性。
技术框架：DAPS的整体架构包括结构邻域编码器、组级对比目标和Mathlib-then-Blueprint适应过程，旨在系统性地挖掘和利用依赖关系。
关键创新：DAPS的核心创新在于引入依赖感知机制和结构化的前提选择方法，与传统的基于相似性的选择器相比，能够更好地捕捉数学中的复杂依赖关系。
关键设计：在模型设计中，采用了多层次的依赖关系提取和组级对比损失函数，确保模型在训练过程中能够有效学习到不同层次的依赖信息。通过对Lean Blueprint项目的系统挖掘，DAPS能够利用稀有的研究级前提。
🖼️ 关键图片
📊 实验亮点
DAPS在Mathlib4-Heldout上实现了89.25的Recall@32，较强选择器LeanHammer提升了11.41，并在miniF2F和IMO-ProofBench等分布外基准上保持领先，证明了其在定理证明中的有效性。
🎯 应用场景
该研究的潜在应用领域包括自动定理证明、数学知识库的构建以及教育领域的智能辅导系统。DAPS的创新方法能够帮助研究人员和学生更有效地利用数学引理，提升定理证明的效率和准确性，具有重要的实际价值和未来影响。
📄 摘要（原文）
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: https://daps-eth.github.io/.