Re$^2$Math：基准测试研究级数学中的定理检索

大语言模型在封闭世界数学推理中表现优异，但研究辅助需基于文献的工具使用。本文提出 Re$^2$Math 基准，评估从部分证明中进行工具导向检索的能力。该任务要求识别现有工具、定位学术来源并验证假设一致性。实验显示，尽管系统能检索有效陈述，但确立其在局部证明步骤中的适用性仍是难点（最佳准确率仅 7.0%）。该基准通过解耦引用召回、基础 grounding 和证明缺口充分性，将文献支持的数学工具使用转化为可控诊断任务。