SOTA · 语言与推理

数学

竞赛数学、证明辅助与数值推理

数学是 AGI 讨论里最容易被高估也最容易被低估的域:高估是因为竞赛题分数已经接近人类顶尖,低估是因为「会做题」与「会做研究」之间的鸿沟比分数看起来大得多。它与 AGI 的关系很直接:数学是少数有形式化真值的领域,一个命题可以被机器验证为对或错,于是它同时是能力的标尺和自我改进的候选路径(自动猜想、自动证明、自动形式化)。证明辅助之所以关键,是因为它把「模型说它对」换成「检查器说它对」,这是置信度分级里唯一能天然拿到 A 档的证据形态。梯顶现在有了专门的数学条目:AlphaEvolve(编码代理式进化搜索,唯一一条经一年 Borg 生产验证的结果,持续回收 Google 全球算力 0.7%)、DeepSeek-Prover-V2(MiniF2F-test 88.9%、pass@8192)与 Kimina-Prover(miniF2F 92.2%、TTRL 搜索后)。两条证明器并列不排名:协议不可通约,pass@8192 与 pass@1 也不可比。三条读数都要打折:证明器分数全是厂商自报,没有在 Lean 4 + mathlib 环境复算,而 AlphaEvolve 的「matmul 提速 23%」是特定硬件下的经验读数,与 Lean 通过所代表的数学意义上的对不是一回事。12 个同步第三方榜仍无独立数学榜(AIME、FrontierMath、MathArena 均未接入),这个域的结论请读作方向而非水位。

尺子AIME、FrontierMath、MathArena

SOTA 阶梯

数学科研梯顶B

AlphaEvolve:让模型去优化「有客观评分函数」的问题

Google DeepMind 的编码代理式进化搜索:Gemini Flash 出量、Gemini Pro 出质地提出候选,自动评估器打分,高分候选留进种群当下一轮上下文,本质是 LLM 当变异算子的进化搜索;它只做有自动评估器的优化问题,因此归到 math 与 agents 两域。进化出的调度启发式已在 Google 数据中心(Borg)生产运行超过一年,持续回收 Google 全球算力的 0.7%(口径是 Google 全球算力,不是全人类算力),卡片读数取自它:全部结果里唯一经长期生产验证的一条。另有 matmul kernel 特定规模提速 23%;数学侧在 50 多个开放问题上约 20% 给出改进,含 4x4 复矩阵乘法用 48 次标量乘改进 Strassen 1969 年的 49 次记录。可验证性与证明器不同:Lean 通过是数学意义上的对,「提速 23%」是特定硬件下的经验读数。可用性接近零:无公开权重、Early Access 只有登记表,前提是你写得出便宜、快速、可信的评估器。置信度 B(有争议):Borg 那条经一年生产验证,未复现任何一条。

0.7%Google 全球算力回收(生产验证)有争议 · 2025-05

生产Google DeepMind官网

数学科研梯顶C

DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」

DeepSeek 的形式化定理证明模型:671B MoE 底座(与 DeepSeek-V3 同源)、目标语言 Lean 4,是在旗舰级底座上做形式化对齐。核心创新是冷启动的递归子目标分解:竞赛级命题一步证成功率极低、RL 几无正样本,于是先让 DeepSeek-V3 把命题拆成子目标串,再由 7B 小模型逐个证,合成的完整证明成了训练数据,即用可分解性换数据密度;RL 奖励二元,信号来自 Lean 内核。读数(厂商自报):MiniF2F-test 88.9%(pass@8192)、PutnamBench 49/658(约 7.4%)、自建 ProverBench 325 题。三个数一起读:MiniF2F 在该采样预算下已近饱和,换普特南立刻掉一个数量级;ProverBench 自家题自家跑要打折。公开仓库(约 1304 stars)含证法 ZIP,可直接在 Lean 里跑,可核验性比闭源高一档。边界:pass@8192 意味着八千多个候选再筛,与 pass@1 不可比。与 Kimina-Prover 的 92.2% 协议不可通约,并列收录,不排名。置信度 C(厂商宣称):未在自有 Lean 4 + mathlib 环境复算。

88.9%MiniF2F-test厂商宣称 · 2025-07

研究DeepSeek官网 Repo

数学科研梯顶C

Kimina-Prover:不挂搜索树,靠整证生成 RL 把 miniF2F 推到 92.2%

Moonshot AI 与 Numina 的 Lean 4 定理证明线,立场逆主流:训练与推理均无 prover 中间反馈,不用 MCTS、价值函数与过程奖励模型(arXiv:2504.11354),搜索内化成一次整证生成;Formal Reasoning Pattern 先写结构化自然语言草稿再落 Lean 代码,把稀疏二值奖励重述成语言问题。底座 Qwen2.5-72B、上下文 32K。两代分开读:Preview(2025-04)miniF2F-test 80.7%(pass@8192);72B(2025-07-10)加 TTRL 搜索与错误修复后 92.2%,是收录时最高公开读数,卡片取此数,同口径 pass@1 仅 63.9%。等预算 pass@1/32/1024 为 63.9/84.0/87.7,三档全领先 671B DeepSeek-Prover-V2(61.9/82.4/86.6)。打折:对照表由 Kimina 团队发布、DeepSeek 两行为其复跑;仓库未声明许可证;miniF2F 仅 244 题且已过 92%,区分度在衰减。该域无第三方榜,读数只读作方向。置信度 C(厂商宣称):未在固定 commit 复算。

92.2%miniF2F(TTRL 搜索后)厂商宣称 · 2025-07

研究Moonshot AI(Numina & Kimi)官网 Repo

现在就能用的资产

这个域还没有挂上可直接装用的 skill。

消费它的领域

还没有内容把这个能力归到某个领域。

边界与失败模式

这个域的边界要先说清楚:没有独立数学榜接入,就无法用与其他域同一把尺子给出 confirmed 读数,任何「某模型拿下 AIME 满分」的说法在这里只能记 vendor-claim 或 needs-reproduction。行业层面的失效模式同样清晰。一是竞赛题与研究的断层:题面短、条件完整、答案唯一,这三条把问题裁成了可评测的形状,而真实数学的难点在「问题本身是什么」——提出值得证的命题、找到有用的定义,这部分目前没有尺子,也没有可靠系统。二是数值推理仍然脆:多位数算术、单位换算、金融与工程计算里的量纲一致性,大模型出错的方式很安静,不给出不确定度,只在下游被发现。三是形式化的成本结构没变:把一段证明写成 Lean/Isabelle 可检查的形式,目前仍高度依赖人工,自动化只覆盖了骨架与常规步骤,越界的引理仍要人补,所以「机器验证过」的覆盖率远低于外界想象。四是评测泄漏与题源枯竭:AIME 与奥数题库年代久远,新题供给跟不上模型迭代,分数上涨里有多少是能力、多少是见过,现在无法分离——这正是没有榜单就不下结论的原因。成本与延迟:数学推理的成本几乎全在 token 上,一道需要长链验证的题可能消耗数万 token,且推理档位越高越贵;而形式化环节的瓶颈不是算力,是懂 Lean 的人。

作为亚马逊联盟会员,我们可能从符合条件的购买中获得佣金。