让数学家用自然语言快速找到合适定理的智能搜索工具
Lean Finder: Semantic Search for Mathlib That Understands User Intents
- 基于数学讨论聚类与用户意图模拟，优化语义匹配
- 相比前代工具和GPT-4o，检索准确率提升超30%
- 适配大模型证明器，助力形式化推理自动化
我们提出Lean Finder，一个理解数学家真实意图的Lean与mathlib语义搜索引擎。形式化定理证明进展常因难以定位相关定理及Lean 4语言学习成本高而受阻。现有搜索工具主要依赖形式陈述的自然语言转换，却忽视真实查询与表述间的差异。为此，我们提出以用户为中心的语义搜索：通过分析公开的Lean讨论语义并聚类，再在模拟用户意图的合成查询上微调文本嵌入，并结合多源反馈信号对齐数学家偏好，增强对用户目标的多维理解。在真实查询、非形式化陈述和证明状态上的评估表明，相较于先前搜索系统和GPT-4o，Lean Finder实现超过30%的相对性能提升。此外，该系统兼容基于大模型的定理证明器，实现检索与形式推理的无缝衔接。项目地址：https://leanfinder.github.io
原文摘要 · Abstract (English)
We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over $30\%$ relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。