教 AI 做数学题，关键不是算得快，而是"看穿"题目
> *Learning to Reason with Insight for Informal Theorem Proving* > Yunhe Li, Hao Shi 等 | arXiv: 2604.16278 | 2026
---
一个数学老师的观察
你有没有注意过，数学好的学生和数学一般的学生，差别到底在哪里？
不是计算速度。不是公式背得多。而是——看到一道题，能不能一眼看出该用什么方法。
比如看到一道积分题，高手立刻想到"换元法"，而新手可能要试好几种方法才能碰对。这个"一眼看出"的能力，数学上叫洞察力（Insight）。
这篇论文的作者们发现，大语言模型在做数学证明时，缺的恰恰就是这个东西。
---
形式化 vs 非形式化
目前的自动定理证明主要有两条路线。
一条是形式化证明：用 Coq、Lean、Isabelle 这些专门的证明助手，每一步都必须严格无误。好处是绝对可靠，坏处是门槛极高——你需要把自然语言翻译成形式语言，这个过程本身就很难。
另一条是非形式化证明：直接让 LLM 用自然语言写证明过程，就像数学家在草稿纸上推导一样。好处是门槛低，能利用 LLM 的语言能力；坏处是容易出错，而且模型经常"看似在证明，其实在胡说"。
这篇论文走的是非形式化路线，但他们发现了一个关键瓶颈：模型缺乏洞察力。它能写出证明的步骤，但不知道该用哪个核心技巧来解决问题。
---
DeepInsightTheorem：教模型"看穿"题目
研究者们构建了一个叫 DeepInsightTheorem 的层次化数据集。这个数据集的结构很巧妙——每个证明样本不只是"题目+答案"，而是分成了三个层次：
1. 核心技术（Core Technique）：解决这道题需要的关键方法是什么？比如"数学归纳法"、"反证法"、"构造法"。 2. 证明草图（Proof Sketch）：用几句话概括证明的大致思路，不涉及具体细节。 3. 完整证明（Full Proof）：详细的证明过程。
这种层次化结构模仿了人类数学家的思维过程：先识别方法，再规划路线，最后填充细节。
---
渐进式训练：从学徒到大师
有了数据集，怎么用？研究者设计了一种渐进式多阶段 SFT 策略，模仿人类学习数学的过程：
- 第一阶段：只训练基础证明写作能力，让模型学会"把证明写清楚"。
- 第二阶段：加入核心技术识别训练，让模型学会"看出该用什么方法"。
- 第三阶段：综合训练，让模型同时具备洞察力和证明能力。
实验结果表明，这种"洞察感知"的生成策略在多个数学基准上显著优于基线。教会模型识别和应用核心技术，确实能大幅提升数学推理能力。
---
我的思考
这篇论文的思路很朴素但很深刻：AI 做数学题的瓶颈不是"不会算"，而是"看不出"。
这让我想到一个类比：下棋。一个象棋新手可以学会所有规则的走法，但真正让他变强的是"棋感"——看到棋盘就能判断出哪一步最好。数学证明也是一样，知道所有证明技巧不等于会用对技巧。
渐进式训练的设计也很有启发性。我们训练 AI 时经常一股脑把所有数据灌进去，但人类学习从来不是这样的——先打基础，再学方法，最后综合运用。这篇论文证明了，模仿人类的学习节奏，对 AI 也很有效。
---