Learning to Reason with Insight for Informal Theorem Proving
For LLM-based theorem proving, this work addresses the bottleneck of recognizing core techniques, enabling more effective mathematical reasoning.
The paper identifies lack of insight as a bottleneck in informal theorem proving with LLMs and proposes DeepInsightTheorem, a hierarchical dataset with core techniques and proof sketches, plus a Progressive Multi-Stage SFT strategy. Experiments show significant improvement over baselines on challenging math benchmarks.
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.