上海交大等联手揭秘：为何顶尖AI在"大学数学证明"面前屡屡翻车？

这项由上海人工智能实验室、上海交通大学、香港中文大学MMLab及大湾区大学联合开展的研究，以预印本形式发布于2026年7月13日，论文编号为arXiv:2607.11849，有兴趣深入了解的读者可通过该编号查阅完整原文。

你有没有想过，那些在高考数学题上轻松拿满分、在国际数学奥林匹克竞赛题目上也能对答如流的AI系统，一旦碰到大学本科的证明题，表现会是什么样？研究团队给出的答案，可能会让你大吃一惊。

这项研究的出发点，来自一个现实中的困惑。现有的数学基准测试，大多相当于在考AI的"填空题"能力——给出一个问题，AI算出一个最终答案，对了就得分，错了就扣分。但真正的数学，远不是这么回事。数学的核心在于"证明"，也就是用一步步严密的逻辑推理，从已知条件出发，让结论无懈可击地成立。就像一名律师在法庭上不仅要说出"被告无罪"，还必须拿出每一条证据链，环环相扣，让每一步推理都经得起质疑。

现有的评测体系，恰恰对这条"证据链"视而不见。AI可能歪打正着地写出正确答案，却在过程中漏洞百出；也可能因为最终答案写法略有差异而被判错，尽管整个证明过程完全正确。这种只看结果、不看过程的评测方式，严重低估了AI在严谨数学推理上的真实短板。

正是为了填补这一空白，研究团队构建了一套名为AdvancedMathBench的评测套件，专门用来检验AI在高阶数学证明上的真实水平。这套工具分为两个核心部分：一个叫ProverBench，专门测试AI能不能写出完整、正确的数学证明；另一个叫VerifierBench，专门测试AI能不能判断别人写的证明是否正确，并指出问题所在。

一、考题从哪里来：一份精心筛选的数学"卷子"

要考察AI的真实数学水平，首先得有一套足够有分量的题目。研究团队为此花了相当多的心思，从四个渠道广泛收集素材。

第一个渠道是国内顶尖高校的本科课程考试题，包括复旦大学、北京大学和上海交通大学的历年考题。第二个渠道是国际顶尖院校的博士资格考试题，包括斯坦福大学、加州大学洛杉矶分校、清华大学和约翰斯·霍普金斯大学的考题——博士资格考试可以理解为博士生在攻读学位过程中必须闯过的一道关卡，难度远高于本科。第三个渠道是丘成桐大学生数学竞赛的历年真题，这是国内数学竞赛中含金量极高的一项。第四个渠道是系统性地从各数学分支的权威教材中提取练习题，以保证题目覆盖面足够广。

有了原始素材，接下来还需要层层筛选。研究团队先把所有材料统一解析成结构化的电子格式，然后毫不留情地删掉所有"判断题"、"选择题"、"填空题"——因为这些题型可以靠猜测或者只看最终答案来应付，不需要真正的逻辑推导。只有那些必须写出完整证明过程才能作答的题目，才有资格留下来。

接下来还有一道"难度预筛"工序。研究团队让多个顶尖AI模型分别对每道题生成若干份证明，然后用一个专门的验证模型反复判断这些证明是否正确。如果一道题的所有AI答案都被判为正确，说明这道题太简单，直接淘汰。保留的是那些让AI产生分歧、难以稳定判断的题目——这些才是真正能考验AI极限的好题。

最后一关是人工审核。具有博士级别数学训练背景的专家逐一审查保留下来的每道题，确认题目表述清晰、参考解答正确，并剔除掉那些表述模糊、内容重复或者已经在网络上被广泛传播（可能造成数据污染）的题目。经过这整套流程，最终形成了245道证明题，构成了ProverBench；同时整理出888份由AI生成的证明稿件，配上专家标注，构成了VerifierBench。

二、证明题是怎么分级的：本科生卷与博士卷的差距有多大

最终的ProverBench分成两个难度层次。第一层叫做UG组，即本科生组，共200道题，内容涵盖概率论、数学分析、微分方程、高等代数、统计学、高等分析、几何学、离散数学、数值分析等本科阶段的核心科目。第二层叫做QE组，即博士资格考试组，共45道题，内容集中在图论、几何与拓扑学、代数、分析以及应用与计算数学这五个方向。

光看题目数量，QE组只有UG组的零头，但不要被这个数字迷惑。QE组的题目需要的是研究生乃至博士层面的数学修养，考察的不只是能否运用公式，而是能否在抽象的数学结构中进行深层次的逻辑演绎。拿图论和拓扑学来说，这些领域的问题经常需要把直觉上看起来"显然"的命题，通过极其严密的步骤从基本公理出发一步步论证出来，任何一个跳步都可能让整个证明崩塌。

后续的实验结果也完全印证了这一点。几乎所有AI模型在从UG组切换到QE组时，得分都出现了明显跳水，有的甚至腰斩。

三、如何评判一个证明是否正确：不依赖标准答案的"法官"系统

这里有一个非常棘手的问题。数学证明不像填空题，不存在唯一标准答案。同一道定理，可以用代数方法证，可以用分析方法证，可以用构造法证，甚至可以用反证法证。只要逻辑严密、结论正确，条条大路通罗马。因此，研究团队不能简单地把AI的证明和参考答案做文字比对，然后判断对错。

为此，研究团队专门训练了一个自动验证程序，可以称之为"证明法官"。这位法官不只是给证明贴上"对"或"错"的标签，还能指出证明在哪一步出了问题，属于什么性质的错误。

训练这位法官同样需要大量的素材。研究团队为ProverBench中的每道题，额外让多个强力AI模型生成更多证明稿件，形成丰富多样的训练数据池。此外，他们还运用了一种"迭代修改"的策略，专门生成质量较高的候选证明，以保证训练数据涵盖各种难度和风格的证明。

然而，这里又遇到了一个棘手的偏差问题。因为训练数据的筛选策略倾向于保留那些让验证模型"拿不定主意"的证明，这些模糊案例自然而然地偏向于错误证明，导致训练数据中错误样本占比偏高。一旦法官在这种数据上训练，就会形成"宁可错杀，不可放过"的偏执性格，对正确的证明也疑神疑鬼，误判率很高。

研究团队设计了一套"正样本扩充"方案来纠偏。专家先对错误证明给出修改建议，然后引导原来的AI模型根据建议修改证明，修改后的版本再经过DeepSeek-V4-Pro和GPT-5.5等强力模型的审核，通过审核的才被添加为正确证明的训练样本。这一过程额外补充了约1200份高质量的正确证明案例。

在此基础上，研究团队还用强化学习进一步打磨法官的能力。具体做法是：不只奖励法官给出正确的对错判断，还奖励法官写出与专家意见深度吻合的分析理由。这就像培养一个裁判，不只要求他判球进还是没进，还要求他能说清楚为什么是这个判决，理由是否经得起专家推敲。通过这种方式，法官在识别错误证明方面的能力有了显著提升，尤其是那种表面上很像正确证明、实际上暗藏致命漏洞的"伪正确"证明。

最后，研究团队还采用了一种名为"悲观验证"的策略。对每份AI生成的证明，法官要独立进行8次验证。只要有任何一次验证发现了问题，这份证明就直接被判为不通过。只有8次验证全部通过，这份证明才算获得认可。这就像在法庭上采用"无罪必须无懈可击"的标准，任何一个陪审员提出质疑，都足以推翻无罪判决。在94个人工标注的测试样本上，这套法官系统达到了82.1的平衡F1分（一种衡量准确率和召回率综合表现的指标），明显优于直接使用GPT-5.5-xhigh作为评判者的70.6分。

四、AI写证明题到底考了多少分：从本科到博士的"滑铁卢"

做好了这一切准备，正式的考试开始了。研究团队让市面上主流的顶尖AI系统挨个上场，先写证明，再评分。

在本科生组，表现最好的是GPT-5.5-xhigh，得了64.5分（满分100分）。这个成绩放在人类考场上，大约相当于勉强及格。考虑到题目全都是大学本科的数学证明题，AI系统连六成半的题目都没能写出完整正确的证明，这个结果颇能说明问题。Claude-Opus-4.8得了59分，DeepSeek-V4-Pro得了54分，其余模型得分在20到53分之间。

一旦切换到博士资格考试组，分数整体大幅跳水。GPT-5.5-xhigh降至48.9分，Claude-Opus-4.8降至40分，而Gemini-3.1-Pro-Preview更是从本科组的46.5分骤降至17.8分，几乎被拦腰截断。Kimi-K2.6从48分跌至20分，表现同样惨烈。相对稳健的是DeepSeek-V4-Pro，从本科组的54分降至博士组的40分，跌幅在这群模型中算是最小的。

这些数字意味着什么？研究团队特意把这些成绩和AI在其他数学测试上的表现进行了横向对比。在HMMT（高中数学竞赛）和USAMO（美国数学奥林匹克）这两个基准测试上，同样这批AI系统的平均得分高达87%左右，而在ProverBench上的平均得分只有45%左右，相差了整整41个百分点。换句话说，AI在高中竞赛数学上表现得如鱼得水，但在大学及博士阶段的证明题上，明显力不从心。

这种差距揭示了一个深层问题：现有的主流数学评测工具，可能因为过度聚焦于竞赛题型，而系统性地高估了AI在严格数学推理上的真实能力。

五、AI判断别人的证明：为什么"看出错误"比"不犯错误"更难

VerifierBench考察的是另一种能力：给AI看一份由别人写的数学证明，让AI判断这份证明是否正确，并说明理由，指出错在哪一步。这就像让AI当一次论文审稿人，不只是写文章，还要批改别人的文章。

研究团队采用的评判方式有两种。第一种叫做"粗略评分"，只看AI给出的最终判断——"这份证明正确"或"这份证明有误"——是否和专家意见一致。第二种叫做"元验证评分"，不仅检查最终判断，还检查AI给出的分析理由是否真正指出了正确的错误位置，以及理由是否与专家的解释在数学上高度吻合。

在粗略评分标准下，模型表现还算体面。GPT-5.5-high和GPT-5.5-xhigh都达到了76分，DeepSeek-V4-Pro达到74.1分。但一旦切换到元验证评分，分数普遍下滑。GPT-5.5-high从76分降至63.6分，GPT-5.5-xhigh降至64.9分，GLM-5.2从73.9分降至63.3分。整体而言，粗略评分和元验证评分之间的平均差距高达9分。

这意味着：AI经常能够猜到一份证明"大方向是错的"，但未必真正理解错在哪里、错的性质是什么。这就像一个学生批改作文，说"这篇文章有问题"，但说不清楚究竟哪里出了问题、为什么出了问题。表面上判断正确了，实际上并没有真正理解。

在所有模型中，最突出的问题是"无法识别伪正确证明"。许多模型的真正率（TPR，即对正确证明判为正确的比率）非常高，但假负率（TNR，即对错误证明判为错误的比率）却低得惊人。gpt-oss-120b和Intern-S2-Preview-35B的TPR都超过95，但TNR分别只有32和30.7。Claude-Opus-4.8的TPR高达93.8，TNR却只有35。简单来说，这些模型对正确的证明几乎照单全收，但对那些看起来有模有样、实则暗藏漏洞的错误证明，却缺乏足够的辨别能力。

反而是DeepSeek-V4-Pro，虽然TPR不是最高的，但它的TNR达到55.8，是所有模型中最高的，因此综合的平衡F1分最好，达到65.1。这说明，一个优秀的证明审查者，不只是要慷慨地接受正确证明，更需要谨慎地拒绝错误证明。当前AI系统的最大软肋，恰恰在于后者。

研究团队还做了一系列消融实验，系统验证了自动验证法官中每个设计环节的贡献。从最基础的Intern-S2-Preview-35B出发，加入基于结果的强化学习（Rough-RL）后，元验证平衡F1从54.9提升至59.5；进一步换成基于元验证奖励的强化学习（Meta-Ver-RL），提升至62.6；加入额外的人工标注数据后，提升至60.5；加入正样本扩充后，大幅提升至72.2；最终加入悲观验证策略，达到73.9。每一个环节都在往更准确的方向推进，而且各环节的作用相互补充、缺一不可。

归根结底，这项研究告诉我们一件很重要的事：AI在数学上的能力，并没有我们通常以为的那么全面。在那些靠刷题、靠记公式、靠熟练套路就能搞定的题型上，AI表现出色，甚至让人刮目相看。但一旦进入真正需要逻辑严密性的证明领域，尤其是研究生及以上层次的数学，AI就开始频繁露出马脚。

更耐人寻味的是，AI不只是"写不好证明"，连"判断别人的证明对不对"都不太靠谱——尤其当面对那种看起来头头是道、实则在某个关键步骤悄悄跳了逻辑的错误证明时，AI往往缺乏足够的警惕性，容易被"表面上的合理性"蒙蔽。

这对AI在科学研究中的应用有直接影响。如果我们希望未来有一天，AI能够辅助甚至独立完成数学定理的证明与验证，那么当前的这条短板就是必须正视的瓶颈。这项研究提供的评测工具和验证流程，为后续的改进方向提供了一个清晰的参照坐标。

至于这对普通人意味着什么——下次当你看到某款AI宣称自己在数学上如何厉害，不妨想想：它能在高中竞赛题上得高分，和它能在大学数学课的证明题上写出完整严密的论证，是两件性质截然不同的事情。前者考的是熟练度和记忆力，后者考的是真正的逻辑推理能力。而后者，恰恰是AI系统目前最需要继续深耕的方向。

对这项研究有兴趣的读者，可以通过论文编号arXiv:2607.11849查阅完整原文，了解更多技术细节和实验数据。

Q&A

Q1：ProverBench和普通的数学测试有什么区别？

A：ProverBench专门考察AI写数学证明的能力，而不只是算出最终答案。普通数学测试往往只看答案对不对，但ProverBench要求AI给出完整的逻辑推导过程，由专门训练的验证系统逐步审查每一个证明步骤是否严密正确，更接近真正的数学考核方式。

Q2：VerifierBench测的是什么，为什么AI在这上面也表现不好？

A：VerifierBench测的是AI能不能判断一份数学证明是否正确，并说清楚问题在哪一步。AI之所以表现不佳，主要是因为很多错误证明表面上看起来合情合理，只在某个关键步骤暗藏致命漏洞。AI往往能识别出明显的错误，但对这种"伪装成正确"的证明缺乏足够的辨别力，容易轻率地接受。

Q3：悲观验证策略是什么意思，为什么要用这种方法？

A：悲观验证是指对每份AI写的证明，让验证程序独立进行8次检查，只要有一次发现问题就判定证明不通过，必须8次全部通过才算合格。这样做是因为数学证明中的错误往往很隐蔽，单次检查可能遗漏，多次独立检查能显著降低漏判概率，使最终评定结果更加严格可靠。