融合文本与依赖关系，提升形式化证明中前提选择的准确性
Combining Textual and Structural Information for Premise Selection in Lean
- 用图神经网络建模前提间的依赖关系，结合文本嵌入
- 在LeanDojo上比基线提升超25%的检索性能
- 适合形式化验证和自动化证明研究者参考
前提选择是制约大型形式化库中定理证明扩展的关键瓶颈。现有基于语言的方法常将前提孤立处理，忽略了它们之间的依赖网络。本文提出一种图增强方法，将Lean形式化文本的密集嵌入与异构依赖图上的图神经网络结合，捕捉状态-前提及前提-前提关系。在LeanDojo基准上，该方法在标准检索指标上超越ReProver语言基线超过25%。结果表明，关系信息对前提选择具有显著促进作用。
原文摘要 · Abstract (English)
Premise selection is a key bottleneck for scaling theorem proving in large formal libraries. Yet existing language-based methods often treat premises in isolation, ignoring the web of dependencies that connects them. We present a graph-augmented approach that combines dense text embeddings of Lean formalizations with graph neural networks over a heterogeneous dependency graph capturing both state-premise and premise-premise relations. On the LeanDojo Benchmark, our method outperforms the ReProver language-based baseline by over 25\% across standard retrieval metrics. These results suggest that relational information is beneficial for premise selection.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。