用13个数学领域测试证明模型，发现准确率掩盖了真实短板。
MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
- 分模块评估模型在形式化、推理和抗变形上的表现
- 数学等价改写下模型鲁棒性严重下降
- 适合研究AI数学推理能力与局限性的学者
形式化定理证明支持可验证的数学推理评估，但现有基准多关注整体证明准确率，覆盖范围窄，且缺乏对等价重述鲁棒性的检验。我们提出MathAdv，一个涵盖本科至研究生水平13个数学领域的诊断性基准。结合Lean 4定理证明器，MathAdv提供最多三项辅助任务：检测数学知识的多选题、分离非正式推理的填空题，以及专家设计的变换以测试对问题呈现方式的鲁棒性。对当代定理证明器的评估得出四项发现：形式化仍是主要瓶颈；不同数学领域表现差异显著；自然语言引导有助于通用大模型，但会干扰专用模型；数学等价改写暴露了严重的鲁棒性缺陷。这些结果表明，组件级评估能揭示整体准确率无法反映的模型能力与失效模式。数据集与评估脚本已开源。
原文摘要 · Abstract (English)
Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。