Lean Finder V2：面向 Mathlib 的语义搜索与查询消歧
🧭 语义搜索 · 查询改写与消歧
Simon Fraser University · Rice University · University of Pittsburgh
用对抗训练生成大规模短歧义查询，结合模型微调与输入层改写，在 MathlibQR 上至少相对提升 11%
📌 工作参考价值（4 点）
- 用对抗训练补足“短歧义 query”数据：电商搜索里“苹果”“nike 卫衣”等短查询经常缺 context；可仿照用生成模型 + 判别器迭代生成大量带标签的歧义 query，而不是只靠真实日志，显著扩充训练集，解决数据稀疏。
- 模型层 + 输入层双层消歧：同时 fine-tune 检索模型（增强对短 query 的鲁棒性）并在检索前对 query 做改写/补全（如加类目、属性、别名），两者互补；在商品搜索或 Agent 工具检索中可分开评估增量，避免只做单一层。
- 面向真实短查询做人类评估基准：构建少量人工标注的短 query benchmark，用 unlabeled 真实 human/agent 交互做 ranking 评估，比离线 dense retrieval 指标更贴近线上体验。
- 检索质量直接挂钩下游 agent 任务成功率：与 Claude Code 集成后证明 proof success 提升，说明 Agent 工具检索/商品召回改善能直接转化为任务成功；建议将检索召回作为 Agent 流程中的关键优化点。
LeanPRM：基于 Lean 的自然语言证明过程监督
🧭 过程监督 · Lean 自动标注
University of Texas at Austin · University of California, Los Angeles · New York University
利用 Lean 形式化证明自动生成自然语言证明的逐步正确性标签，训练过程监督验证器，步级准确率从 48.2 提升至 74.7
📌 工作参考价值（4 点）
- 对 Agent/多步决策轨迹，可借鉴「可执行环境自动打标签」：用沙盒、规则引擎或领域知识库对中间步骤做形式化校验，替代人工标注，低成本构建过程监督数据。
- 「分离形式错误与语义错误」的过滤模型思路值得迁移：先自动生成大量轨迹标签，再训练一个二分类器剔除仅因语法/格式失败但推理正确的负样本，避免污染奖励模型。
- 训练过程奖励模型时，可以混合少量人工标注与大量自动标注；本工作证明在没有人类标注的情况下，自动标签也能显著优于 PRM800K 人工标注，适合快速迭代线上推理链路。
- 对于电商推荐理由生成、搜索 query 改写等有可执行校验（如转化、点击、库存）的场景，可尝试用业务指标为中间步骤提供弱监督，再微调 LLM 做步骤级打分。