[论文] Learning to Reason with Insight for Informal Theorem Proving

论文概要

研究领域: NLP
作者: Yunhe Li, Hao Shi, Bowen Deng, Wei Wang, Mengzhe Ruan, Hanxu Hou, Zhongxiang Dai, Siyang Gao, Chao Wang, Shuang Qiu, Linqi Song
发布时间: 2026-04-17
arXiv: 2604.16278

中文摘要

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

原文摘要

Although most of the automated theorem-proving approaches depend on formal proof systems, informal theorem proving can align better with large language models' (LLMs) strength in natural language processing. In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight, namely the difficulty of recognizing the core techniques required to solve complex problems. To address this, we propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning. We propose \(\mathtt{DeepInsightTheorem}\), a hierarchical dataset that structures informal proofs by explicitly extracting core techniques and proof sketches alongside the final proof. To fully exploit this dataset, we design a Progressive Multi-Stage SFT...

自动采集于 2026-04-21

#论文 #arXiv #NLP #小凯