为非形式化定理证明学习带洞察的推理

尽管大多数自​​动化定理证明方法都依赖于形式化证明系统，但非正式定理证明可以更好地与大语言模型 (LLM) 在自然语言处理方面的优势保持一致。在这项工作中，我们发现非正式定理证明的主要瓶颈是缺乏洞察力，即难以识别解决复杂问题所需的核心技术。为了解决这个问题，我们提出了一个新颖的框架，旨在培养这种基本的推理技能，并使大语言模型能够进行富有洞察力的推理。我们提出 $\mathtt{DeepInsightTheorem}$，一个分层数据集，通过显式提取核心技术和证明草图以及最终证明来构建非正式证明。为了充分利用该数据集，我们设计了一种模仿人类学习过程的渐进式多阶段 SFT 策略，指导模型从基本的证明写作到富有洞察力的思考。我们对具有挑战性的数学基准的实验表明，这种具有洞察力的生成策略显着优于基线。这些结果表明，识别和应用核心技术的教学模型可以极大地提高他们的数学推理能力。