arXiv 机器学习· Jialin Lu, Xiaoyu Liu, Hengrui Luo, Rodrigo Stehling, Linxi Liu, Weiran Sun, Yuepeng Wang, Wuyang Chen·· 7 小时前AI 评分41
Lean Finder V2：消除用户查询歧义的 Mathlib 语义搜索框架
Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
AI 导读
研究人员推出 Mathlib 语义搜索框架 Lean Finder V2，结合模型层面的对抗微调与输入层面的查询重写来消除简短查询中的歧义。在人工构建的 MathlibQR 基准上，该模型取得 SOTA 表现，相对此前最佳语义搜索引擎至少提升 11%。该系统与 Claude Code 集成后，有效提升了下游定理证明任务的成功率。
来源：arXiv 机器学习 · arxiv.org