[论文] 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)

# 费曼来信：你是想请个“背公式”的学霸，还是想要一个“一眼看穿”的天才？——聊聊数学证明中的洞察力 读完关于 **Learning to Reason with Insight** 的论文摘要，我脑子里立刻跳出一个关于“审题”的画面。 为了让你明白为什么 AI 做数学证明总是“看似在努力，其实在胡说”，咱们来聊聊“看穿”这件事。 ### 1. 现状：那个在乱麻里“打转”的 AI 目前的非形式化定理证明（直接用自然语言写证明），面临一个尴尬的瓶颈：**缺乏洞察力**。 AI 虽然背熟了所有的引理和定理，但它就像是一个**只会查字典的孩子**。当你给他一道复杂的积分题，他只会机械地尝试各种公式，却不知道那道题背后的“**阵眼**”在哪。这叫 **“盲目搜索”**。 ### 2. DeepInsightTheorem：教 AI “先审题，后动笔” 这项研究最硬核的地方在于，它不再强迫 AI 直接写答案。它构建了一个 **DeepInsightTheorem** 层次化数据集，强迫 AI 按照人类数学家的三步走战略来思考： * **第一步：识别核心技术（Core Technique）**：别急着算！先告诉我，这道题的“命门”是不是“数学归纳法”或者“反证法”？这就是所谓的“一眼看穿”。 * **第二步：画草图（Proof Sketch）**：用几句话勾勒出战术地图。不求细节，只求方向。这叫**“逻辑的骨架”**。 * **第三步：填肉（Full Proof）**：在正确的地图指引下，再去填充那些枯燥的推导细节。 ### 3. 费曼式的判断：理解是“路径的简化” 所谓的“洞察力”，并不是你比别人算得快。 而是**你在面对无穷无尽的可能路径时，能瞬间剔除那 99% 错误的分支，直接锁定通向真相的那根金线。** 这篇论文告诉我们：**AI 的数学能力，不在于它吐出了多少个 Token，而在于它在吐出第一个 Token 之前，是否已经“看穿”了这个问题的物理/逻辑本质。** 当 AI 学会了“先思考核心技术”，它就不再是一个概率预测器，而是一个开始拥有“直觉”的数学学徒。 **带走的启发：** 在解决复杂工程问题时，别急着去写代码。 先去寻找那个**“核心技术（Core Technique）”**。 **如果你不能用一句话说清楚这个问题的“阵眼”在哪，那么你所有的代码堆砌，都只是在概率的迷雾中进行一场昂贵的豪赌。** #MathReasoning #LLM #TheoremProving #DeepInsight #Education #FeynmanLearning #智柴认知实验室🎙️