DeepInsightTheorem: Cultivating Mathematical Insight in LLMs via Hierarchical Reasoning

TL;DR

While LLMs are proficient at "fluent" text generation, they often struggle with the "Aha!" moments required for complex mathematical proofs. This paper argues that the bottleneck is a lack of insight—the inability to identify core techniques early on. By introducing DeepInsightTheorem, a dataset and a multi-stage training curriculum, the authors enable models to first identify high-level strategies (Core Techniques) and structures (Sketches) before attempting the final proof, leading to state-of-the-art performance in informal theorem proving.

The "Entropy Spike" Problem: Why LLMs Fail at Math

In informal theorem proving (using natural language and LaTeX), most reasoning steps are routine. However, every complex proof contains pivotal junctions—like deciding to construct a specific auxiliary function or invoking a non-obvious lemma.

The authors observe that at these junctions, the model's token entropy spikes. In other words, the model becomes highly uncertain because it hasn't "planned" the core technique. If the probability of choosing the right technique is low ($\delta$), the probability of completing a proof with $k$ such techniques drops exponentially (${\delta }^k$).

Figure: Token-level entropy peaks exactly when a core technique (like the Baire Category Theorem) needs to be invoked.

Methodology: DeepInsightTheorem & Progressive SFT

To bridge the gap between a problem statement and its proof, the authors decompose the reasoning process into three layers:

1. Core Techniques: High-level "tools" (e.g., "apply the Pigeonhole Principle").
2. Proof Sketch: A step-by-step roadmap of the argument.
3. Full Proof: The detailed LaTeX execution.

The Human-Centric Curriculum

Simply giving the model all this data at once doesn't work (the "Novice Gap"). Instead, they use a Progressive Multi-Stage SFT:

• Stage 1 (Apprentice): Train on standard $(Q,Proof)$ pairs to build foundational math language skills.
• Stage 2 (Journeyman): Train on $(Q,Sketch,Proof)$ to learn logical planning.
• Stage 3 (Expert): Train on the full $(Q,Techniques,Sketch,Proof)$ hierarchy to cultivate insight.

Experimental Validation

The framework was tested on elite math benchmarks: FIMO (Olympiad-style), PutnamBench, and HMMT.

Key Findings:

• Consistency: Across Qwen and Llama families, the hierarchical approach consistently beat standard SFT.
• Efficiency: The 7B model variant reached performance levels comparable to models trained with much more expensive Reinforcement Learning (RL) methods.
• Small Model Gains: Smaller models (1B-3B) saw a disproportionately large boost, suggesting that "insight-guided thinking" is a way to squeeze more reasoning power out of limited parameters.

Table: Comparison across different model sizes and benchmarks showing the superiority of Three-stage SFT.

Deep Insight: Why It Works

The essence of this work is structural decoupling. By forcing the model to predict techniques first, the authors are essentially training a "fast-and-slow" thinking system. The "Technique Analysis" phase acts as a localized Micro-Chain-of-Thought, reducing the search space for the subsequent sketch and proof.

From an Industry perspective, this proves that for complex tasks, data structure matters as much as data volume. By annotating existing proofs with their underlying "pivotal ideas," we can dramatically increase data efficiency.

Conclusion & Future Outlook

DeepInsightTheorem proves that informal theorem proving is not just about imitation, but about technique recognition. While the authors focus on SFT, the next logical step is naturally Reinforcement Learning—using these core techniques as a search space for Monte Carlo Tree Search (MCTS) or similar planning algorithms.

For practitioners, the takeaway is clear: if your LLM is failing at complex reasoning, don't just give it more examples—give it a map of the core techniques it needs to solve them.