AI界的"考官"终于来了：谷歌、OpenAI的顶级模型在这套考题面前纷纷露出真实水平

这项研究由两位独立研究人员完成，于2026年4月以扩展技术报告形式发布在arXiv预印本平台，编号为arXiv:2605.12524v1，分类为计算机科学·逻辑（cs.LO）。该研究是2025年EMNLP Findings会议论文《Stress-Testing the Reasoning Competence of LLMs With Formal Proofs》的扩展版本，包含大量超出会议版本的新任务、新结果、新方法和新分析。

---

说到测试人工智能的推理能力，市面上已经有了无数套"考卷"。GPT-4在高考里能考出高分，在各种逻辑测试中也表现亮眼。然而，那些看似令人印象深刻的高分背后，藏着一个令人不安的秘密：这些模型有时候给出了正确答案，却是通过错误的推理过程得到的，就像一个学生靠蒙题蒙对了选择题，但完全不理解其中的道理。

为了揭穿这种"外强中干"的假象，这项研究推出了一套全新的测试体系，名为PROOFGRID。它不是问AI"答案是什么"，而是要求AI写出完整的推理过程——就像让学生不仅交答案，还要把解题步骤一步一步写清楚，并且由一台精准无误的机器来检验每一步是否真的合乎逻辑。这套考题迫使模型展示真正的思维链条，而非仅仅猜测最终结果。

---

**一、为什么现有的AI考试形同虚设**

现有的AI推理测试存在一个根本性缺陷，那就是它们几乎只考察最终答案，而完全不管这个答案是怎么得出来的。

考虑一下数学考试的情形。当题目是"方程x?-5x+6=0的根是什么"时，答案是{2,3}。如果一个AI回答了{2,3}，我们就说它答对了。但事实上，这个AI可能是通过胡乱猜测、凑出来的，或者从训练数据里直接记住了这道题。它并不需要真正理解"二次方程根的公式"，只需要背住这道题的答案就行。

这个问题在数学奥赛题目上尤为突出。有研究者对2009年到2023年的455道精选国际数学奥林匹克赛题做了系统分析，结果发现令人震惊：在最终答案正确的情况下，推理过程真正完全正确的概率，在o1模型上只有12.5%，在o3-mini上是14.3%，而在o1-mini、DeepSeek R1和Gemini 2.0上，这个数字是——0%。换句话说，这些模型的正确答案几乎全是"蒙"出来或者"记"出来的，推理过程要么是错的，要么是表面合理但骨子里自相矛盾的。

更广泛的测试也暴露了类似问题。在被视为权威的数学基准测试MATH 500上，GPT-4.1的得分是87.6%，DeepSeek 3.1是91.5%，Gemini 2.5 Pro是91%。三个模型的差距只有3.9分，头两名之间只差0.5分——这说明这个考卷已经快失去区分能力了，不同水平的模型都能考出差不多的高分。

PROOFGRID在同一道测试题（PL1-PW任务）上给出的分数则截然不同：GPT-4.1只有35%，DeepSeek 3.1是49%，而Gemini 2.5 Pro高达94%。第一名和最后一名之间差了整整59分，前两名之间也差了45分。这种清晰的差距才真正说明了不同模型之间真实能力的分层。

---

**二、证明你会推理，而不只是给出答案**

PROOFGRID的核心思想其实相当简单：要求AI用一种专门设计的、极其精简的逻辑语言来书写完整的证明过程。

这种语言叫做NDL（Natural Deduction Language，自然演绎语言）。NDL刻意设计得非常简单，任何人只需读几页说明就能学会。它的基本规则就像搭积木一样：每一步推理都必须明确指出你依据了哪个规则、使用了哪些已知条件，并且你得出的结论必须严格符合那个规则的要求。这样，一台程序就可以像裁判一样，逐步检查每一步推理是否合法，最终判定整个证明是否成立。

举个具体的例子。假如题目是：已知"A成立"和"A成立则B成立"，请证明"B成立"。一个完整的NDL证明需要这样写：

第一步，引用规则"modus ponens"（假言推理），将"A"和"A=>B"作为输入，得出"B"。

这个过程就像厨师不仅要端出一道菜，还要把每一步的食谱都写清楚——用了什么食材，经过了哪道工序，最后为什么会得出这道菜。读者（或者说机器检查器）可以逐步验证每一个步骤是否合理。

正因为这种精确性，PROOFGRID的评分标准是纯粹机械的、可重复的、完全客观的。不需要人工判卷，不需要"AI评AI"的循环评判，只需要一段确定性程序就能得出结论。

---

**三、考题的设计：从基础热身到顶级挑战**

PROOFGRID共包含15个任务，分布在几个不同的模块中，难度层层递进。就像一场马拉松比赛，前几公里是热身，中段是考验耐力，最后几公里才是真正的生死关头。

最基础的模块叫做PL1（第一级命题逻辑）。这一层的题目涉及的逻辑变量较少（中位数只有3个），公式结构相对简单。即便如此，PL1也不简单——它包含四种不同类型的任务。

第一种是"证明写作"（Proof Writing），要求模型从零开始写出一段完整的证明，证明某个逻辑结论确实可以从给定的前提推导出来。第二种是"证明检查"（Proof Checking），给模型一段已经写好的证明，让它判断这段证明是否正确，如果有错，要指出第一个出错的地方。第三种是"证明掩蔽"（Proof Masking），把一段完整的正确证明里的某些关键词遮住，换成占位符（MASK1、MASK2……），让模型猜出被遮住的内容。第四种是"证明补洞"（Proof Gap-Filling），把证明的某些整段删去，换成"GAP-1"、"GAP-2"这样的标记，让模型把缺失的推理步骤补全。

更高级的模块PL2包含复杂度更高的逻辑推理，使用了一种基于电路诊断的问题框架：给定一个逻辑电路的工作原理，以及某个输出出错的观察，要求证明哪些部件可能出现了故障。这类问题本质上是一种"溯因推理"——从结果反推原因——具有相当的实际意义。

PL3则更进一步，涉及八个不同的经典难题家族，包括图着色问题、鸽巢原理、Tseitin公式（一种源自可满足性理论的难题家族）、子集基数问题、De Bruijn公式、DAG铺石子问题等。这些问题之所以困难，不是因为题目本身很长，而是因为它们需要全局性的组合推理——你必须从众多前提中挑选出正确的那些，将它们巧妙地串联起来，才能推出结论。而且这些前提里往往夹杂着一些"无用"前提作为干扰，考验模型筛选有效信息的能力。

还有一个模块PL4，专门测试在一种叫做"希尔伯特演算系统"的极简逻辑框架下写证明。这个系统只允许三条公理和一条推理规则，却要用它推出所有命题逻辑定理。就好像只给你一把锤子和三种固定动作，要求你建出一座大楼——难度可想而知。

最后还有一个等式推理模块（Equational Logic），完全不使用任何形式语言，直接用"s = t by E1, E2"这样的等式推导链来测试模型的代数推理能力。

---

**四、一个宽容的裁判，却依然公平**

在实际测试中，研究者发现了一个有趣的现象：许多模型其实已经"想通了"某道题，但在把思路转化为标准格式时，会犯一些无关紧要的小错误。

比如，一个常见的错误是把"left-and"规则和"right-and"规则搞混——这两个规则都是从"A并且B"这样的合取命题中提取一个成分的，区别只是提左边的A还是右边的B。模型在推理层面完全正确，它知道要提取什么，但在执行层面搞反了方向。

如果用严格的评分标准，这步推理被判为错误，整个证明失败。但从逻辑洞察的角度来看，模型其实已经掌握了核心思路。

为了区分"真正的推理错误"和"执行层面的小失误"，研究者开发了一套"有容乃大"的检查工具——"仪器化证明检查器"（Instrumented Proof Checker）。这个工具会自动修复一系列常见的表面错误：括号不匹配会被修复，多余或缺少的分号会被修复，左右规则混淆会被忽略，双重否定（"A"和"非非A"被视为等价）会被自动处理……但对于真正的逻辑错误——比如用了一个前提条件但那个条件根本不在当前假设库里——则一律严格判错。

这个设计带来了巨大的分析价值。通过对比"严格分数"和"仪器化分数"，研究者能够精确量化每个模型"推理想法正确但执行失误"的比例。

结果相当有趣：DeepSeek R1-0528在评估PL1-PW的400个证明过程中，被仪器化检查器发现并修复的错误超过2500次，平均每个证明有近7次错误，但其中绝大多数是语法层面的小问题，修复后的准确率提升超过了39个百分点。而顶级模型Gemini 3.1 Pro Preview在同一任务上几乎不需要修复——只有极少数的小错误。

这种对比揭示了模型能力的一个重要维度：有些模型"会想但不会写"，有些模型则"既会想又会写"。

---

**五、24个顶级AI同台竞技，排名出乎意料**

研究团队测试了从2024年底到2026年初发布的24个主流AI模型，涵盖OpenAI、Google、Anthropic、DeepSeek、xAI等几乎所有主要厂商的产品，包括GPT-4o、GPT-4.1、GPT-5、GPT-5.1、GPT-5.2、o3、o3-mini、o4-mini、Gemini 2.5 Pro、Gemini 3 Pro Preview、Gemini 3.1 Pro Preview、Claude Sonnet 4、Claude Opus 4、Claude Opus 4.5（含扩展思考版本）、DeepSeek V3、DeepSeek V3.1、DeepSeek R1、DeepSeek Reasoner、Grok-3、Grok-4、Mistral Magistral、LLaMA 3.1 405B、Hermes-4等。

最引人注目的发现是关于o4-mini的。这个模型曾被OpenAI宣传为在2025年AIME数学竞赛中达到99.5%的通过率，在FrontierMath竞赛子集上甚至超过了人类顶级数学家团队的平均水平（约22% vs 约19%）。然而在PROOFGRID上，o4-mini的表现却让人大跌眼镜——它在24个模型中长期排在后半段，在PL3-PW（第三级命题逻辑的证明写作）任务中只有6%的准确率，而同为OpenAI模型的o3则达到了22%，相差三倍还多。

这种反差指向一个值得深思的结论：那些让模型在传统数学题目上取得高分的能力——大量记忆数学知识、运用特定解题技巧——在面对纯粹的抽象逻辑推理时并不管用。PROOFGRID通过消除所有领域知识依赖，让模型没有捷径可以走，只能靠真正的逻辑推理能力来应对。

在整体表现上，Gemini 3.1 Pro Preview在大多数任务中遥遥领先，特别是在PL2-PW（仪器化准确率高达94%）、PL3-PW（仪器化准确率72%）以及希尔伯特证明写作（PL4-PW，仪器化准确率71%）等任务上。GPT-5.2和GPT-5.1紧随其后，但在难度最高的任务上与Gemini 3.1的差距显著。Claude Opus 4.5在证明检查类任务上表现突出，证明不同任务确实测试了不同维度的能力。

最难的那些任务——子集基数问题、Tseitin公式问题、希尔伯特演算证明写作的挑战版——目前没有任何模型能够可靠解决，准确率普遍低于10%甚至接近0%。这些任务将成为未来若干年内的重要参照点。

---

**六、一个诡异的现象：模型"清醒地犯错"**

在PL3-PW任务的分析中，研究者发现了一个令人困惑的现象，他们称之为"认知不稳定性"（Epistemic Instability）。

具体来说：模型在写证明的过程中，有时会写下一步根本不正确的推理——例如，它写"A15由(A16|A15)推出"，声称"A15"可以从"A16或A15"这个析取命题直接得出。但这在逻辑上是完全错误的：一个析取命题只告诉我们两者之一成立，而不是两者都成立。

当研究者事后把这个步骤单独拿出来，问模型"A15能从(A16|A15)推出吗"，模型会立刻正确地回答"不能"，并给出清晰的反例——"如果A16为真而A15为假，那么(A16|A15)仍然成立，但A15不成立"。

换句话说，当模型被单独问这个简单问题时，它完全知道正确答案。但在写证明的过程中，它却犯了这个它明明知道是错误的错误。

这就像一个学生，当你问他"1+1等于多少"，他会说"2"；但当他在做一道大题目的过程中，需要用到"1+1=2"这个步骤时，他可能会写"1+1=3"——然后继续做下去，毫不察觉。

为了量化这种认知不稳定程度，研究者对九个顶级模型进行了系统测试：从每个模型写错的证明中抽取一步逻辑错误，单独问模型这步推理是否成立。结果是：所有九个模型，100%的概率正确识别出了这些步骤确实是错误的，而且平均把这些错误的困难程度评为1.15到1.74分（满分5分）——也就是说，模型认为这些错误"极其简单"。

这个发现引出了一个深刻的问题：为什么模型在写证明时会犯它们在独立测试中能轻松识别的简单错误？研究者的解释是：模型的推理能力不是模块化的。在全局性的、高认知负载的任务（如写一段长证明）中，模型需要同时追踪假设库的状态、当前的推理目标、已使用的规则……这种全局信息处理会对局部的精确性产生干扰，导致本来知道的规则被"遗忘"或"用错"。

---

**七、量化模型的"认知不稳定指数"**

为了给这种不稳定现象提供一个精确的度量，研究者设计了"认知稳定指数"（Epistemic Stability Index，ESI），取值范围在0到1之间，越高表示模型的行为越一致、越理性。

ESI的计算逻辑是这样的：首先收集模型在写证明时做出的所有推理判断，然后独立地问模型每一步"这个推理是否正确"，看两次判断是否一致。如果模型写证明时接受了某步推理，但被单独问到时却拒绝了它（或反之），就计入"不一致"。最终用不一致的比例来计算ESI的扣分。

计算结果揭示了令人担忧的真相：Gemini 2.5 Pro和GPT-5的ESI都只有0.27，意味着它们约73%的证明与它们自己的独立判断相矛盾；GPT-5.1是0.38；Gemini 3 Pro Preview是0.41；Claude Opus 4.5是0.48；Grok-4是0.52；o3是0.53；Gemini 3.1 Pro Preview相对最好，也只有0.61；GPT-5.2是0.62。

这意味着即使是当前最强大的模型，在写出一段证明后，这段证明仍有将近40%的概率与它自己对相关推理步骤的独立判断相矛盾。模型在不同的认知语境下有不同的"信念"，这是一种深层次的理性缺陷。

---

**八、题目辨别力：一把精准的尺子**

PROOFGRID还引入了一套专门衡量"测试题辨别能力"的指标体系，避免了"考卷太简单大家都考满分"或"考卷太难大家都接近零分"的极端情况。

最基础的指标叫做DI（可辨别指数，Discriminability Index），计算方法是：对所有模型两两组合，计算它们分数的差的绝对值，然求平均。DI=0意味着所有模型得分完全一样，测试毫无意义；DI越高，说明测试越能分辨出不同模型的真实水平差异。

在PROOFGRID的各任务中，PL1-PC的DI约为0.27，PL3-PC高达0.42，PL3-PW的DI为0.23，PL1-GF为0.375，PL2-PW的DI达0.30。相比之下，许多主流基准测试的有效DI已经接近0.05或更低，基本失去了区分能力。

研究者还引入了更严格的"标准化辨别分"，基于项目反应理论（IRT）中的费舍尔信息量来计算。这个指标不仅考虑整体分布，还能精确回答"对于某一特定能力区间的模型，这道题的辨别力有多强"这样的精细化问题。比如，PL3-PC对中等能力模型的标准化辨别分高达0.93，说明这个任务对于区分中等水平模型极为有效；而PL4-PW则对高端模型更有辨别力，标准化辨别分达0.70。

---

**九、置信度校准：模型知道自己什么时候不确定吗**

在等式推理的补洞任务中，研究者还测试了模型的置信度校准——模型能不能准确判断自己答对了还是答错了。

每个模型在给出答案的同时，需要给出一个1到5的置信度分数（1=完全不确定，5=非常确定）。通过比较置信度预测和实际答题正确率，研究者发现了普遍的过度自信现象。

最差的情况是：Mistral Magistral、LLaMA 3.1 405B、Grok-3等模型的整体预期校准误差（ECE）超过0.6，有些甚至接近0.8——这意味着当模型声称"我非常确定（置信度5）"时，它实际上错误的概率可能高达80%。以赌博来类比：如果你相信这个模型的高置信度表态，并以19:1的赔率押注它是正确的，实际上你平均每次决策会损失5美元。

相对来说，GPT-5.2的整体ECE只有0.12，Gemini 3.1 Pro Preview是0.12，Claude Opus 4.5是0.13——这三个模型的置信度具有一定的参考价值，但即便如此，在高置信度区间（置信度4和5）的校准误差仍然相当大，不能完全信任。

这项发现的实际意义在于：如果你想用置信度阈值来过滤AI输出（比如"只相信置信度超过4的答案"），对于大多数模型而言这是不安全的，因为恰恰在高置信度时模型最容易犯错。

---

**十、项目反应理论：给每道题每个模型精准画像**

研究者还引入了心理测量学领域经典的"项目反应理论"（IRT）来对测试结果进行更精细的分析。IRT原本是用来分析学生考试成绩的统计模型，现在被用于分析AI的测试表现。

IRT最直观的工具是"莱特地图"（Wright Map）——把每道题目的"难度"和每个模型的"能力"放在同一个坐标轴上。通过观察模型和题目在坐标轴上的相对位置，可以判断"哪些题目对哪类模型最有区分意义"。

以PL1-PM（PL1级别的证明掩蔽任务）的莱特地图为例：题目在能力轴上的分布相当均匀，从最简单的（对应GPT-4o水平的模型恰好有50%概率做对）到最难的（对应Gemini 3.1这种顶级模型也有一定挑战性），形成了一个覆盖全能力区间的完整谱系。这说明PL1-PM是一道非常"平衡"的测试任务，对所有能力层级的模型都有区分意义。

相比之下，PL4-PW（希尔伯特演算证明写作）的任务信息曲线向右偏移明显，说明这道题对低水平和中等水平模型几乎没有区分价值（它们全都接近零分），只对顶级模型才有意义。其标准化辨别分在能力区间（0.5,3.2）上达到0.70，而在低能力区间基本为零。

---

**十一、还有很多没被彻底攻克的高难度题**

值得特别指出的是，PROOFGRID中有相当一部分任务至今没有模型能够可靠地解决，这些任务将成为未来若干年内的重要标杆。

子集基数问题和Tseitin公式问题，所有24个模型的准确率基本在5%以下甚至接近0%。这两类问题的共同特点是：不一致性来自全局性的数量约束（前者是整数计数约束，后者是模2奇偶性约束），但这些约束被编码成了无数分散的小型逻辑公式，每个公式看起来都无害，只有把它们全部综合起来才能看出矛盾。这恰好暴露了当前AI模型的一个深层缺陷：擅长局部推理，拙于全局聚合。

希尔伯特演算证明写作的挑战版（PL4-PW-c）更是极端：在50道测试题中，Gemini 3.1只解决了6道（12%），GPT-5.2解决了3道（6%），其他所有模型均为0。

较长的PL1证明检查挑战版（PL1-PC-c）同样困难重重：50个证明，每个有700-980行，Claude Opus 4.5只达到69%的纯猜测准确率（等于仅比抛硬币好38%），而所有四个测试模型均低于"始终猜对"这一82%的多数派基准，说明模型无法从长证明中可靠地提取正确的结构信息。

较长的PL1证明补洞挑战版（PL1-PM-c，每个证明数百行）也一样：GPT-5.4仪器化准确率38%，GPT-5.2是32%，Gemini 3.1是34%，Claude Opus 4.5只有6%。

---

**结尾**

归根结底，这项研究做了一件很有价值的事：它给AI推理能力的测试竖起了一面真正的镜子。

之前的那些考卷，很多时候测试的不是推理能力，而是记忆能力、模式匹配能力、或者更坏的情况——蒙题能力。PROOFGRID通过要求模型写出完整的、可机器验证的证明链，把"答案正确"和"推理正确"区分开来，给AI的真实推理水平提供了一个更诚实的快照。

这项研究也带来了一个令人振奋的消息：当前最强的几个AI模型在相当难度的抽象逻辑推理任务上确实展现出了真实的推理能力，而不只是在记忆和模式匹配。这说明推理能力的发展是真实发生的，而不是数字游戏。

但同时，它也清晰地揭示了当前模型的局限：全局性组合推理仍然困难，执行精度仍然不稳定，认知自洽性仍然存在显著缺陷。这些不是表面上能被更好的提示语或更多的训练数据轻易修复的问题——它们指向了AI架构本身需要解决的深层挑战。

对任何关心AI真实能力的人来说，这项研究提供了一个难得的清醒视角。如果你想深入了解细节，可以在arXiv上通过编号arXiv:2605.12524查阅完整的论文原文。

---

Q&A

Q1：PROOFGRID和传统AI推理基准测试有什么本质区别？

A：传统基准测试（如MATH、MMLU）只检验最终答案是否正确，PROOFGRID则要求模型写出可被程序逐步核验的完整逻辑证明链。这意味着模型无法靠背答案或猜测得分，必须展示真实的推理过程。就像考试时要求写出解题步骤，而不是只交选项。

Q2：o4-mini在AIME竞赛中接近满分，为什么在PROOFGRID上表现却排在后半段？

A：AIME这类竞赛题目涉及大量数学知识和已知技巧，训练数据中有丰富的类似题目，模型可以通过记忆解题模板来应对。PROOFGRID的题目是纯粹的抽象符号逻辑，没有任何可以借助的领域知识，必须依赖真正的逻辑推导能力。两种能力是不同的维度，互相不能替代。

Q3：PROOFGRID中说的"认知不稳定性"是什么意思，对实际使用AI有什么影响？

A：认知不稳定性指的是同一个模型，在完整推理过程中接受了某步逻辑，但当被单独问"这步逻辑是否正确"时，又会否认它。这说明模型在复杂任务中的判断和在简单问题中的判断不一致。实际影响是：你不能完全信任AI在复杂推理过程中的每一步输出，它可能"清醒地犯错"——不是因为不知道规则，而是因为在全局压力下"忘记"了它知道的规则。