DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

TL;DR

DeepTheorem introduces a scalable informal theorem-proving framework that aligns large language models with human-like mathematical reasoning by focusing on natural-language proofs rather than formal proof assistants. It provides a large 121K-sample dataset of IMO-level informal theorems with correctness, difficulty, topic annotations, and verifiable theorem variants, plus proofs generated for training signals. A novel RL-Zero training paradigm leverages verifiable rewards to improve reasoning performance over supervised fine-tuning, accompanied by comprehensive outcome and process evaluation metrics. Empirical results show state-of-the-art performance and strong parameter efficiency, demonstrating the potential of informal, language-based theorem proving for advancing automated mathematical exploration.

Abstract

Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.

Figures (8)

• Figure 1: (a): Our dataset surpasses others with extremely challenging theories; (b): RL-Zero training with our DeepTheorem datasets on 7B model achieves strong results.
• Figure 2: A data sample from the DeepTheorem dataset.
• Figure 3: Difficulty density histogram comparison across widely used training dataset (i.e. Lean-Workbook, Deepseek-Prover-V1, OpenR1 Math) and testing benchmarks (i.e. miniF2F, Putnam-Bench, FIMO, HMMT2425).
• Figure 4: Statistics of DeepTheorem hierarchical topics.
• Figure 5: The process pipeline of constructing DeepTheorem dataset.