Re²Math：研究级数学中定理检索的基准

大语言模型在封闭世界数学推理方面的能力越来越强，但研究援助也需要基于来源的文献使用。当证明达到重要步骤时，有用的助手应该确定所需的工具（例如引理）是否已经存在，确定合适的学术来源，并验证其假设是否与当前证明上下文一致。为了严格评估此类功能，我们引入了 Re$^2$Math，这是基于工具的部分数学证明检索的基准。每个实例都是根据主定理证明中的候选工具引用构建的，具有分层上下文和可选的泄漏控制锚点提示。我们还使任务基于来源但与引用无关，因为任何足以证明转换的可接受定理都会被接受。评估使用发布冻结的检索工件，确保可重复性，而基准本身支持自动、持续扩展新构建的实例。在当前的基准测试集上，尽管源接地率大幅提高，但最佳固定判断 ToolAcc 仍达到 7.0%，这表明当前系统经常检索有效语句，但无法确定其对本地证明步骤的适用性。通过解耦引文回忆、基础和证明差距充分性，Re$^2$Math 将基于文献的数学工具的使用转变为受控的诊断任务。