评估大模型证明质量，不止看对错，还要看清晰、简洁、可迁移。
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
- 提出ProofRank基准，从简洁性、计算难度等五方面量化证明质量。
- 不同模型在证明质量上差异显著，且与正确率存在权衡。
- 适合关注数学推理实用性与可读性的研究者参考。
大型语言模型（LLMs）已具备解决复杂数学问题的能力，常能生成正确答案。但仅正确不足以衡量其价值：数学证明还需清晰、简洁、有洞察力且可迁移。尽管证明质量具有主观性，其部分特征仍具普遍价值。本文识别出这些特征，构建了来自高难度数学竞赛的ProofRank基准，用于评估五类可扩展的证明质量代理指标：(i) 简洁性，衡量是否避免冗余步骤；(ii) 计算简便性，衡量对繁琐计算的依赖程度；(iii) 认知简单性，衡量所用技巧的可理解性；(iv) 多样性，衡量同一问题下生成证明的多样性；(v) 适应性，衡量模型能否遵循指定证明方法。实验显示，各模型在证明质量上存在显著差异，且这些差异无法通过仅评估正确性的基准捕捉。此外，各项质量指标与正确率之间存在明显权衡，提示未来数学推理评估应关注生成证明的实际效用。
原文摘要 · Abstract (English)
Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient: mathematical proofs should also be clear, concise, insightful, and transferable to other problems. While this proof quality is subjective and depends on the reader and context, many of its components are concrete and broadly valued. In this work, we identify such components and introduce ProofRank, a benchmark curated from challenging mathematical competitions. ProofRank evaluates several scalable proxies of proof quality: (i) conciseness, measuring whether proofs avoid unnecessary steps; (ii) computational ease, measuring the extent to which a proof relies on tedious calculations; (iii) cognitive simplicity, measuring how accessible the used proof techniques are; (iv) diversity, measuring how varied a model's proofs for a single problem are; and (v) adaptivity, measuring whether a model can follow a specified proof technique. Across models, we find substantial differences in proof quality that are not captured by correctness-only benchmarks. We also observe significant trade-offs between proof-quality metrics and correctness, suggesting that future evaluations of mathematical reasoning should measure how useful LLM-generated proofs are.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。