Lean Finder：理解用户意图的 Lean 数学库语义搜索
机器学习
2026-02-24 v2 人工智能
摘要
我们提出了 Lean Finder，一个理解并与数学学家意图相匹配的 Lean 和 mathlib 语义搜索引擎。形式定理证明的进展往往受限于查找相关定理和 Lean 4 语言学习曲线陡峭的难度，使得进展缓慢且费力。虽然已有的 Lean 搜索引擎虽有帮助，但主要依赖于非正式化表述（即对形式陈述的自然语言翻译），而忽略了与真实用户查询之间的不匹配。在 contrast，我们提出一种面向数学学家的以用户为中心的语义搜索，致力于满足其需求。我们的 метод首先分析和聚类公开 Lean 讨论的语义，然后在模拟用户意图的查询上进行微调文本嵌入。我们进一步通过多样化的反馈信号将 Lean Finder 与数学学家的偏好相匹配，编码出对其目标从多个角度的深入认识。针对真实查询、非正式化表述和证明状态的评估显示，我们的 Lean Finder 相较于之前的搜索引擎和 GPT-4o 实现了超过 30% 的相对改进。此外，Lean Finder 与基于 LLM 的定理证明器兼容，桥接了检索与形式推理。Lean Finder 可在 https://leanfinder.github.io 访问。
引用
@article{arxiv.2510.15940,
title = {Lean Finder: Semantic Search for Mathlib That Understands User Intents},
author = {Jialin Lu and Kye Emond and Kaiyu Yang and Swarat Chaudhuri and Weiran Sun and Wuyang Chen},
journal= {arXiv preprint arXiv:2510.15940},
year = {2026}
}