arXiv · ML· Jialin Lu, Xiaoyu Liu, Hengrui Luo, Rodrigo Stehling, Linxi Liu, Weiran Sun, Yuepeng Wang, Wuyang Chen·· 4 小时前AI 评分20
Lean Finder V2：通过语义搜索消解 Mathlib 用户查询歧义
Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
AI 导读
Lean Finder V2 通过模型级对抗训练与输入级查询重写实现 Mathlib 语义搜索。在 MathlibQR 基准上较前最优引擎提升至少 11%，成为最强系统。 集成 Claude Code 后，该系统提升了下游定理证明任务的成功率。
来源：arXiv · ML · arxiv.org