前言

数学，长期以来被视为人工智能最难攻克的高地之一。

它高度形式化、符号密集、推理链条漫长，对中间过程的正确性有极高要求——这与大模型擅长的“流畅语言生成”之间，天然存在张力。

也正因为如此，AI 在数学上的每一次实质性突破，往往都不是多答对几道题，而是一次推理范式与系统架构的跃迁。


过去两年里，“AI for Math”从热点概念逐步走向工程现实：

一边是竞赛分数不断被刷新，另一边则是对评测失真、数据污染、不可验证推理的反思不断加深。

本文尝试站在一个长期做教育产品、也深度参与 AI 工程落地的开发者视角，系统梳理当前的阶段下：

  • 主流数学基准的真实可信度发生了哪些变化
  • 大模型数学能力的真实的分层现状
  • 架构型解题系统如何取代单模型刷题
  • 以及哪些方向，才真的值得产品与研究投入

如果你正在做数学相关的 AI 产品，这篇文章就是为你写的。



一、大模型的数学能力：从刷题能力到结构能力

1. 基准测试的真实演进

早期数学能力评测，基本围绕 GSM8K / MATH / AIME 展开。
但到 2025 年，这套体系已经明显出现分化。

GSM8K：接近饱和，且被系统性证明存在污染风险

GSM8K 曾是模型是否真的会算应用题的代表基准，但如何它的问题最多：

  • 题目规模小、公开时间久
  • 与公开解题内容高度重合
  • 已被多篇研究证实存在训练集污染

对照测试（如 GSM1k）显示：同一模型在 GSM8K 上的高分，可能在未污染但同构的题集上直接下降 10%–15%。这是来自多个独立对照实验的一致现象。

AIME / AMC / MATH：仍有价值，但必须标注“新鲜度”

AIME 依然是当前最常用的高中竞赛基准，但今年的共识是：

  • 必须明确题目年份，AIME 2024 与 AIME 2025 难度与污染风险差异明显
  • 必须说明评测口径，是否多次采样、是否允许工具、是否混入旧题

在多个评测平台上，**顶级模型在 AIME 2025 上已接近 100%**。
不过这并不意味着数学被解决了，而只是说明标准竞赛题对顶级模型的区分度正在迅速下降。

新的可信方向：实时竞赛流与反刷榜基准

为解决刷榜幻觉，2025 年开始出现两类新基准：

  • 实时竞赛流（如 MathArena）：只评测最新发布的竞赛题
  • 难题精选（Apex 类）：主动过滤掉对模型过于友好的题

结果是在 IMO 2025 证明题上，顶级模型的完成率仍 **低于 40%**。

在只保留最难题的 Apex 集合上，最好模型也只有**约 5%**。

这两个数字，远比任何 AIME 满分更能反映模型的真实上限。


2. 25 年主流模型的能力分层

第一层：Final Answer（竞赛解题）

在 AIME / AMC 这类任务上，GPT-5.x、Gemini 3 Pro 等模型已接近“刷穿”。

这一层能力对教育产品有价值，但区分度已明显下降。

第二层：Proof Writing（自然语言证明）

IMO 级别证明题仍是硬骨头，模型容易给出看起来合理的证明，但逻辑漏洞频发。人类仍需逐步审查。

这是教学与科研应用的核心瓶颈。

第三层：Formal Proof（形式化证明）

在 Lean / Coq 等系统中，架构型 Prover 已在 PutnamBench 等任务上达到 **80%+**。

不过这里的关键不是模型大小，而是 生成 → 验证 → 失败定位 → 局部修复 的工程闭环。



二、系统架构演进：从思维链到解题架构体

1. Prompt 层的演进

Chain-of-Thought 解决了模型不显式思考的问题，但在数学中，它暴露出三个根本缺陷：

  1. 推理结构隐含在自然语言中，难以校验
  2. 一步出错，后续全部污染
  3. 无法与形式化工具直接对齐

因此，新的主流做法是 Sketch-Proof：

  • 先生成结构草图（目标、引理、分支）
  • 再逐步填充可验证推理

2. 架构型系统成为主流

25 年最有代表性的数学系统，几乎都呈现出相似的形态：

  • 多阶段解题流程
  • 明确的中间表示
  • 外部验证器深度介入

典型模式包括：

  • 题干解析 → 数学意图识别
  • 解题草图生成 → 子问题分解
  • 引理调用 / 工具计算
  • 验证失败 → 局部修复 → 重组

这类系统的成功，更多来自软件工程，而非模型参数规模。



三、正确率保障机制：如何逻辑闭环

1. 形式化验证成为分水岭

在引入 Lean / Coq 后，数学 AI 出现了质变：

  • 每一步推理都必须通过类型检查
  • 模糊语言与跳步被强制消除
  • 错误能被精确定位到具体断言

这使得模型不再糊一整段证明，而是被迫学会结构化思考。


2. 自动修复与过程批判成为核心能力

新一代系统普遍具备：

  • 失败感知：知道哪一步错了
  • 局部重写：只改必要部分
  • 策略调整：而非从头乱试

Process Critic、Verifier-Formalizer 等模块，使模型逐步具备自我审稿能力。


3. 一个成熟的工程级验证链，大致长这样

结构化输出

→ 工具计算校验

→ 形式化断言生成

→ SMT / Symbolic 检查

→ 反馈调度与重试

没有这一整条链，数学 AI 几乎不可能用于严肃场景。



四、应用落地：哪些真的在发生

1. 数学教育

  • 个性化辅导开始强调解题路径而非结论
  • 错题系统不再只存答案，而是存结构失败点
  • AI 批改开始结合符号与逻辑，而非纯语言评分

真正有价值的不是讲得像人，而是哪里错、为什么错、下一步怎么练。


2. 科研与数学内容生产

  • 形式化工具正在重构数学研究流程
  • 老论文被结构化、引理被复用
  • 数学知识开始具备可执行性

AI 在这里真的更像一个极其耐心的研究助理。


3. 给产品开发者的现实建议

  • 标准化解题过程数据
  • 把验证器当一等公民
  • 明确区分：思考模型 / 执行工具 / 检查模块
  • 不要迷信一个模型解决一切


写在最后

AI 在数学中的价值，从来不只是替人做题。

真正重要的，是它是否能帮助我们拆解问题结构，让推理过程可追踪、可检查、可复用。成为人类思考体系的一部分，而不是一个黑箱。

如果说语言模型的早期成功，是“让机器会说话”，那么 AI for Math 的长期目标，应该是让机器学会一步步负责任地思考。

这，可能才是 AI 真正进入教育与基础科学核心地带的开始。







延伸阅读