Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
作者: Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov, Martin Vechev
分类: cs.CL
发布日期: 2026-05-11
备注: 9 main text pages, 36 total pages, In proceedings to 2026 NeurIPS Evaluations and Datasets Track
💡 一句话要点
提出ProofRank基准以量化评估大模型数学证明的质量，超越单纯的正确性评价。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大语言模型 数学推理 基准测试 逻辑证明 可解释性 认知负荷 模型评估
📋 核心要点
- 现有数学推理评估主要关注结果正确性，忽视了证明过程的清晰度、简洁性与认知负担等深层质量维度。
- 论文提出了ProofRank基准，通过简洁性、计算简易性、认知简单性、多样性和适应性五个维度量化评估证明质量。
- 实验表明，模型在正确性与证明质量之间存在显著权衡，证明了多维度评估对于衡量LLM数学推理实用性的必要性。
📝 摘要（中文）
大语言模型（LLM）已展现出强大的数学解题能力，常能为复杂问题提供正确证明。然而，仅凭正确性不足以衡量证明的优劣，高质量的数学证明还应具备清晰、简洁、深刻及可迁移性。尽管证明质量具有主观性，但其核心要素是具体且普适的。本文识别了这些关键要素，并引入了ProofRank基准，该基准基于具有挑战性的数学竞赛题目构建。ProofRank通过五个可扩展的代理指标评估证明质量：简洁性（避免冗余步骤）、计算简易性（减少繁琐计算）、认知简单性（技术易于理解）、多样性（模型生成证明的差异度）以及适应性（遵循特定证明技术的能力）。研究发现，不同模型在这些指标上存在显著差异，且这些差异在仅关注正确性的基准中无法体现。此外，证明质量指标与正确性之间存在显著权衡，表明未来的数学推理评估应更关注模型生成证明的实用价值。
🔬 方法详解
问题定义：现有LLM数学评估体系过度依赖“正确性”这一二元指标，忽略了数学证明在教育、科研中所需的逻辑清晰度、简洁性及可读性，导致模型可能通过冗长或晦涩的路径得出正确答案。
核心思路：将主观的“证明质量”拆解为可量化的代理指标。通过构建ProofRank基准，从五个维度对模型生成的证明进行多维画像，从而揭示模型在推理风格和逻辑构建上的本质差异。
技术框架：ProofRank基于数学竞赛数据集构建，通过自动化指标与模型辅助评估相结合的方式，对生成的证明进行打分。框架包含五个核心模块：简洁性评估（步骤冗余度）、计算复杂度分析、认知负荷评估（技术难度）、多样性度量（解法空间覆盖）以及适应性测试（约束遵循能力）。
关键创新：首次将数学证明的“质量”从定性分析转向定量评估，通过多维代理指标捕捉模型在推理过程中的逻辑偏好，揭示了正确性与证明质量之间的非线性关系。
关键设计：采用了基于LLM-as-a-judge的评估范式，利用强模型对弱模型的证明过程进行打分，并结合符号化分析工具（如计算步数统计）来增强评估的客观性与可解释性。
🖼️ 关键图片
📊 实验亮点
实验发现，即使在正确性表现相近的模型间，证明质量也存在显著差异。研究揭示了“正确性”与“简洁性/认知简单性”之间的负相关权衡，即模型为了追求正确性往往倾向于使用更繁琐的计算路径。ProofRank成功量化了这些差异，证明了仅靠正确性指标无法全面反映模型的数学推理水平。
🎯 应用场景
该研究可应用于大模型的训练优化与评估体系升级。在教育领域，可筛选出更具启发性和易读性的证明，辅助学生学习；在科研辅助中，可评估模型生成的证明是否符合数学直觉，提升模型在形式化验证与数学发现中的实用价值，推动LLM向更严谨的推理方向发展。
📄 摘要（原文）
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.