arXiv cs.LG· Jialin Lu, Xiaoyu Liu, Hengrui Luo, Rodrigo Stehling, Linxi Liu, Weiran Sun, Yuepeng Wang, Wuyang Chen·· 11 天前AI 评分39
Lean Finder V2：支持查询消歧的 Mathlib 语义搜索框架
Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
AI 导读
Lean Finder V2 是一种针对 Mathlib 的语义搜索框架，通过对抗训练与查询重写消除简短、模糊查询的歧义。在人工整理的 MathlibQR 基准上，该框架刷新 SOTA，较此前最优语义搜索引擎取得至少 11% 的相对提升。它在人类与编码智能体未标注查询测试中被评为最强系统，集成至 Claude Code 后提升了定理证明成功率。
来源：arXiv cs.LG · arxiv.org