Scaling Mathematical Proof Supervision from Structured Textbooks

AI summary

Overview

Research area: Natural Language Processing / mathematical reasoning in large language models, specifically the construction and organization of supervised fine-tuning (SFT) data for proof generation.

Technical level: Intermediate. The paper is readable without deep mathematics, but assumes familiarity with supervised fine-tuning, pass@k evaluation, retrieval-augmented prompting, and curriculum learning.

Scope (one sentence): The paper builds TOME-Math, a 380,292-record proof-supervision corpus extracted from 2,118 university mathematics textbooks while preserving chapter order, proposition–proof links, and dependency references, and then uses it to study how data organization — not just data volume — affects mathematical reasoning in a 30B-parameter base model.

What This Paper Is About

Most mathematical training data for language models is flattened into isolated problem→solution pairs, which throws away the way textbooks actually build knowledge: definitions lead to lemmas, lemmas to theorems, theorems to proofs, all arranged in a prerequisite-respecting chapter order. The authors ask whether keeping that structure — chapter sequence, explicit references between propositions, and source provenance — produces better proof supervision than simply scaling up question–answer pairs. Their goal is both to release a large structured corpus and to run controlled experiments showing which structural signals actually help, at inference time and during training.

Key Contributions

1. TOME-Math corpus. A structure-preserving pipeline converts 2,118 mathematics textbooks into 380,292 proof-oriented QA records — 205,861 Proof QA and 174,431 Gap QA — spanning 29 subject categories, while retaining chapter progression, proposition–proof links, resolved dependency references, source locations, and a separate reservoir of textbook-authored exercises.

2. Full-corpus effectiveness. Fine-tuning Qwen3-30B-A3B-Base on the 364,631-example book-held-out training split raises the unweighted six-benchmark mean from 29.17% to 45.83%, achieving the best score on five of six evaluations (TOME-LongForm, TOME-Objective, MiniF2F, ProofNet, MATH-500) and second on AIME 2026, outperforming all three public instruction-data baselines in aggregate.

3. Isolating what structure buys. Three controlled studies: training-free structure-guided retrieval lifts TOME-LongForm pass@1 from 13.25% to 17.38% under a matched context budget; forward textbook curricula beat shuffled and reverse schedules across six subjects and three data scales; and spreading a fixed token budget across more books improves every subject.

4. Ablation of the training recipe. A full-corpus ablation separates the contributions of Gap QA, forward chapter ordering, and Gap-first scheduling, showing each is necessary and that they reinforce one another.

Main Findings

• Aggregate gain over the base model. TOME-Math improves the six-benchmark unweighted average from 29.17% to 45.83%, a 16.66-point gain (16.7 rounded). Per-benchmark: TOME-LongForm 43.86, TOME-Objective 43.96, MiniF2F 57.43, ProofNet 42.98, MATH-500 76.55, AIME-26 10.19, versus base scores of 13.25, 32.93, 34.45, 17.14, 68.80 and 8.44.

• Size is not the explanation. OpenMath1 contains 1.82M examples, roughly 4.8× TOME-Math, yet averages 29.13% and loses to TOME-Math on all six benchmarks. MetaMath (395k) averages 34.64% and MathInstruct (262k) averages 41.10%, both below TOME-Math's 45.83%. The authors caution that this comparison alone does not isolate textbook structure as the causal factor.

• Structure-guided retrieval helps without any training. On the same 300 TOME-LongForm problems with a frozen model and a shared context budget, pass@1 rises 13.25% (Closed) → 14.00% (Random Same-Book) → 14.71% (Local Chapter) → 15.54% (TOME Props Only) → 17.38% (TOME Props + Gap), a 4.13-point gain. Adding Gap QA on top of propositions is worth 1.84 points.

• Retrieval gains are broad but not automatic. The full TOME (Props + Gap) policy improves all six subjects by 1.75–6.00 points over Closed, with the largest gains in mathematical analysis and topology (+6.00 each). Random same-book or local-chapter context sometimes leaves performance unchanged or lowers it.

• Forward curricula beat alternatives at every scale. At 0.75M, 1.8M and 2.4M tokens per subject, macro-average pass@16 is 41.04% → 42.52% → 43.21% for Shuffle, versus 45.38% → 48.98% → 50.93% for Forward–Gap. Forward–Gap is strongest in all 18 subject–scale cells.

• Chapter direction is the dominant ordering signal. Forward–Gap beats Reverse–Gap by 5.65, 7.41 and 8.50 points across the three scales; with forward progression held fixed, Gap-first ordering adds a smaller but consistent 2.37, 1.91 and 1.53 points over Forward–Mix. The margin over Shuffle widens from 4.34 to 6.46 to 7.72 points as data grows.

• Source breadth is a separate scaling axis. At a fixed 0.75M-token Forward–Gap budget, spreading training over 16 books instead of 8 (Broad–sparse vs Narrow–dense) improves pass@16 in every subject by 1.6–4.8 points (3.3 on average). Largest gains: topology +4.8, differential geometry +4.4, discrete mathematics +3.6; smallest: mathematical analysis +1.6.

• Subject-specific supervision transfers across fields. Normalizing each checkpoint's off-domain score by the target specialist's in-domain score gives a macro-average transfer coefficient of 0.92; topology (0.98) and differential geometry (0.97) have the strongest source-side means, eight of 30 ordered pairs exceed 1.0, and both fields reach 1.29 on probability targets.

• Every recipe component matters. Ablating the full recipe lowers pass@1 on all six benchmarks: without Gap QA, scores fall most on the four proof benchmarks (5.05–6.77 points); swapping Gap-first for within-stage mixing costs 3.74 and 2.59 points on the two TOME benchmarks, with global shuffling costing a further 0.25 and 0.95.

Methodology in Plain English

Building the corpus. The pipeline starts with 2,118 PDF textbooks selected against university course syllabi and reviewed by domain experts. DeepSeek-OCR converts each PDF into multimodal Markdown plus page images. A page-by-page model pass separates tables of contents and body text from covers and prefaces, rebuilds a hierarchical table of contents, and then walks the book with a state machine that decides, for each page, whether it belongs to the current chapter, the next chapter, or straddles a boundary. Ambiguous boundaries are re-checked. A second pass splits expository content from textbook exercises; exercises are kept aside as an evaluation reservoir and never enter the proof-generation path.

Two kinds of proof supervision. From expository chapters, a model extracts theorem–proof, lemma–proof and definition–proof units and retrieves the earlier propositions each proof relies on — these are Proof QA. Then a stronger model with thinking enabled audits each proof for gaps (skipped steps, unstated lemma assumptions, "obviously" jumps). When it finds a substantive gap, a lighter model rewrites the missing obligation as a self-contained proposition and proves it — these are Gap QA. Of 918,235 generated Gap QA candidates, 174,431 survived, a 19.00% yield. Quality control runs at both structural level (TOC hierarchy, page boundaries, question continuity, answer alignment, standalone completeness) and semantic level (a source-conditioned judge scoring completeness, accuracy, LaTeX formatting, self-containment and atomicity, treating invented proof steps as failures rather than style issues).

Evaluating. All experiments use Qwen3-30B-A3B-Base and differ only in supervision corpus, training for one epoch each. Evaluation covers six subjects with the largest usable textbook collections (abstract algebra, differential geometry, discrete mathematics, mathematical analysis, probability, topology). TOME-LongForm holds 300 proof-heavy problems drawn from 64 reserved books; all 15,661 QA records tied to those books are excluded, leaving 364,631 training examples. Each problem gets 16 sampled solutions, scored by a reference-guided step verifier that reviews each solution eight times with gpt-5.6-luna and accepts it only if no review finds a substantive error. TOME-Objective adds 145 multidisciplinary objective problems, and MiniF2F, ProofNet, MATH-500 and AIME 2026 provide public coverage.

Controlled studies. The retrieval experiment holds the context-token budget, backbone, prompt and decoder fixed across five context policies, removing the target exercise and any overlapping reference material from every pool. The curriculum experiment holds examples, token budget, initialization and optimizer fixed while reordering the same frozen QA set into Shuffle, Forward–Gap, Reverse–Gap and Forward–Mix. The breadth experiment holds the 0.75M-token budget fixed while doubling books from 8 to 16.

Why This Matters

Impact on research. The paper reframes mathematical data scaling as a question of organization rather than raw count, and provides an empirical framework — plus a released corpus — for studying how curriculum order, dependency structure and source breadth affect reasoning. It also introduces Gap QA as a supervision signal that targets precisely the intermediate steps textbooks leave implicit, and shows this signal is worth more than chapter ordering on proof benchmarks.

Real-world applications.

• Automated tutoring and textbook-companion systems that need to generate or verify proofs step by step, aligned to a specific course's chapter order.
• Formal mathematics and autoformalization pipelines (e.g., Lean-based projects) that need large pools of natural-language proofs with dependency metadata before translation.
• Curriculum and assessment design, using the retained exercise reservoir to build placement or practice sets tied to source provenance.
• Retrieval-augmented study assistants that cite the exact book, chapter and proposition behind an answer.

Industry relevance. Structured supervision with provenance is directly useful to teams building domain-specific reasoning models, since it enables auditable citations and controlled data-mixing decisions. The cost analysis is practical too: the authors record per-book costs of $40–50 for the strongest thinking configuration, roughly $5 for the lite model, about $10 for the mid-tier thinking model, and about $7 for the chosen hybrid — evidence that corpus construction at this scale is economically feasible with deliberate model allocation.

Future Directions

• Extending structure to more subjects and levels. The evaluation concentrates on six university subjects with the largest usable textbook collections; whether the same curriculum and retrieval benefits hold for the remaining 23 subject categories, or for pre-university material, is untested.

• Formal verification. The pipeline is entirely natural-language; connecting Gap QA obligations to proof assistants so that generated intermediate steps can be machine-checked is a natural next step the paper does not pursue.

• Alternative orderings and dependency-aware schedules. The ablations show chapter direction dominates and Gap-first ordering adds a smaller complementary gain; whether finer-grained dependency graphs (rather than linear chapter order) yield additional gains is left open.

• Separating corpus effects more cleanly. The authors explicitly note that the full-corpus comparison against public baselines "does not by itself isolate textbook structure as the causal factor," inviting controlled experiments that vary only structure at matched content.

Target Audience

Researchers and engineers working on mathematical reasoning and data-centric training for language models — particularly those who build SFT corpora, design curricula, or study retrieval-augmented reasoning. It is also relevant to teams working on autoformalization and to educators or content engineers interested in turning textbook structure into machine-usable supervision. Readers wanting to reproduce or extend the work will need the appendices, which document the module-level pipeline, the judging rubric, model allocation, training configurations and scoring protocols.

Authors’ abstract

Mathematical supervision for language models is typically flattened into isolated problem-solution pairs, discarding the curricular organization and evidential structure of the original sources. We introduce TOME-Math (Textbook-Oriented Mathematical Evidence), a large-scale corpus that converts 2,118 textbooks spanning the core areas of university-level mathematics subjects into approximately 380K structured proof-supervision records while preserving chapter order,…