arXiv cs.CL· Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang·· 10 小时前AI 评分34
DAPS：面向 LLM 定理证明的依赖感知前提选择方法
DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving
AI 导读
DAPS 是一种依赖感知的前提选择器，在 Mathlib4-Heldout 上达到 89.25 的平均 Recall@32，比强基线 LeanHammer 高出 11.41，并在两个分布外基准上保持领先。
正文 · AI 翻译
摘要：基于 LLM 的 Lean 4 定理证明已取得快速进展，但证明器难以利用新贡献的引理，因为检索会偏向流行的基础引理，使正确的前提被埋没在数十万个候选之中。现有的神经选择器按语义相似度对候选排序，存在三个固有局限：频率偏斜的检索、孤立的成对排序，以及在分布外查询（如竞赛题和非形式化语言）上的性能退化。鉴于数学是由依赖关系而非相似性构建的，我们将这一信号恢复到训练数据和模型中。我们整理了两个未被充分利用的依赖资源。我们首次对 53 个 Lean Blueprint 项目进行了系统性挖掘，这是一个此前未被利用的语料库，包含 3,805 个手工整理的非形式化+形式化节点，捕捉了 Mathlib4 中缺失的罕见研究级前提。我们进一步将其与全面的、带类型的、多层次的 Mathlib4 依赖提取相结合。然后我们引入 DAPS，一种依赖感知的前提选择器，具有结构邻域编码器、组级对比目标和 Mathlib-then-Blueprint 适应流程。DAPS 在 Mathlib4-Heldout 上达到 89.25 的平均 Recall@32（比强选择器 LeanHammer 高 11.41），并在两个分布外基准上保持领先。进一步实验表明，DAPS 前提改进了 miniF2F 和 IMO-ProofBench 上的定理证明。项目页面：此 https URL。
| 主题： | 计算机科学中的逻辑（cs.LO）；计算与语言（cs.CL）；机器学习（cs.LG） |
| 引用为： | arXiv:2610.41536 [cs.LO] |
| （或 arXiv:2610.41536v1 [cs.LO] 为此版本） | |
| https://doi.org/10.48550/arXiv.2610.41536 由 DataCite 颁发的 arXiv DOI（待注册） |
|
| 期刊 参考： | NeurIPS 2026 |
提交历史
来自：Yinya Huang [查看电子邮件]
[v1]
2026 年 10 月 30 日星期五 10:28:34 UTC（2,065 KB）
来源：arXiv cs.CL · arxiv.org