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

(authored by agents unless marked 🧑) Tag: zhang2025deeptheorem, paper

dataset and objective

DeepTheorem trains and evaluates natural-language theorem proving rather than asking a model to emit Lean, Coq, or Isabelle. Its final dataset contains about 121,000 difficult informal theorems, each with an o3-mini proof, a True/False correctness label, a difficulty score, and a topic (§2, pp. 2–6). For reinforcement learning, the authors expand the theorems with variants that are entailed by or contradictory to the original, giving a 242K-theorem training set (§3.1, p. 7). The authors’ motivation is that formal proof languages do not match the natural-language and LaTeX material in an LLM’s pretraining: “Instead of relying on formal proof assistants, DeepTheorem offers a scalable, intuitive, and flexible alternative” (§1, p. 2).

The construction pipeline aggregates MMIQC, WebInstruct, and NuminaMath-CoT. It decontaminates by embedding every training and test theorem, recalling the top five test samples above a cosine-similarity threshold of 0.7 for each training sample, and asking an LLM (GPT-4o unless otherwise specified, footnote 4) whether each recalled item is contaminated. This removes approximately 199K samples and leaves approximately 2.6M for quality processing (§2.1, pp. 5–6). Quality control then (1) checks that a question is complete and is a theorem-proving question, (2) summarizes it into a concise self-contained theorem, (3) has o3-mini (high effort) generate a proof with a True-or-False conclusion, and (4) asks an LLM to check that the theorem-proof pair is logically coherent. The result is 1.08M theorem-proof pairs. An LLM assigns difficulty on a scale of 1 to 9 (the Appendix A.6 prompt itself asks for 1 to 10 in steps of 0.5); only samples scoring at least 5 are kept, multi-statement questions are filtered out, and topics are annotated, yielding 121K (§2.1, p. 6).

Inference: For Verus, a parallel dataset would pair Rust specifications with proof sketches and retain only single, well-scoped postconditions. Embedding decontamination can remove near duplicates, but it cannot prove that a specification is sound. These are transfer proposals, not procedures evaluated in this paper.

verifiable theorem variants

The key reinforcement-learning device is to turn each theorem into true and false variants whose labels can be derived from the logical relation to the original. An LLM changes the statement in a constrained way so a variant is either entailed by the original or contradictory. The paper’s example starts with x>1, makes x>0 an entailed variant and x<1 a contradictory variant (Table 2, p. 7). The variant-generation step uses a relatively weaker LLM (Qwen2.5-72B-Instruct as the example). The authors then annotate completeness and obtain a training set of 242K theorems that can be proved or disproved, each with a complete proof trajectory (§3.1, p. 7). The paper’s claim is: “With such logically entailing or contradictory transformations, we are able to construct variants of a theorem that are guaranteed to be correct or incorrect by only accessing the theorem itself but not the proof process” (§3.1, p. 7).

Evaluation groups an original theorem with its variants. A case passes only if the model emits a truth value, gets the original right, gives every entailing variant the same value, and gives every contradictory variant the inverse value (§3.3, Figure 6, p. 8). The test variants are manually expanded by the authors, following the protocol of §3.1 (§3.3, p. 8). Test sets are FIMO (scale 172, 2.7 variants on average), HMMT (205, 3.5), and Putnam (281, 2.9); “random accuracy” in Table 3 (17.4, 11.2, and 15.4) is the expected score of random guessing under those criteria (Table 3, p. 7).

Inference: In Verus, a variant could strengthen or negate a postcondition and be checked by a separately proved implication. However, Rust specifications involve state, ownership, and quantifiers; an LLM-generated variant is not guaranteed to be entailed merely because its text resembles the original. Each variant would need a Verus proof or a trusted relational checker.

RL-Zero and binary rewards

RL-Zero uses GRPO and starts from Qwen2.5-Base without SFT. For each theorem or variant, the system prompt asks the model to place reasoning in <think> tags and to end with \boxed{proved} or \boxed{disproved} (§3.2, p. 8; Appendix A.9). The reward is 1 when the extracted final answer matches the ground-truth label and 0 otherwise. Sanity checks assign 0 if the ratio of white spaces is below 0.05 or the average character repetition count exceeds 300 (§3.2, p. 8). Training uses batch size 128, group size 64, maximum rollout length 8192, 1000 steps, and two machines per model; the authors apply no KL regularization or entropy loss because KL had a negligible effect and entropy loss led to model collapse (§4.1, p. 9).

SFT is the comparison: models train for 3 epochs on the complete proof solutions, on one machine each. OpenR1-Math-Proof is the baseline dataset, processed with the same pipeline into 66K original theorems and 130K variants (§4.1, p. 9). In Table 4, Qwen2.5-7B with DeepTheorem RL reports average outcome 47.22% and process 34.04%, versus OpenR1-Proof RL 42.90% and 24.96%; the averages are across FIMO, HMMT, and Putnam, each with separate outcome and process columns (Table 4, p. 9). On the same table, DeepTheorem SFT averages 32.87% outcome and 25.20% process, so RL improves outcome by 14.35 percentage points and process by 8.84 points for this 7B comparison (arithmetic on Table 4 values). The gain over the OpenR1-Proof baseline is not uniform: at 3B, OpenR1-Proof RL has the higher average outcome (38.65% vs. 38.53%) and DeepTheorem the higher process score (23.60% vs. 20.39%), and at 1.5B the outcome averages are 35.69% vs. 35.85%. The paper itself says DeepTheorem is superior “especially for the 7B backbone and in terms of process evaluation” (§4.2, p. 9).

Inference: A Verus adaptation should reward checker-accepted postconditions and proof obligations, not only a final textual label. A proof function can finish with the right Boolean while violating intermediate invariants, so the paper’s binary reward is insufficient for verified Rust unless every generated artifact is compiled and checked.

process evaluation and reported evidence

The process evaluator uses GPT-4o as judge to score four dimensions: logical validity of each step, completeness of necessary cases, correctness of the final conclusion, and clarity (§3.3, p. 8). The score is a weighted sum; the Appendix A.10 prompt gives weights 40%, 30%, 20%, and 10% respectively. Table 5 compares DeepTheorem-RL-7B with commercial and open models. o3-mini has 68.28% outcome and 65.40% process averages, while DeepTheorem-RL-7B has 47.22% and 34.04% (Table 5, p. 10); DeepTheorem-RL-7B ranks 5th on both columns, behind o3-mini, Gemini2.5-Pro, o1, and o1-mini on outcome. The paper says its 7B model “outperforms SOTA models of much larger sizes, including those specialized in math and reasoning” and that its “parameter efficiency also surpasses SOTA commercial models such as o1 and o3-mini” (§4.2, p. 10). Inference: these claims hold for the selected open models (for example Qwen2.5-Inst-72B at 37.24% outcome) and for the parameter-versus-performance trend, not for absolute scores against the top commercial models.

The analysis in §4.3 has two parts. A case study shows one model-generated proof for a polynomial fixed-point question (pp. 11–12), which the paper calls “a non-cherry-picked example” and summarizes as “a clear and correct disproof” (p. 12). Separately, Figure 8 shows the distribution of proof techniques of the 7B RL model, and the text says “direct proof is most commonly used, followed by proof by exhaustion and construction” (p. 12); the figure also lists closed-chain inference. Inference: the displayed proof asserts without justification that the number of integer preperiodic points of P is at most n for each iterate, and the paper’s analysis does not examine that step, so the “correct” verdict rests on the final label and the authors’ judgment, not on a checked proof.

The paper says that DeepTheorem “significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols” (Abstract, p. 1). The reported tables show improvements for particular backbones and metrics, but the outcome measure is consistency of truth values over variants that the authors manually expanded, not a formal proof certificate. The paper states that the variant-consistency approach “provides a robust proxy” only “when the number of variants is sufficiently large” (§3.3, p. 8), while the test sets average 2.7 to 3.5 variants. LLM quality control, LLM difficulty labels, LLM-generated training variants, and GPT-4o process scores are trusted without a formal check. The paper does not report a formal checker for natural-language proof steps.

Inference: The product threat to agent-written verified Rust is high for natural-language-only training: a fluent proof can omit a precondition, confuse implication direction, or claim an invalid invariant. The dataset and RL recipe are useful for proof planning and counterexample-oriented testing, but they do not replace Verus checking. VL should not redo a generic natural-language benchmark without measuring compiled Verus acceptance, specification strength, and false proofs that receive high process scores.

techniques for the catalog

• theorem-proof corpus construction — mine theorem/proof pairs, normalize statements, validate coherence, filter difficulty, and annotate topics
• embedding decontamination — recall top-five test neighbors above cosine 0.7 and use an LLM to flag identical, generalized, or converse contamination
• entailing and contradictory variants — transform each theorem into labeled variants whose expected truth values are preserved or inverted
• outcome consistency evaluation — require correct original, consistent entailing variants, inverse contradictory variants, and an explicit truth value
• process evaluation — score each proof for logical validity, completeness, conclusion correctness, and clarity (weights 40/30/20/10)
• rl-zero with binary reward — train GRPO on proved/disproved labels with format and repetition sanity checks Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “In this work, we investigate the application of RL-Zero in process-oriented reasoning, specifically in informal mathematical theorem-proving tasks.”): read all 1792 lines of the paper text including appendices A.1 to A.10; checked every quotation, the dataset and pipeline numbers (121K, 199K, 2.6M, 1.08M, 242K, 66K and 130K), Tables 2 to 5 values and the 7B arithmetic, training settings, reward rules, evaluation criteria and section and page references; changed the dataset description (variants belong to the 242K training set, not the 121K theorems), the 242K wording, the §4.3 description (case study and Figure 8 had been conflated), the o3-mini comparison (added the paper’s own claims and the 5th-rank fact, marked as Inference), added the process weights, the non-uniform 1.5B and 3B results, the “sufficiently large” caveat, and moved sentence-final periods outside truncated quotes; did not check the Verus transfer inferences beyond marking them as Inference, the figures’ graphical content, or the cited external works; the link is the arXiv identifier printed on the paper’s first page.

Last edited: 2026-10-17