[Paper] 学习具备洞察的推理用于非形式定理证明

Source: arXiv - 2604.16278v1

概述

本文解决了在使用大型语言模型（LLMs）进行非形式化定理证明时的一个根本障碍：模型往往缺乏洞察——即指导证明的核心技巧或“啊哈”步骤。通过显式教导 LLM 识别并运用这些技巧，作者展示了在解决以自然语言表述的高难度数学问题时，模型性能有了显著提升。

关键贡献

• DeepInsightTheorem 数据集 – 一个层次化的非正式证明集合，将 (1) 核心技术、(2) 简明的 证明概述、以及 (3) 完整的详细证明 分离开来。
• 渐进式多阶段监督微调 (SFT) – 一个课程学习管线，首先在基础证明写作上训练模型，然后在提取核心技术上训练，最后在生成带有洞察感知指导的完整证明上训练。
• 实证验证 – 在已建立的数学推理基准（例如 MATH、MiniF2F）上进行的大量实验表明，洞察感知方法相较于强基线提升了最高 15 % 的绝对准确率。
• 洞察使用分析 – 消融研究显示，显式建模核心技术贡献了大部分性能提升。

方法论

1. 数据集构建

• 人类标注者将每个非形式化定理分解为三层：
  • Technique（技术）: 一个简短短语，例如 “use induction on n”（对 n 进行归纳）或 “apply Cauchy‑Schwarz”（使用柯西‑施瓦茨不等式）。
  • Sketch（草图）: 对技术如何应用的高级概述。
  • Full Proof（完整证明）: 逐步的自然语言证明。
• 该层次结构使模型能够先学习 做什么（what），再学习 如何做（how）。

2. 渐进式多阶段 SFT

• Stage 1 – 证明写作：在原始证明文本上微调基础大语言模型（例如 LLaMA‑2‑7B），以获得基本的数学语言能力。
• Stage 2 – 洞察提取：训练同一模型在给定问题陈述时预测 核心技术。这迫使模型关注高级推理模式。
• Stage 3 – 洞察引导生成：将技术标记与问题结合，让模型生成完整证明，并以先前学习的洞察为条件。
• 这些阶段按顺序执行，类似于人类学生先学习写证明，然后学会发现关键思路，最后写出明确利用该思路的证明。

3. 评估

• 准确率通过与参考证明的完全匹配以及使用验证器（例如符号检查器或独立的大语言模型）的 语义正确性 指标来衡量。
• 基线包括标准微调、思路链提示（chain‑of‑thought prompting）以及检索增强生成。

结果与发现

• 仅使用核心技术预测 就能提升约 7 %，这证实了 insight token 含有大量信息。
• 使用渐进式课程训练的模型收敛更快（约减少 30 % 的训练步数），并表现出更稳定的损失曲线。
• 人类评估显示，带有显式 insight 的证明 更易读，且 更易于理解，相比基线模型生成的证明有明显优势。

实际意义

• Developer tooling：将“洞察提取”模块集成到代码助手或教育机器人中，可以让基于 LLM 的数学辅导更加可靠和透明。
• Automated verification pipelines：通过公开核心技术，下游符号检查器可以专注于验证更小、更明确的子问题，从而降低计算开销。
• Cross‑domain reasoning：层次化方法可以迁移到其他需要高层策略的领域（例如算法设计、安全性证明生成、科学假设形成）。
• Curriculum‑learning APIs：渐进式微调配方足够轻量，可包装为“训练计划”服务，供任何希望在不进行大规模数据收集的情况下提升推理能力的 LLM 提供商使用。

限制与未来工作

• 标注成本 – 构建 DeepInsightTheorem 需要专家数学家对技术和草图进行标注，这可能无法扩展到所有子领域。
• 对新领域的泛化 – 当前数据集聚焦于本科层次的数学；在高级研究层面的证明上的表现仍未经过测试。
• 对模型规模的依赖 – 对于非常小的模型（<2 B 参数），收益会减小，这表明有效洞察学习对模型容量有下限。

未来方向

• 使用弱监督进行半自动技术提取，以减少标注工作量。
• 扩展层次结构以包含反例生成，用于证明调试。
• 探索多模态洞察线索（例如图示），用于几何密集型问题。

结论：通过教会大型语言模型首先识别证明背后的“关键思路”，作者们开启了非正式定理证明性能的新水平——这一方法可以在许多 AI 辅助推理任务中重新利用。

作者

• Yunhe Li
• Hao Shi
• Bowen Deng
• Wei Wang
• Mengzhe Ruan
• Hanxu Hou
• Zhongxiang Dai
• Siyang Gao
• Chao Wang
• Shuang Qiu
• Linqi Song

论文信息

• arXiv ID: 2604.16278v1
• 分类: cs.AI, cs.CL, cs.LG
• 发布于: 2026年4月17日
• PDF: Download PDF