DeepInsightTheorem：培养大语言模型数学推理中的洞察力

本文提出DeepInsightTheorem框架，旨在解决大语言模型（LLMs）在非形式化数学定理证明中缺乏洞察力的问题。框架通过层次化数据集设计和渐进式多阶段监督微调（SFT）策略，帮助模型识别核心解题技巧、规划证明结构，从而提升数学推理能力。实验表明，该框架在初等数学、竞赛数学及大学数学等多个基准测试中显著优于基线方法，尤其在复杂问题上表现突出。

自动定理证明领域传统依赖形式化系统（如Coq、Isabelle），虽可靠但门槛高、效率低、可读性差。LLMs擅长非形式化证明（自然语言），但核心瓶颈是缺乏洞察力——即识别核心解题技巧的能力。当前LLMs能执行步骤却难以自主选择方法，限制了复杂问题的表现。

框架从数据和训练策略两维度构建：

1. 层次化数据集：含核心技巧标注（如归纳法、反证法）、证明草图（全局框架）、完整证明（细节）三层结构，提供"为什么这样证明"的信号。
2. 渐进式多阶段SFT：四阶段训练：基础证明写作→技巧识别与应用→洞察式思考（先草图后细节）→综合精炼，模仿人类学习过程。
3. 洞察力感知生成策略：推理时先显式选技巧→生成草图→展开细节，提升证明质量与可解释性。

实验覆盖初等、竞赛、大学数学等基准，对比标准SFT、Chain-of-Thought及专用模型：

• 性能提升：所有基准上优于基线，复杂问题提升10%-30%。
• 相关性：技巧识别准确率与证明成功率高度相关；草图质量与证明质量密切相关。
• 泛化能力：跨领域泛化表现优于基线，说明学到元能力。

有效性原因：

• 从模式匹配到策略选择：显式技巧训练让模型学会分析问题选方法。
• 层次化表示降低认知负荷：分全局（草图）与局部（细节）处理。
• 渐进学习符合认知规律：由浅入深构建能力。 核心贡献：将非形式化证明从"执行"提升到"洞察"层次，证明LLMs可超越模式匹配，展现类人数学思维。

局限：数据集规模有限、领域覆盖不足、缺乏形式化验证。 未来方向：自动技巧发现、RL增强、人机协作、形式化-非形式化桥接。 影响：对数学教育（显式教技巧、强调规划）和AI推理（元认知、层次化推理）有启示。