数学AI考卷发下来了，及格线是多少？

让AI证明数学定理，现在流行考它做奥数题。国际数学奥林匹克竞赛的题目，Putnam数学竞赛的题目，这些成了检验AI证明能力的标准考卷。

但这里有个问题很少有人问出口：世界上真正需要证明的数学命题，有多少是奥数题？

答案是几乎没有。真正的数学工作者，无论是研究概率论的教授，还是做机器学习理论分析的工程师，他们日常打交道的是马尔可夫链的收敛性、鞅的停时定理、布朗运动的路径性质。这些内容在任何一本竞赛题集里都找不到。用奥数题给AI的数学能力打分，有点像用短跑成绩去评价一个马拉松运动员，成绩好看,但根本不是同一项运动。

凯斯西储大学的研究团队看到了这个错位，做了一件事：造一套真正来自研究生随机过程课程的考题，450道，全部用Lean 4这种可以被计算机逐行核验的形式化语言写出来。这套考卷叫STOCHBENCH。

**Lean**：一种交互式定理证明器和编程语言，写在里面的数学证明可以被计算机自动检查每一步逻辑是否严密，不存在人工审稿时可能出现的疏漏。

出题人知道答案不够

现有的形式化数学题库大多长这样：MiniF2F收集了奥赛题，ProofNet对接本科生教材，PutnamBench专攻大学生数学竞赛。这些题库的一个共同点是，题目本身足够刁钻,足够能体现证明技巧,但离真实的应用数学有相当距离。

随机过程恰好是被冷落得最严重的一块。Mathlib是Lean语言配套的数学库,相当于一个巨大的公共代码仓库,里面存放着社区共同验证过的数学定义和定理。

**Mathlib**：Lean语言的开源数学定理库，收录了大量已经被形式化证明的数学结果，供后续证明复用。

翻开Mathlib的随机过程部分，你会发现存量的确在增长,布朗运动被形式化了,鞅收敛定理被证明了,但覆盖面依然稀疏,大片的马尔可夫链理论、更新过程、排队论,基础设施都是空的。这就好比你要装修一套房子,水电基本管道已经预埋好,但很多房间连墙都没砌。研究团队意识到,如果继续等Mathlib补全所有基础设施再出题,可能要再等好几年。

所以他们换了个思路：不等地基全部建好，先把题目立出来。有基础设施支持的，就直接用Mathlib里现成的定义写成题目，这类题目叫做"直接型"。基础设施还没跟上的，就把证明需要用到的关键性质当作已知条件先给出来，让证明者在这个假设下完成剩余的推理，这类题目叫"抽象型"。

举个具体例子。假如题目要证明"最优停时定理"，也就是鞅在随机停止时刻的期望值等于初始时刻的期望值。如果Mathlib里已经有完整的鞅定义和停时定义，这道题就可以直接引用，写成直接型。但如果某个概念比如某种特定的收敛性质，Mathlib里还没有对应的形式化定义，研究团队就把这个性质写成一条假设放进题目条件里，让证明者从这条假设出发去推导结论，而不需要重新造轮子去证明这个性质本身成立。

这种做法有点像盖房子时先用脚手架撑住还没浇筑的部分。你没法等每一根承重柱都浇筑完成才开始搭建上层结构，脚手架先把位置占住，让整体框架先立起来，后续再逐步把脚手架换成真正的承重构件。如果STOCHBENCH坚持只出直接型题目，那这套题库现在可能只有几十道题，覆盖面窄得可怜，根本没法反映随机过程这门学科真正的知识密度。

最终，450道题里有114道是直接型，占25.3%，剩下336道是抽象型，占74.7%。这个比例本身就说明了一件事：随机过程这门学科在Lean里的基础设施还差得远，但数学问题不会等基础设施建好才存在。

八张考卷，覆盖研究生随机过程的骨架

题目从哪来？研究团队没有闭门造车，一部分题目是团队自己原创设计的，更大一部分来自真实的教材和课堂讲义，包括《概率论、数理统计与随机过程》这本教材，以及麻省理工学院三门随机过程相关课程的讲义和作业，涵盖入门课、进阶课和离散随机过程专题课。

选题时团队特意划了一条线：如果一道题本质上是在考概率论的基本性质，比如证明总变差距离满足三角不等式，这种更接近纯概率论基础，不算随机过程的特色内容，直接排除。留下来的题目必须真正体现随机过程这门学科的核心关切。

最终题库覆盖八个主题。离散状态的马尔可夫链，包括有限和可数状态两种情形，出题96道，是数量最多的一类。鞅论与停时理论紧随其后，94道。更新过程41道，随机游走与大偏差62道，布朗运动与随机微积分45道，泊松过程40道，连续时间马尔可夫链与排队论55道，弱收敛与泛函极限17道。

这八块拼起来，基本就是一份完整的研究生随机过程教学大纲。这不是巧合，是团队有意为之的结果。

为了让不同题目之间能够互相调用共同的数学语言，团队还专门构建了一套共享定义库。比如有限状态链会用统一的矩阵形式表达随机性、平稳性、不可约性、非周期性、转移矩阵幂的最终正性、细致平衡、时间可逆性和总变差距离。像"击中时间"这种概念，团队定义了通过一步转移方程刻画的辅助工具，让多道涉及首达时间的题目可以复用同一套记号，而不是每道题各写各的定义，造成概念上的割裂。

这里有一个细节值得展开讲讲。随机过程有个容易被忽略的区分：一个过程在某个时刻的分布，和这个过程在多个时刻上的联合行为，是两回事。前者叫边际分布，后者叫联合过程律。题库里专门区分了这两种表达方式，一种叫HasMatrixMarginals，描述某时刻的分布对应转移矩阵幂的某一行；另一种叫HasChainLaw，直接给出整条路径上多个时刻同时取某些值的联合概率公式。为什么要费这个劲区分？因为有些证明只需要知道某一时刻的分布就够了，有些证明必须掌握整条路径的联合信息才能往下推，比如证明两条马尔可夫链的耦合上界，就必须同时用到边际分布和"相遇之后保持一致"这个路径级条件。如果题库不做这个区分，很多题目要么信息给多了变得平庸，要么信息给少了根本无法证明。

考官换成了AI，AI考了多少分

题目出好了，谁来做题？研究团队用了一个基于Claude Opus 4.8的智能体，配合Lean语言的错误反馈机制和检索工具，让它自主尝试证明每一道题。

**Opus 4.8**：Anthropic公司开发的大语言模型版本，本文用作自动定理证明的智能体核心引擎。

规则很简单，每道题给15分钟，智能体可以反复查看Lean报错信息、检索库函数、修改证明策略，直到时间用完或者证明通过为止。这个设定本身就是一种压力测试：真实做研究时，数学家可能会花一整个下午甚至几天啃一道难题，但15分钟的硬性限制逼着AI必须快速判断哪些策略值得尝试，哪些该放弃。

结果是157道题被干净地证明出来，成功率34.9%。这里"干净"有个明确标准：证明里不能有sorry占位符,不能用sorryAx这种绕过完整证明的手段，也不能引入额外的、未经证明的假设。Lean的编译器会逐字核验，容不得半点含糊。

**sorry**：Lean语言中的占位符关键字，用来标记暂未完成的证明步骤，让代码能先通过编译，但不算真正完成证明。

分主题看，成绩差异很大。鞅与停时这块表现最好，61.7%的通过率；连续时间马尔可夫链与排队论41.8%；马尔可夫链38.5%；弱收敛35.3%；随机游走25.8%；泊松过程17.5%；布朗运动与随机微积分17.8%；更新过程垫底，只有4.9%。

这个分布不是随机波动，背后有清晰的原因。鞅论恰好是Mathlib里基础设施最完善的领域之一，前面提到的Ying和Degenne在2022年就把Doob鞅收敛定理形式化了，停时和条件期望的工具链相对成熟。相比之下，更新过程几乎没有专门的Mathlib支持，41道题清一色是抽象型，AI要在几乎从零搭建的地基上完成证明，难度自然陡增。

直接型和抽象型题目的表现差距也很惊人。直接型题目的通过率是69.3%，抽象型只有23.2%，差了整整46个百分点。这说明什么？说明当基础设施齐全、AI可以直接调用现成定理拼接证明时，它做得相当不错；但一旦需要从一堆假设条件出发，自己搭建证明的中间步骤，独立发展出新的引理，成功率就断崖式下跌。这个对比其实提醒我们，现在的AI证明器更擅长"检索式"证明，把已有的积木搭起来，而不是真正意义上的"发现式"证明，从零构造出前人没写过的中间结果。

论文附录里给了一个特别能说明问题的案例，编号Q361，考的是马尔可夫链击中时间的一个经典不等式：最坏情况下的期望击中时间，不超过平稳分布下期望击中时间最大值的两倍。这道题的形式化只给了击中时间满足的首步方程，没有给凯梅尼常数定理，也没有给击中时间的三角不等式，这两个中间结果都需要AI自己发现并证明。

AI在这道题上花了超过30分钟（超出15分钟基线的独立测试），最终交出的证明包含九条辅助定理，从矩阵幂的非负性开始，逐步证明极大值原理的传播引理，再用返回时间恒等式推出凯梅尼函数的调和性，靠不可约性和极大值原理证明这个函数在整条链上是常数，同一套传播引理又被复用去证明击中时间的三角不等式，最后用平稳分布加权平均把这些结果拼成最终的不等式。这个过程很像盖房子时先浇筑几根关键承重柱，再一层层往上搭楼板，如果没有这九条辅助定理打底，直接冲最终结论，几乎不可能成功。这道题也从侧面说明了一件事：抽象型题目不是把证明变简单了，而是把证明的自由度和难度都交还给了证明者，AI必须自己判断该往哪个方向搭脚手架。

质检报告：哪里还在漏水

研究团队没有回避问题。他们做了定性检查，发现失败案例大致分两类。一类是纯粹的证明搜索失败，题目本身合理，但AI没找到正确的引理组合，或者卡在难啃的库接口上，找不到调用路径。另一类更值得警惕，是形式化本身存在瑕疵，比如漏掉了可测性假设、可积性条件，或者非空性前提。这类问题不是AI证明能力不够，而是题目本身在翻译成Lean语言的过程中出了纰漏。

为了应对这个风险，团队设计了一个补救机制：如果AI没能证出题目本身，但反过来证明了这道题在当前的形式化下是错误的，也算通过。这相当于给了一条应急通道，万一题目翻译错了，编译器至少能捕捉到这个矛盾，而不是让证明者在一个根本不成立的命题上无限空转。

题库和主题的分类目前都是人工判定的，团队在论文里坦诚承认这一点，直接型和抽象型这样的术语，边界在什么地方，团队内部也没有给出严格的量化定义。这算不算一种局限？确实是，但换个角度看，任何一个新领域的基准测试在早期阶段都很难做到边界完全清晰，先把框架搭起来，让更多人参与进来打磨细节，可能比闭门造出一套自认为完美的标准更实际。

这份题库的价值，可能不只在打分

STOCHBENCH最终的产出不只是一份成绩单。团队同时公开了450道题目对应的自然语言原文和Lean形式化版本的配对数据，还有共享定义库和智能体证明尝试的完整记录。

这个配对数据本身有额外的用途，可以用来训练"自动形式化"模型,也就是让AI学习把自然语言写的数学命题自动翻译成Lean代码的能力。而那些已经通过编译核验的证明，可以反过来当作监督信号，训练下一代证明生成模型。

某种程度上，STOCHBENCH做的事情有点像给一门被忽视的学科重新画一张地图。奥数题库测的是解题技巧的极限，而STOCHBENCH测的是AI能不能真正读懂、真正复现一个学科日常运转所依赖的那些推理链条。这两件事看起来都是"让AI证明数学定理"，但它们对应的能力其实相当不同。

写在后面

读这篇论文时，最让我停下来想的不是那157道被证出来的题，而是那46个百分点的差距,直接型69.3%对抽象型23.2%。这个数字差距比整体34.9%的通过率本身更有信息量，它揭示出当前AI证明器的一个结构性弱点：擅长在已铺好的轨道上快跑，一旦轨道断了要自己接，速度立刻掉下来。

另一个让我意外的细节是更新过程那4.9%的通过率。41道题里只证出2道。这不是AI偷懒，而是这个领域在Mathlib里几乎是一片空地，AI每次证明都得从最基础的地方开始搭建，做题变成了半个搭基建的活。这提醒我一件容易被忽略的事：AI证明能力的进步，某种程度上被形式化数学基础设施的完善程度死死拴住了。不是模型不够聪明，是它手边缺工具。

Q361那道击中时间不等式的证明过程也让我反复看了好几遍。九条辅助定理，层层递进，最后拼出一个结论。这种证明结构和人类数学家真正做研究时的思路其实很像,先摸索几个局部性质，确认它们成立，再把它们组装成大结论。这和刷题式的"套公式"完全是两种脑力活动。如果未来的AI证明器能在抽象型题目上把23.2%这个数字往上推，可能意味着它开始具备某种真正的数学发现能力，而不只是熟练的检索匹配能力。

Q&A

Q1：STOCHBENCH是什么？

A：STOCHBENCH是凯斯西储大学团队推出的Lean 4形式化数学基准测试，包含450道来自研究生随机过程课程的定理证明题，覆盖马尔可夫链、鞅论、布朗运动等八个主题。

Q2：STOCHBENCH和奥数题库比如MiniF2F有什么不同？

A：MiniF2F、PutnamBench这类基准测试题目都来自数学竞赛，STOCHBENCH的题目全部来自真实的研究生教材和课程讲义，更贴近应用数学的实际推理需求，而不是竞赛技巧。

Q3：AI在STOCHBENCH上表现如何？

A：基于Claude Opus 4.8的证明智能体在15分钟单题时限下，450道题里证出157道，通过率34.9%。其中直接引用现成数学库的题目通过率69.3%，需要自己搭建中间证明的抽象型题目只有23.2%。