cs.LG提交于 2026-10-23已译

Lean Finder V2：可消歧用户查询的 Mathlib 语义搜索

Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries

Jialin Lu · Xiaoyu Liu · Hengrui Luo · Rodrigo Stehling · Linxi Liu · Weiran Sun · et al.

中文摘要

Lean Finder V2 是面向 Mathlib 的语义搜索框架，通过模型级对抗训练(adversarial training)与输入级查询改写(query rewriting)消歧用户查询。人类数学家和编码智能体通常只输入简短属性、记号、别名或假设，不会提供完整上下文；现有搜索系统却往往假定查询包含丰富上下文。由于真实短查询及其对应的 Mathlib 标准陈述稀缺，该问题被视为数据问题。对抗训练可扩大带标签的简短歧义查询生成规模，并在模型微调和输入改写两个层面学习消歧。在人工整理的 MathlibQR benchmark 上，该方法达到新的最佳水平，相对此前最佳 Mathlib 语义搜索引擎至少提升 11%；进一步优化查询改写还能改善检索效果。在来自人类与编码智能体交互的无标签查询中，其整体排名最强。集成 Claude Code 后，该方法还提升了下游定理证明任务的证明成功率。项目地址：https://leanfinder.github.io/

关键要点

01现有 Mathlib 搜索不现实地假设查询包含丰富上下文。
02以数据扩充为核心，通过对抗训练生成带标签的简短歧义查询。
03结合模型级对抗微调与输入级查询改写进行查询消歧。
04MathlibQR 检索相对此前最佳系统至少提升 11%。
05集成 Claude Code 后提升了下游定理证明的成功率。

解读

尚无解读。

原始英文摘要

arXiv:2610.30843v1 Announce Type: new Abstract: We introduce Lean Finder V2, a semantic search framework for Mathlib that disambiguates user queries through complementary model-level adversarial training and input-level query rewriting. Human mathematicians and coding agents rarely search Mathlib by providing detailed context. In practice, they query short properties, notation, aliases, or hypotheses, leaving much of the intended mathematics implicit. In contrast, existing Mathlib search engines unrealistically assume context-rich queries. The scarcity of real-world short queries paired with ground-truth Mathlib statements makes this ambiguity even more intractable. We argue that this is essentially a data problem. Through adversarial training, we scale up the generation of labeled short and ambiguous queries, and learn to disambiguate user queries at both model-level fine-tuning and input-level query rewriting. On the human-curated MathlibQR benchmark, our Lean Finder V2 sets a new state of the art, with at least 11% relative improvement over the previous best Mathlib semantic search engines. On top of our state-of-the-art retriever, optimized query rewriting further improves MathlibQR retrieval. On unlabeled queries from human and coding-agent interactions, Lean Finder V2 is ranked as the strongest system. Integrated with Claude Code, Lean Finder V2 improves proof success on downstream theorem-proving task. Lean Finder V2 is available at: https://leanfinder.github.io/