DeepInsightTheorem: Cultivating Insight in Mathematical Reasoning of Large Language Models

This paper proposes the DeepInsightTheorem framework, aiming to address the lack of insight in large language models (LLMs) for informal mathematical theorem proving. Through hierarchical dataset design and a progressive multi-stage supervised fine-tuning (SFT) strategy, the framework helps models identify core problem-solving techniques and plan proof structures, thereby enhancing their mathematical reasoning ability. Experiments show that this framework significantly outperforms baseline methods on multiple benchmarks including elementary mathematics, competition mathematics, and university mathematics, especially excelling in complex problems.

The field of automated theorem proving traditionally relies on formal systems (e.g., Coq, Isabelle), which are reliable but have high barriers to entry, low efficiency, and poor readability. LLMs excel at informal proofs (natural language), but their core bottleneck is the lack of insight—the ability to identify core problem-solving techniques. Current LLMs can execute steps but struggle to independently choose methods, limiting their performance on complex problems.

The framework is constructed from two dimensions: data and training strategy:

1. Hierarchical Dataset: Contains three layers—core technique annotations (e.g., induction, proof by contradiction), proof sketches (global framework), and complete proofs (details)—providing signals for "why this proof works".
2. Progressive Multi-Stage SFT: Four training stages: basic proof writing → technique recognition and application → insight-based thinking (sketch first, then details) → comprehensive refinement, mimicking the human learning process.
3. Insight-Aware Generation Strategy: During reasoning, explicitly select techniques first → generate a sketch → expand details, improving proof quality and interpretability.

Experiments cover benchmarks in elementary mathematics, competition mathematics, and university mathematics, comparing against standard SFT, Chain-of-Thought, and specialized models:

• Performance Improvement: Outperforms baselines on all benchmarks, with a 10%-30% improvement on complex problems.
• Correlation: The accuracy of technique recognition is highly correlated with proof success rate; sketch quality is closely related to proof quality.
• Generalization Ability: Better cross-domain generalization than baselines, indicating that meta-abilities are learned.

Reasons for effectiveness:

• From pattern matching to strategy selection: Explicit technique training enables models to analyze problems and choose methods.
• Hierarchical representation reduces cognitive load: Separates global (sketch) and local (detail) processing.
• Progressive learning aligns with cognitive laws: Builds abilities from shallow to deep. Core contributions: Elevates informal proof from the "execution" level to the "insight" level, proving that LLMs can go beyond pattern matching and exhibit human-like mathematical thinking.

Limitations: Limited dataset size, insufficient domain coverage, and lack of formal verification. Future Directions: Automatic technique discovery, RL enhancement, human-AI collaboration, and formal-informal bridging. Impacts: Provides insights for mathematics education (explicitly teaching techniques, emphasizing planning) and AI reasoning (metacognition, hierarchical reasoning).