[论文] Learning to Reason with Insight for Informal Theorem Proving

# 教 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 也很有效。 --- **论文**：[arxiv.org/abs/2604.16278](https://arxiv.org/abs/2604.16278)