学习通过洞察进行非形式化定理证明的推理

# 通过洞察学习非形式定理证明的推理

来源: https://arxiv.org/abs/2604.16278
作者: Yunhe Li (https://arxiv.org/search/cs?searchtype=author&query=Li,+Y), Hao Shi (https://arxiv.org/search/cs?searchtype=author&query=Shi,+H), Bowen Deng (https://arxiv.org/search/cs?searchtype=author&query=Deng,+B), Wei Wang (https://arxiv.org/search/cs?searchtype=author&query=Wang,+W), Mengzhe Ruan (https://arxiv.org/search/cs?searchtype=author&query=Ruan,+M), Hanxu Hou (https://arxiv.org/search/cs?searchtype=author&query=Hou,+H), Zhongxiang Dai (https://arxiv.org/search/cs?searchtype=author&query=Dai,+Z), Siyang Gao (https://arxiv.org/search/cs?searchtype=author&query=Gao,+S), Chao Wang (https://arxiv.org/search/cs?searchtype=author&query=Wang,+C), Shuang Qiu (https://arxiv.org/search/cs?searchtype=author&query=Qiu,+S), Linqi Song (https://arxiv.org/search/cs?searchtype=author&query=Song,+L)

查看 PDF (https://arxiv.org/pdf/2604.16278)

> 摘要：虽然大多数自动定理证明方法依赖于形式证明系统，但非形式定理证明能更好地与大型语言模型（LLM）在自然语言处理方面的优势相适应。在这项工作中，我们发现非形式定理证明的主要瓶颈在于缺乏洞察，即难以识别解决复杂问题所需的核心技术。为解决这一问题，我们提出了一个新型框架，旨在培养这一必要的推理能力，使 LLM 能够执行富有洞察的推理。我们提出了 $\mathtt{DeepInsightTheorem}$，这是一个分层数据集，通过显式提取核心技术和证明草图以及最终证明来结构化非形式证明。为了充分利用这个数据集，我们设计了一个渐进式多阶段监督微调（SFT）策略，模拟人类学习过程，引导模型从基础证明编写逐步发展到富有洞察的思维。我们在具有挑战性的数学基准上的实验表明，这种洞察感知生成策略的性能明显优于基准方法。这些结果表明，教导模型识别和应用核心技术可以显著改进其数学推理能力。

## 提交历史

来自: Yunhe Li [查看邮箱 (https://arxiv.org/show-email/b478e370/2604.16278)] **[v1]** 2026 年 4 月 17 日星期五 17:36:21 UTC (3,441 KB)