自然语言数学证明的可靠细粒度评估

近期大语言模型（LLM）在数学推理方面的进展主要集中于具有易验证最终答案的任务，而生成与验证自然语言数学证明仍是开放挑战。我们识别出缺乏可靠、细粒度的LLM生成数学证明评估器为关键性空白。为此，我们提出了系统性的方法，用于开发和验证评估器，对模型生成的数学证明进行0-7分的细粒度评分。为支持本研究，我们引入ProofBench——首个由专家标注的细粒度证明评分数据集，涵盖145个来自六大数学竞赛（USAMO、IMO、Putnam等）的问题，以及来自Gemini-2.5-Pro、o3和DeepSeek-R1的435个LLM生成解答。使用ProofBench作为测试平台，我们系统性地探索了评估器设计空间的关键维度： backbone模型、输入上下文、指令及评估工作流程。我们的分析提出了ProofGrader——一种结合强推理 backbone LM、来自参考解答和 marking方案的丰富上下文，以及简单集成方法的评估器；其平均绝对误差（MAE）为0.926，显著优于朴素基线。最后，我们在最佳挑选任务中展示了其实际用途：在n=16时，ProofGrader实现4.14/7的平均分，弥合了78%的差距——从朴素的二元评估器（2.48）到人类专家（4.62），凸显了其在推动下游证明生成方面的潜力。