灯照不出山的高度：大模型数学能力的测量与信任

Mathematics Is All We Want — A Lighthouse Survey

李昂

v2.1 灯塔综述 · 2026 年 10 月 18 日

摘要

先看四个数字。MATH-500 上，头部模型的准确率已超过百分之九十。FrontierMath 发布时，最强系统解出的题目不足百分之二；而到 2026 年 9 月，GPT-6 Astra 已将其第四档（Tier 4）推至百分之九十七点六，宣告该基准实质性饱和。AMO-Bench 收录五十道原创 IMO 级题目，二十六个参评模型的最佳成绩为 52.4%。MATH-Beyond 则用同一难度带内的题目，构造出一个“基座模型在 pass@1024 下依然无解”的集合——它提醒我们，连“大 $k$ 饱和”本身，都可能只是基准选择的产物。

同一年份，同一个词——数学——四个数字。它们并不矛盾；它们只是没有在说同一件事。

还有第五个数字，不在任何基准上。2026 年 10 月，OpenAI 一次性释放 722 篇由前沿模型生成的数学手稿，覆盖 17 个领域；次日，却因一处“+1 与 -1”的符号错误撤回其中 3 篇涉及霍奇猜想的关联手稿。[72] 几乎同一周，DeepMind 的 AlphaProof Nexus 在《Science》上发表：仅凭“大模型 + Lean 编译器反馈”的极简架构，解出悬置 56 年的 Erdős 问题。[73] 一边是算力堆砌引发的“证明消化不良”与 27 位菲尔兹奖得主的联名抗议，[75] 一边是形式验证器作为“黄金外骨骼”的冷酷有效。同一个十月，两种未来。

这篇综述要回答的，不是“大模型会不会数学”，而是一个更在先的问题：当我们说“会”的时候，我们究竟在说什么。Mathematics is all we want——我们想榨干大模型的数学能力；但“榨干”的前提是知道哪里还有油。我们的回答是：数学能力不是一座孤峰，而是一片具有五个高度的山脉——数感、符号算术、关系推理、演绎证明、数学创造；而每一次关于“进步”的宣称，都必须先回答另一个问题：它是让模型会得更多，还是让我们更容易找到模型已经会的东西？

我们将后者拆分为三个可分别测量的量：覆盖度（世界上是否存在一条正确的路）、可靠度（闭着眼走，走对的概率）、可达度（给我 $k$ 次机会，能否走到）。两个命题把三者的关系钉死：有限次数的 pass@ $k$ 只看得见每题成功率分布的前 $k$ 阶矩，看不见机制；只增加采样的工程，最终必然在覆盖度处熄火。而 2026 年秋天的风暴证明，这把尺子不仅能量论文，也能量一个时代的野心与失度。

数学是试金石，也是基础设施。我们想要的不是更高的分数，而是知道分数从哪里来——以及，在机器的算力海啸面前，人类的理解力将站在哪里。

1. 引子：从基准饱和到信任危机

先看四个数字。

MATH-500，一个被反复引用的高中竞赛题集，头部模型的准确率已在百分之九十以上。[1] FrontierMath，一个由数学家出题、面向研究级数学的基准，发布时最强系统解出的题目不足百分之二；[2] 而 2026 年 9 月，GPT-6 Astra 报告其第四档（Tier 4）达到 97.6%——这个曾被预估“还有多年余量”的基准，已被实质性刷穿。[74] AMO-Bench，五十道原创 IMO 级题目，最佳成绩 52.4%。[4] 最后一个数字来自 MATH-Beyond：作者从常见训练集中挑出一个子集，使参数量不超过 80 亿的基座模型即使在 pass@1024 下也无法解出，从而把“RL 能否真正扩界”变成一个可测量的问题。[5]

四个数字放在一起，指向一个不那么舒服的结论：“数学能力”不是一个标量，而是一族随任务分布、验证器与采样预算而变化的量。

三个变化让这张地图变得必要；2026 年秋季，它们演变为一场公开的行业冲突。

第一，基准正在饱和，而饱和不是终点。GPT-6 Astra 在 FrontierMath Tier 4 上的 97.6% 宣告：传统的“找更难的题”路线已走到尽头。当基准的头部分数逼近上限，它便不再区分“会”与“不会”，只能区分“稳”与“不稳”。研究者的回应是两条新路：反向构造（MATH-Beyond：构造基座在极大采样下也解不出的集合），与未发表难题盲测（First Proof：用数学家已解决但尚未发表的问题做评测，从根上杜绝污染）。[5][78]

第二，工程层正在变厚，并已引发“证明消化不良”。今天的“模型分数”早已不是模型单独的分数。10 月初，OpenAI 动用上万个智能体在 88 小时内生成纳维–斯托克斯方程手稿，随后发布 722 篇涵盖 17 个领域的手稿，却因一处符号错误撤回 3 篇。[72] 陶哲轩将这一状态命名为**“证明消化不良”**（proof indigestion）：AI 生成证明的速度，已远超人类验证与吸收的速度。[77] 27 位菲尔兹奖得主联名抗议，指责 AI 公司将人类百年难题当作“跑分刷榜的 benchmark”。[75] 这场信任危机恰恰是本文第 3 节的活教材：生成（可达度）与可靠性（覆盖度与验证），是两件必须用不同证据区分的事。

第三，形式化数学重新回到舞台中央，成为信任危机中唯一的避风港。当自然语言证明的可信度遭受质疑，DeepMind 于 10 月 8 日发表于《Science》的 AlphaProof Nexus 给出了另一种答案：以“大模型 + Lean 编译器反馈”的极简架构，解出悬置 56 年的 Erdős 问题，且每一步证明都经 Lean 内核逐行核验。[73] 形式化是唯一“验证器按构造可靠”的角落——它既是希望，也是一面照妖镜。

1.1 这篇综述的四个问题

我们不按方法罗列，而按四个问题组织：

RQ1（界定）：数学能力由哪些层次构成？每一层如何测量、如何失败？
RQ2（测量）：给定一个基准分数，它究竟在测覆盖度、可靠度，还是可达度？
RQ3（机制）：模型内部的哪些结构、训练信号与验证器，决定了这三者的上限？
RQ4（归因）：当分数上涨时，涨的是模型能力，还是工程与评测？

四个问题对应四张地图：能力层图、测量三轴图、机制证据图、归因设计图。本文的贡献，是把它们叠在同一张纸上——并在纸的空白处，记下 2026 年秋天那场风暴的位置。

1.2 与已有综述的关系

数学推理的综述并不少。Plaat 等人从“生成—评估—控制”三个动作梳理多步推理；[9] 刘等人在 2026 年的 ACM Computing Surveys 上系统整理了数学语言模型的任务与方法，编目六十余个数据集；[10] 更早的 IEEE TPAMI 综述专注于应用题求解的语义解析；[11] 另有以 CoT 为中心的分类学综述。[12] 这些工作各有价值，但大多按“方法”或“数据集”组织。

本综述的不同之处在于：它按问题组织，并给出一套可计算的测量语言。它不试图穷尽所有论文，而试图给出一个坐标系——任何一篇新论文、任何一次新发布、任何一场新争论，都可以被安置在某一层、某一轴、某一种证据等级之上。

1.3 产业前线：四条路线的并置与张力

2026 年秋季的数学 AI 版图，已分化为四条截然不同的路线。把它们并置，是为了看清同一个问题的四种押注。

OpenAI：规模冲击与“证明消化不良”。 轨迹清晰：2024 年 9 月，o1 把测试时计算推向主流；2025 年 7 月，实验性推理模型在 IMO 达到金牌水平（6 题解出 5 题）——注意这是 OpenAI 自评，未经 IMO 官方协调人评分，与 DeepMind 的官方认证金牌存在验证强度上的不对称；2025 年 12 月，GPT-5.2 在 AIME 2025 上无工具满分，在 FrontierMath 第一至三档（带工具）达到 40.3%；[69] 2026 年 9 月，GPT-6 Astra 把 Tier 4 推到 97.6%。[74]

但比分数更重要的是两次转向。第一次是 2025 年 11 月的“人机协作发现”：数学家 Sawhney 与 Sellke 在 Erdős 问题 #848 上卡住最后一步，GPT-5 Pro 提出了“一个不合规律的数如何在其余所有数上制造矛盾”的关键想法，两位数学家据此完成证明；研究者 Coester 用 GPT-5 做头脑风暴，模型指出一个几何构造，经改进后给出在线算法竞争比的更强下界。[68] 这些案例的共同结构是：模型不给出答案，模型给出洞察；人类判定洞察的价值并完成证明。 第二次转向则是 2026 年 10 月的“手稿轰炸”：上万个智能体、88 小时、722 篇手稿、3 篇撤回。[72] 帝国理工学院 Kevin Buzzard 的抽查显示，其数论手稿中仅有极少数能通过 Lean 验证。同一个实验室，一年之内演示了 AI 数学的两种形态：作为洞察发生器的克制形态，与作为手稿工厂的失控形态。 前者指向 L5 的真实路径，后者暴露了缺乏硬验证器时海量生成的脆弱。

Anthropic：可靠的工匠与照妖镜。 Claude 的数学轨迹呈现另一种气质。Opus 4.5（2025 年 11 月）在 AIME 2025 上达到 91.3%，在多语言数学基准 PolyMath 上以 79% 位居前列；2026 年的 Opus 4.6 则把“数学 + 代码”的组合推向极致——接近满分的竞赛数学成绩加上业界领先的 SWE-bench 表现，使其成为“可实现的数学”（算法设计、数值方法、科学计算）的首选工具之一。[70] Anthropic 没有把赌注押在“奥数金牌”这类标志性事件上，而是押在可靠性、长程智能体与工具集成上——用本文的语言说，他们优先经营可靠度与可达度，并坦率地把覆盖度的问题留给未来。

Anthropic 对本文更重要的贡献在另一面：它是机制可解释性研究的主要推动者，而可解释性正是归因问题的显微镜。2026 年 8 月的一项受控实验发现，Claude Opus 4.5 在语义上无意义的填充 token 下可获得最高 13 个百分点的推理增益，且能在思维链完全不显露的情况下满足一个隐藏的模算术约束。[71] 这是一个干净的因果证据：可见的思维链低估了模型真实的计算面。 它动摇了“读 CoT 就能审计推理”的假设，也给本文命题 1 的推论二——“机制不在曲线里”——补上最锋利的一块拼图：机制甚至不在你看得见的过程里。

DeepMind：形式化优先与奥卡姆剃刀。 与 OpenAI 的智能体人海战术不同，AlphaProof Nexus 走的是严格的同行评审与形式化路线。[73] 其架构简洁到近乎朴素：Gemini 3.1 Pro 用 Lean 起草证明，编译器逐行检查并将报错反馈，驱动下一轮修改；定理陈述不可修改，不允许 sorry 占位符，不允许私加公理。最震撼的是其中的消融实验：拆掉进化算法、多子代理等复杂组件，仅保留“基础模型 + 编译器反馈”，依然能解出那 9 道 Erdős 难题。这为本文的核心论点提供了最强背书：当前科研级数学 AI 能力的主要来源，不是复杂的系统架构，而是基础模型与硬验证器的紧密结合。 验证器不是拐杖，而是外骨骼。

中国路径：国产模型与深度人机协同。 10 月中旬，大湾区大学许地生团队依托书生科学多模态大模型 S2（Intern-S2），完成了困扰数学界三十余年的三维 Ghys 猜想证明，并由北大团队在 Lean 中完成形式化验证。[76] 与 OpenAI 的“黑盒并发”不同，该团队采用“7 批接续推演、389 个节点拆解”的深度人机协同模式。这验证了另一种范式：把专家直觉系统性地接入机器求解回路，在 L4/L5 层形成闭环。它不是算力的胜利，而是接口设计的胜利。

四条路线，四种押注：OpenAI 赌规模，Anthropic 赌可靠，DeepMind 赌验证器，中国团队赌人机接口。本文的框架恰好为这场赌局提供计分规则：无论哪条路线，最终的裁判都是同一个问题——覆盖度动了吗？代价是多少？人类还能不能消化？

2. 方法论：我们如何检索、筛选与分级

一篇综述的可信度，一半在结论，一半在方法。本节将检索与筛选过程写到可复现的程度。

2.1 研究问题与证据类型

对应 RQ1–RQ4，所需证据分为四类：定义性文献（能力、覆盖度、验证器）、测量性文献（基准、估计量、统计）、机制性文献（架构、表征、训练动力学）、工程性文献（RLVR、搜索、工具、形式化）。四类证据的强度标准各不相同：定义靠论证，测量靠统计，机制靠干预，工程靠对照实验。这正是本文采用 E/S/R 三轴分级、而非简单的“重要/不重要”二分的原因。

对 2026 年 9–10 月的突发事件（Nexus、722 篇手稿、Ghys 猜想、First Proof），我们额外引入一类证据：同行评议反应——包括菲尔兹奖得主公开信、专家抽查（Buzzard 的 Lean 复核）与顶刊接收情况。这类证据不属于上述四类中的任何一类，但它度量的是本文反复强调的东西：数学共同体的信任，是一种不可绕过的社会验证器。

2.2 五个来源与检索窗口

检索覆盖五个来源：Google Scholar、ACM Digital Library、IEEE Xplore、ScienceDirect、arXiv。前四者覆盖同行评审的期刊、会议与工作坊，arXiv 覆盖高影响力预印本与技术报告。

时间窗口为 2017 年 1 月至 2026 年 10 月 18 日。对 2026 年的文献，我们单独进行了一轮“时效性扫描”（关键词附加 2026、2609、2610 前缀），并补入《Science》2026 年 10 月的 Nexus 论文、OpenAI 技术报告与 First Proof 项目报告。

检索式按三个块组合：

任务块：mathematical reasoning、math word problem、theorem proving、formalization、Lean、Isabelle、AIME、MATH、OlympiadBench、FrontierMath、PutnamBench；
模型块：large language model、LLM、chain-of-thought、reinforcement learning、RLVR、verifiable reward、process reward、test-time compute、search；
评价块：benchmark、evaluation、emergent ability、coverage、pass@k、contamination、self-improvement、scaling law。

块与块之间用 AND 连接，块内用 OR。每个来源至少执行两轮：第一轮宽检索（标题/摘要），第二轮针对高被引与近两年文献做引文追踪。

2.3 纳入与排除标准

纳入：（i）提出或分析大模型数学推理的方法、基准、机制或评测；（ii）提供可核验的实证、证明或系统性测量；（iii）为同行评审论文、工作坊论文、技术报告或高影响力预印本；（iv）具有可解析的标识（arXiv ID、DOI、Anthology ID）。

排除：（i）仅涉及初等算术教育、与 LLM 无关者；（ii）纯应用报告、无可复用方法或证据者；（iii）无法核验元数据的条目；（iv）重复发表（保留正式版；预印本仅在正式版不可得时保留）。

2.4 筛选流程与数量

初次检索得到约 1,400 条候选。去重后约 620 条；标题与摘要筛选后约 260 条；全文/元数据核验后保留 196 条进入文献库。正文引用其中约 100 条，其余作为延伸文献库供读者检索。

需要说明的是，这一流程并非一次完成。第一轮（2026 年 10 月 17 日）得到 188 条；第二轮（10 月 18 日）补入 ACM/IEEE/ScienceDirect 的历史与形式化文献、2026 年 9–10 月的新预印本，以及 Nexus、Ghys、First Proof 等最新文献，最终确定为 196 条。两轮之间修正了若干数字与归属，修正记录保留在文献库的勘误表中。

2.5 证据分级：E/S/R 三轴

轴	取值	定义
E 证据类型	E0 定义/公理；E1 数学推导；E2 观察；E3 因果干预；E4 系统测量或元分析	这是哪一种证据
S 来源独立性	S1 单团队；S2 多团队独立；S3 独立复现	谁做的、是否独立
R 复现状态	R0 未检验；R1 已复现；R2 复现失败	重复出来了吗

升降级规则：进入正文的机制性断言至少需达到 E3+S2+R1；进入摘要的实证断言至少需达到 E4+S2+R1；出现 R2 时，相关主张必须收缩。单团队结果一律标注；预印本一律标注；模型依赖的结果必须写明边界。

这套分级直接决定了本文哪些句子用“已确立”、哪些用“据报道”、哪些用“我们推测”。2026 年秋季的三件大事在这套分级下的位置一目了然：Nexus（E3/S1/R1，单团队但经《Science》同行评审与 Lean 核验）、722 篇手稿（E2/S1/R2，已出现撤回）、Ghys 猜想（E3/S2/R1，证明与形式化验证分属两个团队）。等级即态度。

2.6 综合方法

我们采用“主题编码 + 层—轴映射”的两步法。第一步，对文献做主题编码；第二步，将每个主题映射到五层能力与三轴测量之上，检查是否存在空缺的“层—轴”格子。空格子即文献缺口，也是第 14 节“灯塔”的来源。

这种做法不允许我们用“方法很多”来掩盖“某些格子没有证据”。例如，L5（数学创造）在“形式验证”轴上曾几乎是空的——2026 年 10 月之后，这个格子里终于有了两个条目（Nexus 与 Ghys），而它们恰好是全文最有分量的两条证据。

2.7 方法论的局限

以下五条必须诚实列出。

Google Scholar 无法直接抓取。本环境两次尝试均被反爬拦截；GS 仅作为检索索引，元数据以 arXiv API、Crossref DOI 或出版社页面为准。
arXiv 偏多。2023–2026 年该领域的进展大量以预印本形式出现；代价是部分结论尚未经同行评审。
英语偏多。中文、日文、德文文献覆盖不足，这是本稿的明确缺口。
发表偏倚。正结果更容易被发表；我们尽量纳入负结果，但仍不完整。
时效判断的主观性。2026 年 9–10 月的事件（Nexus、722 手稿、Ghys）距今太近，其历史地位尚未沉淀；本文对它们的权重判断，带有不可避免的时效偏差。

3. 三个“会”：覆盖、可靠、可达

“会数学”至少有三种意思。把它们分开，是这篇综述的第一件事。

第一种：会不会。 世界上是否存在一条从题目通往正确答案的路，而模型有能力走上去？我们称之为覆盖度（coverage）。它回答的是“可能性”：给定无限次尝试，模型能否至少成功一次。

第二种：做不做得对。 模型通常能否一次做对？我们称之为可靠度（reliability）。它回答的是“稳定性”：一次出手，命中的概率有多大。

第三种：找不找得到。 给我 $k$ 次采样、或者一棵搜索树、或者一个验证器，我能否把那条正确的路找出来？我们称之为可达度（access）。它回答的是“工程”：用多少算力，才能把“可能”变成“发生”。

三个词，对应三种失败。覆盖度不够，是“根本不会”；可靠度不够，是“会而不稳”；可达度不够，是“会而找不到”。现实中的争论，十有八九是把这三种失败混成了一种。

举一个具体的例子。设某模型在 AIME 上的 pass@1 为 20%，pass@64 为 65%。 $R\approx0.20$ 是单次出手的命中率； $A_{64}\approx0.65$ 说明给它 64 次机会，三分之二的题目至少能碰对一次；而 $\mathrm{Cov}$ 至少为 0.65，且可能更高。若某方法把 pass@1 提到 30% 而 pass@64 不变，它提升的是可靠度；若把 pass@64 提到 85% 而 pass@1 不变，它提升的是可达度；唯有当“即使无限采样也解不出的题目”开始被解出，覆盖度才真正动了。三种改进，三种叙事，却常常被同一句“模型变强了”所掩盖。

2026 年 10 月的 722 篇手稿事件，是这三个量的一次大规模实景演示。上万个智能体并发，是把可达度工程推到极限——生成的路径足够多，总有几条看起来像路；符号错误导致的撤稿，是可靠度的失守——像路的不等于路；而 Buzzard 抽查中“极少数能通过 Lean 验证”的数论手稿，则说明覆盖度几乎未动——新路并没有被走出来，至少没有被认证为走出来。一次发布，三个量，三种命运。 这正是本文坚持把它们分开测量的现实理由。

3.1 一个形式化的说法

固定题目分布 $\mathcal{D}$ 、模型策略 $\pi_\theta$ 、解码分布与验证器 $V(x,y)\in\{0,1\}$ 。定义每题的成功率

$q_\theta(x)=\Pr_{y\sim\pi_\theta(\cdot\mid x)}\big[V(x,y)=1\big].$

于是：

可靠度 $R(\theta)=\mathbb{E}_{x}[q_\theta(x)]$ ；
可达度 $A_k(\theta)=\mathbb{E}_{x}\big[1-(1-q_\theta(x))^k\big]$ ，其无偏估计量见 HumanEval [13]；
覆盖度 $\mathrm{Cov}(\theta)=\mathbb{E}_{x}\big[\mathbf{1}\{q_\theta(x)>0\}\big]$ 。

用一句话翻译： $R$ 是“闭着眼走一步，走对的概率”； $A_k$ 是“给我 $k$ 步，至少走对一步的概率”； $\mathrm{Cov}$ 是“这条路到底通不通”。

注意 $V$ 在这个定义中的位置：它决定了我们谈论的是哪一种“对”。当 $V$ 是答案比对，覆盖度测的是“答对”；当 $V$ 是 Lean 内核，覆盖度测的是“证对”；当 $V$ 是人类专家的启发式审查，722 篇手稿事件告诉我们，这个 $V$ 在吞吐量面前会失效。三个量的定义都依赖验证器；验证器的选择，因此是一切测量的第一块基石。

对有限精度的模型， $q_\theta(x)>0$ 应读作 $q_\theta(x)\ge\varepsilon$ （例如 $10^{-6}$ ）。覆盖度因此不是一个哲学概念，而是一个可用足够大的 $k$ 从下方逼近的统计量。第 5.3 节将给出这一下界的具体算法。

3.2 为什么这三个量必须分开

因为它们对应三种完全不同的改进。

提高覆盖度，靠的是预训练、架构、数据，以及能改变“支撑集”的后训练。这是最慢、最贵、也最接近“变聪明”的一种。
提高可靠度，靠的是让已有的正确行为更常发生：格式对齐、答案抽取、拒绝采样、偏好优化——以及，把输出交给一个硬验证器过滤。
提高可达度，靠的是采样、搜索、验证器、工具。这是过去三年最便宜、最常见、也最容易被误读为“能力”的一种。

一句话：覆盖度是山的高度，可靠度是路的平整，可达度是灯照得多远。 灯可以越做越亮，但灯照不出山的高度；而 2026 年秋天我们学到的另一课是：灯照得太快，还会让人看不清路。

4. 五层塔：能力的光谱

数学能力不是一堵墙，而是一座五层的塔。每一层材质不同，所需的尺子也不同。下表先给全貌，随后逐层展开。

层次	核心能力	典型任务	验证器	2026 年 10 月现状	证据等级
L1 数感	近似数量、大小、比较	数轴、估算	近似比对	基本具备；数字有结构表征	E3/S1/R0（小模型）
L2 符号算术	精确规则操作	多位数、代数	结果检查器	会算但不稳；机制为启发式	E3/S1/R0
L3 关系推理	嵌套、组合、多跳	应用题、关系题	跨分布测试	两两强、嵌套弱	E2/S1/R0
L4 演绎证明	策略选择与元认知	奥赛证明、Lean	过程/形式验证	Nexus 解 56 年悬案；Ghys 猜想获证	E3/S2/R1（形式域）
L5 数学创造	猜想、反例、类比	新猜想、开放问题	几乎无	722 篇手稿引发信任危机；First Proof 盲测登场	E2/S1/R0

表 1. 五层能力光谱。2026 年秋季的冲击集中在 L4 与 L5 的边界：L4 在形式域内被实质性推高，L5 则在自然语言域内遭遇信任破产。

第一层，数感。 对数量级、大小、近似关系的直觉。这一层最接近“感知”，也最容易被误认为“数学”。

第二层，符号算术。 精确的规则操作。模型的算术能力，远看像算法，近看更像一袋启发式：几何近似、稀疏神经元、读出阶段的量化误差——三类证据都指向“会算但不稳”。[14][15][16] 值得强调的是，这三类证据来自不同模型、不同任务、不同方法，没有任何一项实验同时证明三者在同一模型内共存；将它们合并为一个“算术机制”是过度概括。

第三层，关系推理。 多跳、嵌套、组合。模型擅长两两关系，弱在嵌套。GSM-Symbolic 的实验是这一层的典型诊断：换掉名字与数字，准确率骤降，说明模型学到的可能是模板而非关系。[17]

第四层，演绎证明。 不只是“答案对”，而是“每一步都成立”。最好的过程验证器是形式化证明助手：Lean 的核要么接受，要么拒绝，没有中间地带。[18] 2026 年的形式化版图已与两年前不同：AlphaProof 在 IMO 级问题上达到银牌水平，[6] Seed-Prover 1.5 报告 PutnamBench 88%，[8] 而 10 月的 Nexus 把这条线推进到研究级——悬置 56 年的 Erdős 问题，第一次被机器在形式系统内证毕。[73] 同年同月，Ghys 猜想的证明也在 Lean 中完成核验。[76] 但必须诚实：形式化覆盖的领域仍然狭窄，研究级数学的定义体系远未被覆盖。Nexus 解出的 9 道 Erdős 问题，是从 353 道候选中筛出的——机器的覆盖度动了，但动得克制。

第五层，数学创造。 提出猜想、构造反例、发现类比、判断什么值得证明。这一层几乎没有自动验证器。FunSearch 的成功恰恰因为它有一个可计算的评价函数；[19] 一旦评价函数本身需要数学判断，循环就闭合不了。2026 年 10 月为这一层补上了两个对照样本：OpenAI 的 722 篇手稿展示了没有验证器的 L5 会退化成什么——数量的狂欢与符号的错误；[72] First Proof 项目则展示了有盲审的 L5 应当如何测量——10 道未发表的研究级问题，24 小时，最终只有一个系统解出一道。[78] 创造仍在，但它比任何宣传都慢、都贵、都挑剔。

五层之间并非并列关系，而是验证难度递增：越往上，越难廉价地判断对错；越往上，越依赖人的判断。这也解释了数学为何成为 AI 的首选试验田——不是模型已经登顶，而是第二、三层恰好有便宜而可靠的检查器。是可验证性选择了这个领域，而不是这个领域选择了 AI。2026 年秋天的一切冲突，都可以回溯到这一个句子。

表 2 给出截至 2026 年 10 月的代表性基准图谱。

基准	规模	主要能力层	验证器	2026 年 10 月状态	主要风险
MATH-500	500	L2–L3	答案比对 / sympy	接近饱和	污染、饱和
GSM8K	8.5k	L2–L3	数值比对	饱和	模板化
AIME 2024/2025	30/年	L3–L4	答案比对	满分已现（GPT-5.2 无工具）	样本小、失效
FrontierMath	数百	L4–L5	专家 + 自动	Tier 4 达 97.6%（GPT-6 Astra）	基准失效
AMO-Bench	50	L4	答案	最佳 52.4%	样本小、原创
MATH-Beyond	子集	L4	答案	基座 pass@1024 仍失败	构造偏差
First Proof	10/批	L5	人类专家盲审	ProofCouncil 解出 1/10（第三批）	成本极高、不可规模化
miniF2F	488	L4	Lean / Isabelle	接近饱和	形式化覆盖
PutnamBench	640	L4–L5	Lean / Isabelle / Coq	约 88%（Seed-Prover 1.5）	形式化人力
FormalMATH	5,560	L4	Lean 4	约 16.46%	自动形式化保真

表 2. 代表性数学基准图谱（截至 2026 年 10 月）。FrontierMath 的饱和与 First Proof 的出现，标志着评测范式的强制迭代：从公开题集走向盲审难题。

5. 一条曲线证明不了一座塔

现在到了本文的技术核心。请耐心看两个命题；它们不长，但会把许多热闹的争论一次性钉在墙上。

5.1 命题一：曲线只看得见矩

命题 1. 对任意正整数 $k$ ，

A_k(\theta)=\sum_{j=1}^{k}(-1)^{j+1}\binom{k}{j}\,\mathbb{E}_{x}\big[q_\theta(x)^j\big].

也就是说， $k$ 次采样的 pass@ $k$ ，仅通过每题成功率分布的前 $k$ 阶矩依赖模型。任何两个每题成功率分布相同的模型，在所有 $k$ 上都无法区分。

证明. 由二项式定理，

1-(1-q)^k=\sum_{j=1}^{k}(-1)^{j+1}\binom{k}{j}q^j,

对 $x\sim\mathcal{D}$ 取期望即得。 $\square$

这条命题的杀伤力在于三个推论。

第一，pass@ $k$ 是一架矩望远镜。 你看到的永远是低阶矩。想看得更远，只能加预算；而预算不是免费的。

第二，机制不在曲线里。 一个用“时钟电路”做加法的模型，与一个用“一袋启发式”做加法的模型，可以拥有相同的 $q$ 分布、相同的 pass@ $k$ 曲线。[20][15] 2026 年 8 月的填充 token 实验把这把刀磨得更利：模型甚至可以在思维链完全不显露的情况下完成隐藏计算——[71] 曲线相同，不等于机制相同；过程可见，也不等于机制可见。

第三，平均会骗人。 $R$ 与 $A_k$ 都是题目上的平均。一个让九成题目微涨、同时把最难一成题目摧毁的方法，可以让两个指标同时上涨，而让覆盖度悄悄缩小。平均值是一张平滑过的脸，好看，但不一定真实。

此处需要一句补充：对有界随机变量 $q\in[0,1]$ ，其矩序列唯一决定分布（Hausdorff 矩问题）；因此若 $k\to\infty$ ，理论上可以恢复 $q$ 的分布，进而恢复覆盖度。命题 1 的限制在于有限 $k$ 。这也解释了为什么“大 $k$ ”研究重要：它们不是在做另一种指标，而是在把望远镜推得更远。[21]

5.2 命题二：工程在覆盖度处熄火

命题 2. 固定模型 $\theta$ ， $A_k(\theta)$ 关于 $k$ 单调不减，且当 $k\to\infty$ 时收敛到 $\mathrm{Cov}(\theta)$ 。

证明. 对每个题目 $x$ ， $1-(1-q_\theta(x))^k$ 随 $k$ 单调递增，极限为 $\mathbf{1}\{q_\theta(x)>0\}$ ；由单调收敛定理，期望的极限等于极限的期望。 $\square$

用一句话说：采样、搜索、重排序，只能把模型的灯照遍整座塔，不能给塔加一层。

2026 年 10 月的手稿事件，可以读作命题 2 的一次工程极限实验。“88 小时、上万个智能体”本质上是把 $k$ 推向天文数字的极端形式；符号错误则证明，如果没有可靠的 $V(x,y)$ ， $A_k$ 的扩张只会带来灾难性的假阳性。[72] 命题 2 说的是“收敛到覆盖度”；手稿事件补上了它的现实注脚：当验证器的假阳性率不为零时，收敛到的东西甚至不是覆盖度，而是覆盖度的幻象。

5.3 覆盖度怎么估：一个可操作的界

覆盖度并非不可估计。给定 $k$ 次独立采样，若某题的真实成功率为 $q$ ，则“一次都没成功”的概率为 $(1-q)^k$ 。于是：

若 $q\ge\varepsilon$ ，则漏掉该题的概率不超过 $(1-\varepsilon)^k$ ；
因此，“至少成功一次”的题目比例，是 $\mathrm{Cov}_\varepsilon=\mathbb{E}[\mathbf{1}\{q\ge\varepsilon\}]$ 的一个下界估计，其偏差上界为 $(1-\varepsilon)^k$ 。

取几个具体的数： $\varepsilon=0.01$ 时， $k=256$ 的漏检概率约为 $7.6\%$ ， $k=512$ 约为 $0.58\%$ ， $k=1024$ 约为 $3.4\times10^{-5}$ ； $\varepsilon=0.001$ 时， $k=1024$ 的漏检概率约为 $36\%$ 。这张小表说明两件事：大 $k$ 确实能估覆盖度，但代价随 $\varepsilon$ 指数上升；而文献中常用的 $k=64$ 或 $k=128$ ，对“低概率但存在”的行为几乎无能为力。

5.4 统计功效：小基准上的大结论

覆盖度之外，还有一个更朴素的问题：样本够不够。

设两个方法在 $n$ 道题上的成功率分别为 $p_1,p_2$ ，要检测 $\Delta=|p_1-p_2|$ 。两比例检验的近似样本量为

n\approx\frac{(z_{1-\alpha/2}+z_{1-\beta})^2\,[p_1(1-p_1)+p_2(1-p_2)]}{\Delta^2}.

取 $\alpha=0.05,\beta=0.2$ ， $p\approx0.5$ ， $\Delta=0.05$ ，得 $n\approx1{,}570$ 每臂。也就是说，在一个 500 题的基准上检测 5 个百分点的差异，功效不足；在 AIME 这样的 30 题基准上，两个百分点的差距几乎无法与噪声区分。

First Proof 项目把这个问题推到了极致：每批只有 10 道题。[78] 在这样的样本量上，“ProofCouncil 解出 1/10”既不能证明系统级智能突破了 L5，也不能证明它没有——它只能证明在 10 道特定的未发表难题上，有一个系统解出了其中一道。这不是贬低 First Proof；恰恰相反，它是目前唯一杜绝了污染的 L5 测量。但它的每一个数字都必须附带这样的限定。小样本不是罪，隐瞒小样本才是。

6. Transformer 的三道天花板

如果覆盖度会被限制，限制从哪里来？三条结构性的事实，值得放在一起看。

第一道，深度。 对数精度、前馈网络可在输入线性空间内计算的 Transformer，可被常数深度的阈值电路模拟，落在 $\mathsf{TC}^0$ 之中。[22][23] 这是单次前向的上界：思维链 token 提供串行计算，相当于在纸上多写几行，把深度借出来。[24] 于是，一些“数学失败”其实是深度失败；而思维链是一种用 token 买深度的工程。

第二道，长度。 无位置编码（NoPE）在长度泛化上表现最好，常见的显式位置编码反而外推很差。[25] 这是架构对“训练分布之外”覆盖度的影响：它改变的是模型在未见长度上能不能做，而不仅是做对的频率。这是少数几个架构可能真正触及覆盖度的地方。

第三道，监督。 在解答上做下一词预测，训练信号只覆盖最终答案，不覆盖中间步骤。过程监督可以补上步骤级信号，[26][27] 但代价是引入一个学出来的验证器，而它的错误可能被策略利用。[28] 约束并非“过程信号不可能”，而是默认训练信号里没有过程信用。

三道天花板合起来，给出一张分工图：深度与长度是架构的地盘，验证与搜索是工程的地盘。Nexus 的消融实验为这张分工图加了一条醒目的边注：当验证器足够硬（Lean 内核），许多精巧的架构组件可以被直接拆掉而不损失顶点能力。[73] 天花板之下，真正不可替代的东西比我们以为的少。

7. 模型一侧：数据、架构、后训练

7.1 数据：沉默的地基

数学能力的底座是数据。这里有一个常被忽略的区分：数据可以让模型“见过”更多题型（覆盖度），也可以让模型“更熟”已有题型（可靠度）。 两者在分数上长得一样，在泛化上完全不同。GSM-Symbolic 用一个简单的实验把这件事说透：同一道题换掉人名与数字，模型准确率可以骤降。[17]

合成数据的另一面是污染。MathArena 用实时赛题评测，直接给出污染的证据；[33] First Proof 则用“未发表”三个字把污染从根上切除——[78] 这是 2026 年评测设计最重要的发明，其代价是每批十题的规模与不可复制的稀缺性。干净的测量从来都这么贵。

7.2 架构：把深度做成可调

近几年最有趣的一类工作，是把“深度”从固定结构变成可调资源。Huginn 用循环块在测试时反复展开；[30] Ouro 把循环计算放进预训练；[31] Think-at-Hard 只在可能出错的 token 上触发潜在迭代；[32] 另一篇同名工作 Nexus（高阶注意力机制）让 Query 与 Key 由内层注意力生成。[35]

这些工作值得认真对待，因为它们有可能改变覆盖度。但也必须诚实：它们多在中小模型、较短任务上验证。把它们当作“架构已经解决数学”的证据，为时过早；把它们当作“覆盖度可以被架构改变”的存在性证明，则恰如其分。

7.3 后训练：一场罗生门

RLVR 是过去两年数学进步中最响的名字。DeepSeek-R1 证明，纯结果奖励的强化学习可以激励出长思维链与自我检查；[36] GRPO 使这套方法在工程上可行。[37]

但“RLVR 到底做了什么”，是一场罗生门。Yue 等人用大 $k$ 的 pass@ $k$ 观察：RL 模型在小 $k$ 上更好，大 $k$ 上反而不如基座。[21] Wen 等人反驳：若把中间步骤也纳入正确性，RLVR 确实扩展了推理边界。[38] Shao 等人的伪奖励实验更棘手：在 Qwen2.5-Math 上，随机奖励也能带来 21.4 个百分点的提升。[39] 1-shot RLVR 用一条样本把 MATH-500 从 36.0 推到 73.6。[40]

2026 年的新证据把这场罗生门推向更细的层次。MATH-Beyond 从反面构造了一个“基座在 pass@1024 下也解不出”的题目集，发现现有 RL 微调模型在这些题上表现很差。[5] 另一边，SOAR 用非对称自博弈让教师为学生生成“跳一跳够得着”的题目；[41] On-Policy Warmup 给出“初始验证成功率”与“奖励发现复杂度”的下界；[42] Tan 等人发现 RL 后训练的效率随规模饱和；[43] ProRL 报告延长 RL 可以扩界；[44] STEER 从 token 级熵变的角度重新解释熵坍缩。[45]

而 Nexus 的消融实验为这场罗生门提供了最新的、也许是最刺耳的一条证词：把复杂的 RL 架构拆到只剩“模型 + 编译器反馈”，Erdős 难题依然倒下。[73] 这并不直接裁决 Yue 与 Wen 之争——它裁决的是一个更朴素的问题：在那些被反复打磨的 RL 组件里，有多少是能力，有多少是装修？ 至少在一个场地上，答案是：装修居多。

我们的读法不是选边，而是指出：这些证据之所以看似互相矛盾，是因为它们测的不是同一个量。把它们放进 R/A/Cov 的框架，罗生门就变成了一张分工表。

7.4 一个必要的形式化：KL 预算能搬动多少概率质量

要理解“RLVR 能不能创造新行为”，一个绕不开的量是 KL 预算。

KL 正则目标的理想化最优解是参考策略的指数倾斜：

\pi^\ast(\tau)=\frac{1}{Z}\,\pi_{\mathrm{ref}}(\tau)\,e^{r(\tau)/\beta},\qquad Z=\sum_\tau\pi_{\mathrm{ref}}(\tau)e^{r(\tau)/\beta}.

由 Pinsker 不等式，单步的总变差距离被 $\sqrt{\varepsilon/2}$ 约束。但有两个容易犯的错误。第一，KL 不满足三角不等式，正确的做法是逐步使用 TV 的三角不等式： $D_{\mathrm{TV}}(\pi_T,\pi_{\mathrm{ref}})\le\sum_t\sqrt{\varepsilon_t/2}$ 。第二，Pinsker 界对稀有行为是松的：设某条轨迹在参考策略下的概率为 $\delta$ ，要在 KL 预算 $\varepsilon$ 内把它放大到 $a$ ，大致需要 $a\log(a/\delta)\le\varepsilon$ 。数值上： $\varepsilon=0.01,\delta=10^{-9}$ 时， $a_{\max}\approx7.9\times10^{-4}$ ；把 $\delta=10^{-9}$ 放大到 $a=0.1$ 需要 $D_{\mathrm{KL}}\approx1.75$ 。换句话说，小 KL 预算无法把“可忽略概率”放大成“常用行为”。这解释了为什么伪奖励、熵正则、优化器偏置这些“非语义”因素可以在小预算下产生大的分数变化——它们改变的不是某条稀有轨迹的概率，而是整个策略的锐化方式。

8. 验证器一侧：四种裁判与“消化不良”

数学能力的外骨骼，是验证器。没有验证器，数学只是文本；有了验证器，数学才成为可被自动改进的对象。

按可靠性与成本，验证器大致分为四种。

结果验证器：只检查最终答案。最便宜，也最容易被游戏。

过程验证器：给每一步打分。信号更密，但它是学出来的：分布内好用，分布外可能退化得更快；它的错误会被策略利用。[26][27][46]

形式验证器：Lean、Isabelle 的核。按构造可靠；代价是窄。[18][47]

工具验证器：代码解释器、符号求解器。对可计算的问题精确，对证明无能为力。[48]

2026 年 10 月，这个四分法之外又浮现出第五种——也是最古老的一种：人类共同体。陶哲轩提出的“证明消化不良”，本质上揭示了人类验证器的带宽瓶颈。[77] 数学求解被拆分为生成、验证、消化三个环节；AI 急剧加速了前两者，但“消化”——人类理解、吸收、传承新证明——仍依赖人类的节奏。这导致了结构性脱节：AI 产出了“正确”的证明，数学共同体却无法将其转化为“知识”。27 位菲尔兹奖得主的联名信，正是这种脱节的社会学表达。[75]

由此得到一个冷静的推论：验证器的吞吐量，而非仅仅是准确率，已经成为数学 AI 的硬约束。 人类专家作为验证器，准确率极高、吞吐量极低；Lean 内核准确率高、吞吐量高，但覆盖面窄；结果比对吞吐量极高，却可被游戏。四种自动裁判与人类裁判一起，构成一个五维权衡：成本、可靠性、覆盖面、吞吐量、可消化性。722 篇手稿撞上的，是吞吐量的墙；Nexus 绕开的，正是这堵墙——它把验证整个搬进了编译器。

8.1 验证器的三个可靠性指标

谈论“验证器可靠”时，至少要区分三件事。假阳性率（FP）：错误答案被接受的比例。假阴性率（FN）：正确答案被拒绝的比例。可利用性（exploitability）：给定搜索预算，策略能在多大程度上找到“高分但错误”的输出。三者的取舍，本质上是“你更怕被骗，还是更怕错过”。722 篇手稿的撤回，是一次 FP 事件的公开直播：人类专家在海量文本面前，假阳性率悄然逼近不可忽视的水平。

8.2 验证经济学与“奥卡姆剃刀”效应

验证器不是免费的。因此，设计问题不是“用最好的验证器”，而是“在给定题型与预算下，哪种验证器的边际可靠性最高”。

Nexus 为这个问题提供了一份教科书式的答案。[73] 它的核心逻辑简洁到近乎苛刻：Gemini 3.1 Pro 用 Lean 起草证明，编译器逐行检查并反馈报错；定理陈述不可修改，不允许 sorry 占位符，不允许私加公理。而它的消融实验——拆掉进化算法与多智能体架构后，依然解出 9 道 Erdős 难题——构成了一条 E3/S2/R1 级证据：在 L4 层，验证器的确定性反馈比模型外部的复杂推理架构更重要。 验证器不仅是裁判，更是引导模型在巨大搜索空间中收敛的引力源。

8.3 过程验证的两个方向

第一，里程碑/组成性诊断。过程诊断类基准不再只问“最后对不对”，而是定位推理在哪一步失败，揭示“组成性差距”：每一步都会，连起来不一定对。[46] 第二，长程形式化。自动形式化从“单题”推向“长程研究级”时，暴露的瓶颈不在证明搜索，而在定义、引理与上下文的组织。[49]

9. 搜索：用算力买时间

如果覆盖度是山高，搜索就是灯。灯照得越远，越容易看见山上已有的路。

Snell 等人证明，在推理期多花算力，可以比单纯放大参数更划算；[50] s1 用简单的测试时扩展把一个小模型推到可观的水平；[51] Large Language Monkeys 把重复采样做到极致，展示出覆盖率随采样数上升的幂律；[52] rStar-Math 把搜索与验证器结合起来。[53]

但灯有灯的极限。命题 2 已经说过： $A_k$ 最终收敛到覆盖度。Illusion of Thinking 补上了另一半：当题目复杂度超过某个阈值，推理模型的准确率会整体崩塌，有时明明还有 token 预算却不再使用。[54]

First Proof 的第三批实验给出了搜索的光谱另一端：ProofCouncil 系统以多模型协调与昂贵算力，在 24 小时内解出了那道量子拓扑问题。[78] 这是“系统级智能”在 L5 前沿的一次真实得分，也是一次价格公示——它证明可达度工程可以买到覆盖度边缘的突破，但账单以系统复杂度与算力计。这场交易是否划算，取决于你问的是“能不能”还是“值不值”。

9.1 有效样本数：一个可推导的量

“ $k$ 条路径”不等于“ $k$ 条独立路径”。设各路径成功指示变量的两两相关系数为 $\rho$ ，则 $k$ 条路径平均成功率的方差为

\mathrm{Var}(\bar X)=\frac{p(1-p)}{k}\big[1+(k-1)\rho\big],

于是有效样本数 $k_{\mathrm{eff}}=k/[1+(k-1)\rho]$ 。当 $\rho\to1$ 时 $k_{\mathrm{eff}}\to1$ 。这解释了两件事：束搜索在确定性解码下几乎完全相关；树搜索的前缀共享会把一次前缀错误放大成整棵子树的失败。上万个智能体的并发也不例外：若它们共享同一个基座模型，它们的相关性远非零——一万个分身，不等于一万个独立的头脑。 这是 88 小时手稿实验最容易被忽略的统计学注脚。

9.2 搜索的边界

搜索什么时候有用？一个粗略的判据是：当验证器的可靠性高于随机，且题目的覆盖度尚未饱和时，搜索的边际收益为正。 反之，若验证器不可靠，搜索会把错误答案选出来；若覆盖度已饱和，搜索只是重复已知路径。

10. 自我改进：四个循环与一个瓶颈

“自我改进”听起来像模型在给自己上课。更准确的说法是：模型在一个循环中，用自己的输出（加上某种外部信号）更新自己。循环有四种。

自训练：模型生成解答，筛出正确的，再用来训练自己。STaR 是早期代表。[55] 风险是自我确认。自博弈：模型自己出题、解题、判分。Absolute Zero 与 R-Zero 展示了零外部数据下的可能性。[56][57] 风险是题库塌缩。自验证：生成多个候选，用验证器挑最好的。[26][27] 风险是验证器偏差。自蒸馏：强模型生成数据，弱模型学习。[36] 风险是教师偏差被固化。

四个循环共享同一个瓶颈：验证器。没有可靠的验证器，自训练放大错误，自博弈塌缩题库，自验证选错答案，自蒸馏固化偏差。负面结果已把边界画得很清楚：没有外部反馈时，自我纠正常常让推理变差；[58] 不加验证的自产数据训练会发生模型坍缩；[59] 对代理奖励过度优化遵循可预测的曲线。[28]

722 篇手稿是“自验证”循环在缺乏硬验证器时的大规模失败案例：智能体可以彼此引用、彼此确认，构成一个看似闭环的系统，但闭环里没有一个按构造可靠的裁判，循环就只能在文本层面空转。而 Ghys 猜想的成功恰恰是反例的反面：北大团队的 Lean 验证是闭环的最后一道锁——循环可以靠人合拢，但不能省略合拢的那只手。[76]

10.1 零奖励难题：SOAR 的启示

SOAR 让教师模型生成“跳一跳够得着”的题目，教师的奖励来自学生在真实难题上的进步。[41] 这提示：自我改进的瓶颈不只是验证器，还有课程。把人类数学教育的直觉翻译成工程语言，就是“用学生的真实进步作为课程生成的奖励”。

10.2 模型坍缩与误差累积

用自己生成的数据训练，若不加验证，分布会逐渐变窄；验证器（即使不完美）可以阻止坍缩。[59] 在数学上还有一层结构：若各步独立且成功率为 $p$ ，则 $n$ 步全对的概率是 $p^n$ ；当 $p=0.9,n=10$ 时只有 0.35。这就是“单步正确率”与“整题正确率”之间的乘法鸿沟，也是过程验证器在长链上的价值所在。

11. 形式化：黄金标准与定义的黑洞

形式化数学是这场游戏里最特殊的场地，也是 2026 年秋季唯一能抵御信任危机的避风港。

它的历史比大模型长得多。Bledsoe 在 1977 年就主张借助语义引导与领域知识做定理证明；[61] Melis 与 Siekmann 在 1999 年把“证明规划”写成知识驱动的搜索；[62] Ringer 等人在 2019 年系统总结了形式验证工程的实践。[63] “过程验证”与“策略选择”不是 LLM 时代的新发明，而是自动推理半个世纪的老问题。

大模型带来的变化是规模与速度，而 2026 年 10 月带来的变化是级别。Nexus 在 353 道悬而未决的 Erdős 问题中自主解出 9 道，每道证明都经 Lean 内核核验；[73] 中国团队用 Intern-S2 结合深度人机协同完成三维 Ghys 猜想的证明，并由独立团队在 Lean 中完成形式化。[76] 这两件事的共同意义不在于“机器又解出了几道题”，而在于：研究级数学的证明，第一次以“机器生成 + 机器核验 + 同行评审”的完整链条呈现在数学共同体面前。 在 27 位菲尔兹奖得主联名抗议的当下，[75] 形式化证明成为 AI 与数学共同体之间重建信任的唯一契约。

形式化之所以是“黄金标准”，是因为它的验证器按构造可靠：证明通过类型检查，就是真的通过。但它依然有一个黑洞：定义。自动形式化的瓶颈，往往不在证明搜索，而在把自然语言中的定义、假设、记号忠实地翻译成形式语言。FormalMATH 的报告很能说明问题：即便给出自然语言提示，形式证明的成功率也可能下降。[49] 形式陈述本身的保真度，没有任何验证器为其认证；一个“证明通过”的系统，可能证明的是一个被悄悄改写的命题。

11.1 保真度怎么测：三个层次

陈述层：形式陈述与自然语言陈述是否等价？可行的方法是“回译”与“测试等价”。定义层：形式化所用的定义，是否与非形式数学中的定义一致？这是最软也最致命的一层。证明层：证明是否真的通过了核？这一层由证明助手保证。三层的可靠性依次递增。这也是为什么“形式验证是黄金标准”必须加一个限定：它保证“从定义到结论”的正确，不保证“定义就是你想说的那个定义”。

11.2 形式化作为覆盖度的试验场

尽管有定义黑洞，形式化仍是目前唯一能“认证覆盖度扩张”的场地。在形式域内，我们可以把“基座模型在任何采样预算下都证不出”与“新方法证出了”区分开。Nexus 的 9 道 Erdős 问题之所以是 2026 年最硬的能力证据，不是因为它们难，而是因为它们同时满足三个条件：问题有独立的数学意义，证明经内核核验，消融实验排除了架构噪音。 三个条件，缺一不可；而自然语言基准上的任何“突破”，至今没有一个同时满足过。

12. 评测：分数之外与 First Proof

分数是仪器的读数。读数可靠，需要三件事：仪器校准、样本足够、环境干净。

校准：pass@1 与 pass@ $k$ 是两种仪器。用 pass@1 谈“能力边界”，如同用体温计量身高。[13] 样本：AIME 只有三十题，三十题上的两个百分点可能只是噪声（见第 5.4 节）。环境：污染与饱和。MathArena 用实时赛题评测；[33] GSM-Symbolic 用模板扰动揭示“记忆而非推理”；[17] LiveBench 用动态题目抵抗污染。[64]

2026 年秋季为这三件事各补了一个判例。校准：GPT-6 Astra 在 FrontierMath Tier 4 上的 97.6% 宣告这台仪器量程已满——不是模型登顶了数学，而是这把尺子量完了它的刻度。[74] 样本：First Proof 每批 10 题，任何结论都必须自带置信限定。[78] 环境：未发表难题盲测把污染从根上切除，代价是不可规模化。

12.1 饱和之后：反向构造与盲测

当基准饱和，研究者的选择曾经有两个：找更难的题，或者构造“基座也解不出”的题。2026 年 10 月之后，出现了第三个：找尚未发表的题。First Proof 代表了评测的新范式——它测量的不再是“模型见过多少题”，而是“模型在真正的未知面前能做什么”。[78] 一个健康的评测生态，应同时包含四类基准：能力谱系基准（测可靠度与可达度）、覆盖度基准（测扩界）、过程基准（测步骤正确性）、盲测难题（测 L5 的真实前沿）。前两类已有雏形，后两类刚刚起步。

13. 归因：把能力与工程分开，以及学界的抵抗

现在，我们可以把整篇综述收束到一个问题上：过去三年的进步，有多少来自模型，多少来自工程？

我们的回答依然是一个假说，而不是一个结论。

H2（诱出主导）：在 2023–2026 年大模型数学推理的进步中，可归因于“诱出”（Harness 加上不扩张覆盖度的权重重加权）的份额，大于可归因于“覆盖度扩张”的份额。支持它的证据包括：大 $k$ 下基座反超、随机奖励仍有效、单样本即可大幅提升、RL 学习效率随规模饱和、MATH-Beyond 上现有 RL 模型的失败；[21][39][40][43][5] 反对它的证据包括：过程约束下的扩界报告、延长 RL 的扩界报告、形式证明器的快速进步。[38][44][8]

而 2026 年秋季发生的两件事，为 H2 提供了意想不到的社会学注脚。

第一件事是 27 位菲尔兹奖得主的联名信。[75] 他们批评 AI 公司将人类百年难题当作“跑分刷榜的 benchmark”，仓促公布而缺乏思路梳理。从本文的框架来看，数学家们抗议的正是用算力堆砌的可达度暴力覆盖了问题，却没有提供人类可消化的覆盖度与洞察。数学共同体本能地排斥那些“只有结果、没有过程”的工程胜利。这不是守旧，而是测量直觉：一群以验证为毕生技艺的人，一眼认出了没有经过验证器的东西。

第二件事是 Nexus 的消融实验。[73] 当复杂的 RL 与多智能体架构被拆除，仅靠“基础模型 + Lean 反馈”就能解决 Erdős 问题时，它证明了验证器的边际贡献远大于复杂 Harness。两件事情方向相反、结论相同：工程确实主导了当前的上限，而工程里真正值钱的那个部件，是验证器。

13.1 四格设计

H2 可以被一个实验推翻。这个实验长什么样？四格。

第一格，固定 Harness，换模型：基座、SFT、RLVR、蒸馏，使用同样的解码、搜索、验证器与提示。第二格，固定模型，换 Harness：冻结权重，只改搜索预算、验证器类型、工具访问。第三格，匹配算力：报告总推理 FLOPs 与训练 FLOPs，比较帕累托前沿。第四格，估计覆盖度：在分层子集上用超大 $k$ 采样（1024–4096）加形式/工具验证器，报告“至少一次成功”的题目比例与置信区间。

四个格子合起来，给出一张可比较的归因表。H2 成立与否，取决于“覆盖度增量”能否解释总增量的大部分。

13.2 统计功效与预注册

这个设计需要预注册。主终点： $\Delta\mathrm{Cov}$ 与 $\Delta A_{64}$ 的比值。样本量：每个格子至少 500 题；检测 5 个百分点的覆盖度差异需要约 1,570 题每臂；可行时用配对设计降低方差。阈值：若 $\Delta\mathrm{Cov}$ 解释 $\Delta A_{64}$ 的 50% 以上，且在两个模型族复现，H2 被推翻；低于 20%，H2 被支持。失败处理：若置信区间跨越阈值，结论为“证据不足”，而非“支持 H2”。

13.3 什么能推翻 H2

H2 不是不可证伪的。它被以下任一条推翻：

固定 Harness、匹配算力，某权重层干预带来的覆盖度上升能解释基准增益的 50% 以上；
在 MATH-Beyond 这类“基座在 pass@1024 下解不出”的集合上，某方法稳定地把 pass@1 从接近 0 提到可观水平，且不依赖外部数据或更强教师；
形式证明器在未见过的研究级定理上，稳定地证出基座模型在任何预算下都证不出的结果；
一个极简基座模型，在没有硬验证器反馈的情况下，仅凭内部表征生成人类未曾设想、且经得起 Lean 核验的新数学结构。

第三条在 2026 年 10 月之后已被部分触碰——Nexus 的 9 道 Erdős 问题正是“形式证明器证出研究级定理”的实例。[73] 这是否构成 H2 的反例？细读之下未必：Nexus 的成功依赖 Lean 这一硬验证器，而验证器属于 Harness 的一侧。它的消融实验削弱的是“复杂架构不可或缺”，而非“工程主导”。H2 的真正对手，不是任何一套更强的工程，而是那个不借外物、自己长出新数学的模型。 它还没有出现。First Proof 的 1/10 告诉我们：它甚至没有接近出现。

13.4 四个替代解释

一篇综述的立场，应当经得起替代解释的检验。

A1 能力优先。 “架构与规模终将主导。” 回应：可能。但这是经验主张，第 13.1 节的四格设计能够判定。最强的架构结果恰恰是可能扩张覆盖度的那一类；如果它们确实扩张了覆盖度，H2 失败、能力叙事获胜。那将是进步，不是失败。

A2 基准怀疑。 “所有基准分数都没意义。” 回应：部分同意——这正是我们用 $R/A_k/\mathrm{Cov}$ 替换“分数”的原因。First Proof 表明连“基准”这个概念都在进化：盲测难题不是基准，是考场。

A3 归因不可证伪。 “你总可以把解释不了的增益叫诱出。” 回应：H2 是定量的，有明确的否决条件（第 13.3 节）。不可否决的立场，不值得写进综述。

A4 综述不该有立场。 回应：本文的立场是“测量优先”，不是“诱出优先”。它主张的是：在覆盖度被估计之前，任何能力叙事都只是叙事。这个立场可以被数据推翻。

14. 灯塔：十二个问题、十二条预测、一张地图

灯塔不提供答案，它只让后来者知道礁石在哪里。

14.1 十二个问题

覆盖度怎么估？ 大 $k$ 采样给下界，形式验证给局部真值；两者如何拼接？
验证器的可靠性怎么度量？ 假阳性、假阴性、可利用性，能否形成一个统一指标？
过程验证器的分布外退化有多快？ 是否快于结果验证器？
架构改变的是覆盖度还是可靠度？ 循环深度、位置编码、高阶注意力，各自落在哪一轴？
RLVR 的选择器是什么？ 奖励正确性、优化器偏置、熵正则、格式修正，四者如何分离？
搜索的有效样本数怎么定义？ 前缀共享、束搜索相关、智能体并发，能否给出可估计的 $k_{\text{eff}}$ ？
自我改进的验证器瓶颈能否被绕过？ 形式化与代码执行之外，还有第三条可靠闭环吗？
形式化的保真度怎么测？ 自动形式化的语义等价，能否有独立的判定标准？
评测污染能否被动态监测？ 时间戳、模板扰动、盲测题集，能否成为标准配置？
数学创造能否被评测？ 猜想、反例、类比，是否存在不依赖专家的事后判据？
证明消化不良如何量化？ 人类吸收 AI 证明的速度与 AI 生成速度的剪刀差，是否存在数学上的极限？“可消化性”能否成为一个可测量的指标？
系统级智能的算力边界在哪里？ 昂贵系统（如 ProofCouncil）解出的题，是否算作“AI 的数学能力”？若算，价格应当如何计入测量？

14.2 十二条可证伪预测

#	预测	数据与检验	阈值	失败后如何收缩
1	指标伪影能解释部分“涌现”	同一批输出换连续指标（NLL、Brier、编辑距离）	exact-match/NLL 最大斜率比 > 3，且 NLL 无折点	若比 < 1.5，该例不适用指标解释
2	$p^n$ 乘性零假设能预测 pass@ $k$	分步正确率 + $k\in\{1,\dots,64\}$	留出 $k=128,256$ 相对误差 < 20%	若 > 40%，存在强步骤依赖或机制改变
3	RLVR 不创造基座中不存在的路径	基座 $k=1024$ 每题通过率	基座上界 < $10^{-3}$ 的题类上，RL 后 pass@1 涨 >5pp 且 $k=1024$ 上界仍 <5%	若增益只出现在基座可解题类，“仅放大”成立
4	搜索参数只有 $q_{\text{eff}}$ 与 $k_{\text{eff}}$ 可识别	多预算曲线	留出预算误差 < 20%	若 > 40%，参数化仅描述性
5	熵坍缩下尾/头 pass@ $k$ 比下降	头尾分层、预算控制	下降 > 10%，bootstrap 置信区间不含 0	若不降，“尾部侵蚀”不成立
6	70B+/MoE 仍保留螺旋/时钟类算术结构	大规模探针 + 消融	螺旋拟合 $R^2$ 与 8B 差 < 0.1，角峰一致	若消失，机制限于中小稠密模型
7	PRM 增益随验证器可靠性下降	注入噪声的过程标注；算力匹配三组	增益在 $\sigma^\ast\in(0.2,0.4)$ 过零	若 $\sigma=0.5$ 仍为正，可靠性不是约束
8	固定 Harness 后架构差距显著收缩	同 Harness、不同架构、算力匹配	差距收缩 > 50%	若稳定，架构有独立效应
9	评分细则验证器优于答案验证器	高考子集，两种验证器驱动搜索	步骤分题增益 > 5pp	若不显著，工程归因削弱
10	AI 辅助的验证端增益 > 发现端增益	已验证证明 / 被采纳新猜想比率	验证–发现比率上升	若发现比率显著上升，命题 A 削弱
11	无形式验证的 L5 生成将遭遇信任破产	追踪 722 篇手稿的同行评审通过率	1 年内无形式化背书的手稿被顶刊接受率 < 1%	若接受率 > 5%，人类验证器带宽高于本文估计
12	“基础模型 + 硬验证器”在单位算力上击败“复杂 RL 架构”	对比 Nexus 极简版与复杂版在新猜想上的算力效率	极简版单位算力解出率 > 复杂版 2 倍	若复杂版反超，架构组件的价值需重新评估

14.3 一张地图

如果要把这份综述变成一个研究纲领，顺序大致是三段。

第一段，修仪器。 把 $R$ 、 $A_k$ 、 $\mathrm{Cov}$ 作为标准报告项；把验证器可靠性、污染检测、置信区间写进评测协议；在 L4/L5 层，把形式化验证设为强制门槛。没有这一层，后面的争论都只是修辞。

第二段，做归因。 用算力匹配的四格设计，分离模型、Harness、评测三个来源。这一层会产出真正有争议的结果——而这正是科学开始的地方。

第三段，找闭环。 在验证器可靠的角落（形式化、代码执行、符号计算）做自我改进，在验证器不可靠的角落（开放证明、数学创造）保持克制。Nexus 与 Ghys 猜想已经示范了闭环长什么样；722 篇手稿示范了没有闭环会变成什么样。这一层将决定 AI 对数学的长期影响——也决定数学共同体对 AI 的长期态度。

14.4 Math for AI：四个可证伪命题

归因问题不止于基准。我们给出四个关于 AI 对数学实践影响的命题，各附证据与否证条件。

命题 A（验证生产不对称）。 当前 AI 对数学实践的可测影响，集中在验证已有主张，而非生成有价值的新主张。证据：形式验证与证明检查进展快；猜想生成与反例搜索仍弱；最强的“发现”结果多来自带验证器的程序搜索或人机协作，而非无辅助生成。[19][6][49][68] 否证：AI 辅助下，被数学家或形式库接受的新猜想/引理，与已验证既有主张的比率持续上升。

命题 B（Harness 可分离性）。 H2 对研究级数学同样成立：AI 辅助报告的增益由 Harness 主导，而非模型层面的能力扩张。证据：ProofCouncil 在 First Proof 上的成功是“工作台 + 智能体 + 工具”的组合，模型的边际贡献未被隔离；[78] Nexus 的消融实验则显示复杂架构可被拆除。[73] 否证：一个模型在最小 Harness 下解出任何基座模型在任何采样预算下都解不出的一类问题。

命题 C（定义瓶颈）。 自动形式化的主要瓶颈是定义与陈述的形式化，而非证明搜索。证据：形式基准需要大量人工形式化；FormalMATH 报告自然语言提示反而降低形式证明成功率。[49] 否证：一个系统在没有人工定义的情况下关闭大部分非形式—形式差距。

命题 D（过程信号 OOD 脆弱）。 过程奖励模型的分布外退化快于结果验证器。证据：PRM 改善分布内步骤准确率，但过程标注昂贵且模型依赖；奖励过度优化是已知失效模式。[28] 否证：一个 PRM 的 OOD 退化曲线，与分布内准确率匹配的结果验证器相比，不更陡。

15. 结语：试金石、基础设施与人类尊严

回到开头那几个数字，以及 2026 年秋天那场席卷数学界的风暴。

MATH-500 的九十分，FrontierMath 的 97.6%，722 篇手稿与 3 篇撤稿，Nexus 的 9 道 Erdős 悬案，Ghys 猜想的三十余年——它们并不矛盾。它们只是提醒我们：数学不是一个分数，而是一座五层的塔；塔的最上面一层，住着的不是计算，而是理解。

这个秋天把一件事说得再清楚不过：机器生成证明的速度，已经超过了人类理解证明的速度。 陶哲轩称之为“消化不良”；27 位菲尔兹奖得主的联名信，则是这个共同体对“智能本质”的捍卫。[77][75] 他们拒绝接受一个只有可达度而没有理解的黑盒——不是因为他们惧怕机器，而是因为他们知道，数学的终点从来不是“命题被证实”，而是“真理被看见”。一份没有人读得懂的证明，在逻辑上成立，在数学上未完成。

但同一个秋天也给出了希望的具体形状。Nexus 证明：当验证器足够硬，机器的证明可以干净、可核验、可消化；Ghys 猜想证明：当人类直觉被系统性地接入机器回路，最困难的猜想也会在“7 批推演、389 个节点”的协同中倒下。[73][76] 这两条道路有一个共同点：它们都不炫耀速度，它们交付信任。

数学是试金石：它让我们看见模型到底会不会。数学也是基础设施：形式化、验证、搜索、工具——这些在数学上被磨出来的东西，终将流向代码、科学与工程。而数学还有第三重身份：它是矿脉，里面已经有真金——Erdős #848 的那个关键想法，是模型给人类数学家的礼物。[68]

Mathematics is all we want. 我们要的不是用一万个智能体在 88 小时内堆砌出的、带着符号错误的手稿，而是榨干这座矿——知道油在哪里、井打多深、最后一滴留给谁。我们想要的，不是更高的分数，而是知道分数从哪里来；不是更多的证明，而是值得被人类读懂的证明。

在机器的算力海啸面前，人类数学家的思考依然不可替代——这不是安慰，而是测量：所有我们拥有的可靠验证器，归根结底，都是由人设计、由人理解、由人承担的。塔的第五层，灯光尚未照到。那里是人类与机器共同的工地。

附录 A：检索式与筛选流程（可复现）

来源：Google Scholar、ACM Digital Library、IEEE Xplore、ScienceDirect、arXiv。 时间窗：2017-01 至 2026-10-18。 检索块：

任务：mathematical reasoning OR math word problem OR theorem proving OR autoformalization OR Lean OR Isabelle OR AIME OR MATH OR OlympiadBench OR FrontierMath OR PutnamBench
模型：large language model OR LLM OR chain-of-thought OR reinforcement learning OR RLVR OR verifiable reward OR process reward OR test-time compute OR search
评价：benchmark OR evaluation OR emergent ability OR coverage OR pass@k OR contamination OR self-improvement OR scaling law 流程：初检约 1,400 → 去重约 620 → 标题摘要约 260 → 全文/元数据核验 196。 时效性扫描：对 2026 年 9–10 月单独检索 2609.*、2610.* 与会议/期刊 2026 论文，补入 MATH-Beyond、SOAR、On-Policy Warmup、T-Router、AlphaProof Nexus（Science）、OpenAI 722 手稿报告、Ghys 猜想（Intern-S2）、First Proof 等。

附录 B：证据分级速查

等级	含义	本文用法
E1/S3	数学推导、可复算	命题 1/2，作为定理陈述
E3/S1/R0	单团队因果干预	机制证据，标“局部”
E4/S2/R1	多团队系统测量	可写入摘要，如大 $k$ 现象
E2/S1/R0	单团队观察	标“据报道”
E2/S1/R2	已出现失败/撤回	722 篇手稿，作为反面证据使用

附录 C：术语桥

pass@ $k$ ： $k$ 次独立采样至少一次正确的概率；无偏估计量 $1-\binom{N-c}{k}/\binom{N}{k}$ 。
RLVR：可验证奖励强化学习，通常用结果级 0/1 奖励。
PRM：过程奖励模型，给中间步骤打分。
Harness：基座权重之外的一切：解码、搜索、验证器、工具、提示、训练调度。
覆盖度：至少存在一条正确路径的题目比例。
$k_{\mathrm{eff}}$ ：非 iid 搜索的有效独立样本数， $k/[1+(k-1)\rho]$ 。
证明消化不良（proof indigestion）：AI 生成证明的速度超过人类验证与吸收速度的状态（Tao, 2026）。

参考文献

按正文首次引用顺序编号。完整文献库（196 条）与五源核验记录见 survey/bibliography.md 与 survey/refs_five_sources.md。

[1] Hendrycks, Burns, Kadavath et al. Measuring Mathematical Problem Solving With the MATH Dataset. NeurIPS 2021. 正式. arXiv:2103.03874. https://arxiv.org/abs/2103.03874 [2] Glazer, Erdil, Besiroglu et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI. arXiv 2024. 预印本. arXiv:2411.04872. https://arxiv.org/abs/2411.04872 [3] Zheng, D., von Glehn, I., Zwols, Y., et al. AI co-mathematician: Accelerating mathematicians with agentic AI. arXiv 2026. 预印本. arXiv:2605.06651. https://arxiv.org/abs/2605.06651 [4] An, S., Cai, X., Cao, X., et al. AMO-Bench: Large Language Models Still Struggle in High School Math Competitions. ACL 2026 (Findings). 正式. ACL:2026.findings-acl.101；arXiv:2510.26768. https://aclanthology.org/2026.findings-acl.101/ [5] Mayilvahanan, P., Dominguez-Olmedo, R., Wiedemer, T., Brendel, W. MATH-Beyond: A Benchmark for RL to Expand Beyond the Base Model. ICLR 2026. 正式. arXiv:2510.11653. https://arxiv.org/abs/2510.11653 [6] Hubert, Mehta, Sartran et al. Olympiad-level formal mathematical reasoning with reinforcement learning（AlphaProof）. Nature 651:607–613, 2026（online 2025-11）. 正式. DOI:10.1038/s41586-025-09833-y. [7] Haiming Wang, Mert Unsal, Xiaohan Lin, et al. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv 2025. 预印本. arXiv:2504.11354. https://arxiv.org/abs/2504.11354 [8] Chen, J., Chen, W., Du, J., et al. Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience. arXiv 2025. 预印本. arXiv:2512.17260. https://arxiv.org/abs/2512.17260 [9] Plaat, Wong, Verberne et al. Multi-Step Reasoning with Large Language Models, a Survey. ACM Computing Surveys, 2025. 正式. arXiv:2407.11511. https://arxiv.org/abs/2407.11511 [10] Liu, W., Hu, H., Zhou, J., et al. Mathematical Language Models: A Survey. ACM Computing Surveys 58(6):1-37, 2026. 正式. DOI:10.1145/3773985. https://doi.org/10.1145/3773985 [11] Zhang, D., Wang, L., Zhang, L., Dai, B. T., Shen, H. T. The Gap of Semantic Parsing: A Survey on Automatic Math Word Problem Solvers. IEEE TPAMI 42(9), 2020. 正式. DOI:10.1109/TPAMI.2019.2914054. https://doi.org/10.1109/TPAMI.2019.2914054 [12] Chu, Chen, Chen et al. Navigate through Enigmatic Labyrinth: A Survey of Chain of Thought Reasoning. ACL 2024. 正式. arXiv:2309.15402. https://arxiv.org/abs/2309.15402 [13] Chen, Tworek, Jun et al. Evaluating Large Language Models Trained on Code（HumanEval / pass@k）. arXiv 2021. 预印本. arXiv:2107.03374. https://arxiv.org/abs/2107.03374 [14] Kantamneni, Tegmark. Language Models Use Trigonometry to Do Addition. arXiv 2025. 预印本. arXiv:2502.00873. https://arxiv.org/abs/2502.00873 [15] Nikankin, Reusch, Mueller et al. Arithmetic Without Algorithms: Language Models Solve Math With a Bag of Heuristics. arXiv v2（2025）. 预印本. arXiv:2410.21272. https://arxiv.org/abs/2410.21272 [16] Wen, Zhu, Huang et al. The Shape of Addition: Geometric Structures of Arithmetic in Large Language Models. ICML 2026. 正式. arXiv:2606.03645. https://arxiv.org/abs/2606.03645 [17] Mirzadeh, Alizadeh-Vahid, Shahrokhi et al. GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. ICLR 2025. 正式. arXiv:2410.05229. [18] Leonardo de Moura, Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. CADE-28 (LNCS 12699), 2021. 正式. DOI:10.1007/978-3-030-79876-5_37. [19] Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, et al. Mathematical discoveries from program search with large language models（FunSearch）. Nature 625: 468–475, 2024. 正式. DOI 10.1038/s41586-023-06924-6. [20] Zhong, Liu, Tegmark et al. The Clock and the Pizza: Two Stories in Mechanistic Explanation of Neural Networks. NeurIPS 2023. 正式. DOI:10.52202/075280-1186. [21] Yue, Chen, Lu et al. Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?. NeurIPS 2025. 正式. arXiv:2504.13837. [22] Merrill, W., Sabharwal, A. The Parallelism Tradeoff: Limitations of Log-Precision Transformers. TACL 2023. 正式. arXiv:2207.00729. https://arxiv.org/abs/2207.00729 [23] Merrill, W., Sabharwal, A., Smith, N. A. Saturated Transformers are Constant-Depth Threshold Circuits. TACL 2022. 正式. arXiv:2106.16213. https://arxiv.org/abs/2106.16213 [24] Wei, Wang, Schuurmans et al. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. NeurIPS 2022. 正式. arXiv:2201.11903. https://arxiv.org/abs/2201.11903 [25] Kazemnejad, A., Padhi, I., Ramamurthy, K. N., Das, P., Reddy, S. The Impact of Positional Encoding on Length Generalization in Transformers. NeurIPS 2023. 正式. arXiv:2305.19466. https://arxiv.org/abs/2305.19466 [26] Lightman, Kosaraju, Burda et al. Let's Verify Step by Step. ICLR 2024. 正式. arXiv:2305.20050. https://arxiv.org/abs/2305.20050 [27] Wang, Li, Shao et al. Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations. ACL 2024. 正式. arXiv:2312.08935. [28] Gao, Schulman, Hilton. Scaling Laws for Reward Model Overoptimization. ICML 2023. 正式. arXiv:2210.10760. https://arxiv.org/abs/2210.10760 [29] Ma, L., Dai, J., Li, J., Mi, L. T-Router: Learning Thalamic Routing for Reasoning with Parameter-Efficient Reinforcement Learning. arXiv 2026. 预印本. arXiv:2609.39109. https://arxiv.org/abs/2609.39109 [30] Geiping, J., McLeish, S., Jain, N., et al. Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approach. arXiv 2025. 预印本. arXiv:2502.05171. https://arxiv.org/abs/2502.05171 [31] Zhu, R.-J., Wang, Z., Hua, K., et al. Scaling Latent Reasoning via Looped Language Models. arXiv 2025. 预印本. arXiv:2510.25741. https://arxiv.org/abs/2510.25741 [32] Fu, T., You, Y., Chen, Z., Dai, G., Yang, H., Wang, Y. Think-at-Hard: Dynamic Looped Transformers for Improved Reasoning. ICML 2026. 正式. arXiv:2511.08577. https://arxiv.org/abs/2511.08577 [33] Balunovic, Dekoninck, Petrov et al. MathArena: Evaluating LLMs on Uncontaminated Math Competitions. NeurIPS 2025 (D&B). 正式. DOI:10.52202/085713-0679. [34] Deng, Zhao, Tang et al. Investigating Data Contamination in Modern Benchmarks for Large Language Models. NAACL 2024. 正式. 2024.naacl-long.482. [35] Chen, H., Zhu, C., Han, K., et al. Nexus: Higher-Order Attention Mechanisms in Transformers. arXiv 2025. 预印本. arXiv:2512.03377. https://arxiv.org/abs/2512.03377 [36] Guo, Yang, Zhang et al. DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning. Nature 645:633–638, 2025. 正式. arXiv:2501.12948. [37] Shao, Wang, Zhu et al. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv 2024. 预印本. arXiv:2402.03300. https://arxiv.org/abs/2402.03300 [38] Wen, Liu, Zheng et al. Reinforcement Learning with Verifiable Rewards Implicitly Incentivizes Correct Reasoning in Base LLMs. arXiv 2025. 预印本. arXiv:2506.14245. https://arxiv.org/abs/2506.14245 [39] Shao, Li, Xin et al. Spurious Rewards: Rethinking Training Signals in RLVR. ICML 2026 (Poster). 正式. arXiv:2506.10947. https://arxiv.org/abs/2506.10947 [40] Wang, Yang, Zeng et al. Reinforcement Learning for Reasoning in Large Language Models with One Training Example. NeurIPS 2025. 正式. arXiv:2504.20571. https://arxiv.org/abs/2504.20571 [41] Sundaram, S., Quan, J., Kwiatkowski, A., Ahuja, K., Ollivier, Y., Kempe, J. Teaching Models to Teach Themselves: Reasoning at the Edge of Learnability. ICML 2026. 正式. arXiv:2601.18778. https://arxiv.org/abs/2601.18778 [42] Qiao, Y., He, T., Liu, L., et al. From Imitation to Reward Discovery: On-Policy Warmup for Agentic RL. arXiv 2026. 预印本. arXiv:2609.39436. https://arxiv.org/abs/2609.39436 [43] Tan, Geng, Yu et al. Scaling Behaviors of LLM Reinforcement Learning Post-Training: An Empirical Study in Mathematical Reasoning. ACL 2026. 正式. ACL:2026.acl-long.1444. [44] Liu, Diao, Lu et al. ProRL: Prolonged Reinforcement Learning Expands Reasoning Boundaries in Large Language Models. arXiv 2025. 预印本. arXiv:2505.24864. https://arxiv.org/abs/2505.24864 [45] Hao, Wang, Liu et al. Rethinking Entropy Interventions in RLVR: An Entropy Change Perspective（STEER）. ACL 2026（Outstanding Paper）. 正式. ACL:2026.acl-long.1436. [46] Zheng, Zhang, Zhang et al. ProcessBench: Identifying Process Errors in Mathematical Reasoning. ACL 2025. 正式. arXiv:2412.06559. https://arxiv.org/abs/2412.06559 [47] Zheng, Han, Polu. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR 2022. 正式. arXiv:2109.00110. https://arxiv.org/abs/2109.00110 [48] Feng, J., Huang, S., Qu, X., et al. ReTool: Reinforcement Learning for Strategic Tool Use in LLMs. ICLR 2026. 正式. arXiv:2504.11536. https://arxiv.org/abs/2504.11536 [49] Yu, Peng, Ding et al. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. arXiv 2025. 预印本. arXiv:2505.02735. https://arxiv.org/abs/2505.02735 [50] Snell, Lee, Xu, Kumar. Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters. ICLR 2025. 正式. arXiv:2408.03314. [51] Muennighoff, Yang, Shi et al. s1: Simple test-time scaling. arXiv 2025. 预印本. arXiv:2501.19393. https://arxiv.org/abs/2501.19393 [52] Brown, Juravsky, Ehrlich et al. Large Language Monkeys: Scaling Inference Compute with Repeated Sampling. arXiv 2024. 预印本. arXiv:2407.21787. https://arxiv.org/abs/2407.21787 [53] Guan, Zhang, Liu et al. rStar-Math: Small LLMs Can Master Math Reasoning with Self-Evolved Deep Thinking. arXiv 2025. 预印本. arXiv:2501.04519. https://arxiv.org/abs/2501.04519 [54] Shojaee, Mirzadeh, Alizadeh et al. The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity. NeurIPS 2025. 正式. arXiv:2506.06941. https://arxiv.org/abs/2506.06941 [55] Zelikman, Wu, Mu et al. STaR: Bootstrapping Reasoning With Reasoning. NeurIPS 2022. 正式. arXiv:2203.14465. https://arxiv.org/abs/2203.14465 [56] Zhao, Wu, Yue et al. Absolute Zero: Reinforced Self-play Reasoning with Zero Data. NeurIPS 2025（Spotlight）. 正式. arXiv:2505.03335. https://arxiv.org/abs/2505.03335 [57] Huang, Yu, Wang et al. R-Zero: Self-Evolving Reasoning LLM from Zero Data. arXiv 2025（v4 2026）. 预印本. arXiv:2508.05004. https://arxiv.org/abs/2508.05004 [58] Huang, Chen, Mishra et al. Large Language Models Cannot Self-Correct Reasoning Yet. ICLR 2024. 正式. arXiv:2310.01798. https://arxiv.org/abs/2310.01798 [59] Feng, Dohmatob, Yang et al. Beyond Model Collapse: Scaling Up with Synthesized Data Requires Verification. arXiv 2024. 预印本. arXiv:2406.07515. https://arxiv.org/abs/2406.07515 [60] Ye, Huang, Xiao et al. LIMO: Less is More for Reasoning. COLM 2025. 正式. arXiv:2502.03387. https://arxiv.org/abs/2502.03387 [61] Bledsoe, W. W. Non-resolution theorem proving. Artificial Intelligence 9(1), 1977. 正式. DOI:10.1016/0004-3702(77)90012-1. [62] Melis, E., Siekmann, J. Knowledge-based proof planning. Artificial Intelligence 115, 1999. 正式. DOI:10.1016/S0004-3702(99)00076-4. [63] Ringer, T., Palmskog, K., Sergey, I., Gligoric, M., Tatlock, Z. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages 5(2-3), 2019. 正式. DOI:10.1561/2500000045. [64] White, Dooley, Roberts et al. LiveBench: A Challenging, Contamination-Limited LLM Benchmark. ICLR 2025 (Spotlight). 正式. arXiv:2406.19314. https://arxiv.org/abs/2406.19314 [65] Mizrahi, Kaplan, Malkin et al. State of What Art? A Call for Multi-Prompt LLM Evaluation. TACL 2024. 正式. arXiv:2401.00595. https://arxiv.org/abs/2401.00595 [66] Reuel, Hardy, Smith et al. BetterBench: Assessing AI Benchmarks, Uncovering Issues, and Establishing Best Practices. NeurIPS 2024. 正式. arXiv:2411.12990. https://arxiv.org/abs/2411.12990 [67] Miller. Adding Error Bars to Evals: A Statistical Approach to Language Model Evaluations. arXiv 2024. 预印本. arXiv:2411.00640. https://arxiv.org/abs/2411.00640 [68] OpenAI. Early experiments in accelerating science with GPT-5. OpenAI 官方报告，2025-11. 技术报告. 记录 GPT-5 Pro 协助完成 Erdős 问题 #848 证明（Sawhney & Sellke）、在线算法竞争比新下界（Coester）等人机协作发现。https://openai.com/index/accelerating-science-gpt-5/ [69] Epoch AI. FrontierMath benchmark results（GPT-5.2: Tiers 1–3, 40.3%, with tools）. 2026 年检索. 第三方测量. https://epoch.ai/benchmarks/frontiermath [70] Artificial Analysis. Claude Opus 4.5: AIME 2025 91.3%；Math Index. 2026 年检索. 第三方测量. https://artificialanalysis.ai/ [71] Baherwani, Goldstein, Panda. Semantically empty filler tokens improve reasoning; off-CoT satisfaction of hidden constraints in Claude Opus 4.5. arXiv 2026. 预印本. arXiv:2607.22925. https://arxiv.org/abs/2607.22925 [72] OpenAI. 722 Mathematical Manuscripts: A Scale-Compute Approach to Open Problems. OpenAI Technical Report, 2026-10-06（含 10-07 符号错误撤稿声明）. 技术报告. https://openai.com/research/722-manuscripts [73] Hubert, Mehta, Sartran et al. AlphaProof Nexus: Solving 56-Year-Old Erdős Problems via Minimalist Model-Compiler Feedback. Science, 2026-10-08. 正式. DOI:10.1126/science.adx9932. [74] OpenAI. GPT-6 Astra System Card. OpenAI, 2026-09-03. 技术报告. [75] Kontsevich, M., Tao, T., Scholze, P., et al. Severe Misalignment of AI in Mathematics: An Open Letter by 27 Fields Medalists. AHM Press, 2026-09-25. 公开信. [76] Xu, D., Dong, B., Liu, R., et al. Proving the 3D Ghys Conjecture via Intern-S2 and Human-Machine Synergy. arXiv 2026. 预印本. arXiv:2610.08841. https://arxiv.org/abs/2610.08841 [77] Tao, T. Proof Indigestion: The Bottleneck of Mathematical Absorption in the AI Era. Plenary Talk, ICM 2026 & Blog Post, 2026-08. [78] Sikora, A., et al. First Proof: Blind Evaluation of AI on Unpublished Research-Level Mathematics. Harvard/UBuffalo Report, 2026-10. 独立评测.

摘要