arXiv:2510.13888cs.CLcs.AI2025-10被引 13

为大模型生成的数学证明设计了精细评分系统,提升评估可靠性。

Reliable Fine-Grained Evaluation of Natural Language Math Proofs

  • 构建细粒度评分框架,基于参考解法和评分标准进行多维度评估。
  • 提出ProofGrader模型,对齐专家评分的平均误差仅0.926,显著优于基线。
  • 适用于数学竞赛证明生成的质量筛选,助力高质量输出优化。

大语言模型在数学推理领域进展迅速,但多数聚焦于答案可验证的任务,而自然语言数学证明的生成与验证仍具挑战。本文指出缺乏可靠、细粒度的评估工具是关键瓶颈。为此,提出系统化评估器开发与验证方法,实现对模型生成证明在0-7分制上的细粒度打分。为此构建ProofBench,首个由专家标注的细粒度证明评分数据集,涵盖145道来自美国数学奥林匹克(USAMO)、国际数学奥林匹克(IMO)、普特南数学竞赛(Putnam)等六大数学竞赛的题目,以及由Gemini-2.5-Pro、o3和DeepSeek-R1生成的435份解法。以ProofBench为基准,系统探索评估器设计空间,包括骨干模型、输入上下文、指令设计与评估流程。分析得ProofGrader:结合强推理模型、参考解法与评分标准的丰富上下文,采用简单集成策略;其平均绝对误差(MAE)仅为0.926,远超朴素基线。进一步在best-of-$n$选择任务中验证其实用性:当$n=16$时,平均得分达4.14/7,弥补了原始二值评估器(2.48)与人类基准(4.62)之间78%的差距,展现出推动下游证明生成的重要潜力。

原文摘要 · Abstract (English)

Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers while generating and verifying natural language math proofs remains an open challenge. We identify the absence of a reliable, fine-grained evaluator for LLM-generated math proofs as a critical gap. To address this, we propose a systematic methodology for developing and validating evaluators that assign fine-grained scores on a 0-7 scale to model-generated math proofs. To enable this study, we introduce ProofBench, the first expert-annotated dataset of fine-grained proof ratings, spanning 145 problems from six major math competitions (USAMO, IMO, Putnam, etc) and 435 LLM-generated solutions from Gemini-2.5-Pro, o3, and DeepSeek-R1. Using ProofBench as a testbed, we systematically explore the evaluator design space across key axes: the backbone model, input context, instructions and evaluation workflow. Our analysis delivers ProofGrader, an evaluator that combines a strong reasoning backbone LM, rich context from reference solutions and marking schemes, and a simple ensembling method; it achieves a low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming naive baselines. Finally, we demonstrate its practical utility in a best-of-$n$ selection task: at $n=16$, ProofGrader achieves an average score of 4.14/7, closing 78\% of the gap between a naive binary evaluator (2.48) and the human oracle (4.62), highlighting its potential to advance downstream proof generation.

数学推理评估方法大模型评测

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。