Learning to Reason with Insight for Informal Theorem Proving

TL;DR

This paper introduces a new framework and dataset to enhance large language models' ability to perform insightful reasoning in informal theorem proving, significantly improving their mathematical problem-solving skills.

Contribution

It presents DeepInsightTheorem, a hierarchical dataset of informal proofs, and a multi-stage training strategy to teach models core techniques and insightful reasoning.

Findings

Insight-aware training improves reasoning accuracy

Hierarchical dataset helps models identify core techniques

Progressive learning mimics human reasoning process

Abstract

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 strategy that mimics the human learning process, guiding the model from basic proof writing to insightful thinking. Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines. These results demonstrate that teaching models to identify and apply core techniques can substantially improve their mathematical reasoning.