Llemma: An Open Language Model For Mathematics

🎯 Pitch

An open-source 7B model trained entirely on mathematical data not only matches the unreleased 60B+ parameter Minerva on the MATH benchmark, but can also prove theorems in formal systems like Lean without any specific finetuning. This work shows that careful data curation and continued pretraining on code and proofs can unlock formal reasoning as a near-free emergent behavior.

1. Executive Summary

This paper introduces LLEMMA, a 7B and 34B parameter language model specialized for mathematics through continued pretraining of Code Llama on Proof-Pile-2 — a 55B-token mixture of scientific papers, web data containing mathematics, and mathematical code. LLEMMA outperforms all known open base models on the MATH benchmark and matches the unreleased Minerva model suite on an equi-parameter basis, achieving 43.1% Maj@256 with the 34B model versus Minerva 62B's 43.4%. The model demonstrates emergent capabilities in computational tool use (solving MATH problems by generating Python code that calls SymPy and the math module) and few-shot formal theorem proving (generating Lean 4 tactic steps and Isabelle formal proofs from informal descriptions) without any task-specific finetuning. On chain-of-thought reasoning, continued pretraining on Proof-Pile-2 yields a 20-percentage-point improvement on GSM8k and 13 points on MATH over the Code Llama initialization, establishing that domain-specific continued pretraining provides substantial gains for mathematical reasoning even when starting from a strong code-focused base model.

2. Context and Motivation

The Core Problem: We Don't Have Open, Capable Math-Specialized Language Models

The fundamental gap this paper addresses is straightforward but critical: there is no publicly available language model that achieves competitive performance on mathematical reasoning while remaining open for research and downstream use. The state of mathematical language models prior to LLEMMA was bifurcated into two unsatisfying categories:

Closed, high-performing models, exemplified by Minerva (Lewkowycz et al., 2022), which continued pretraining PaLM on technical content to achieve 33.6% on MATH at 540B parameters and 50.3% with majority voting. These models demonstrate that domain-specific continued pretraining works, but they are completely inaccessible — no weights, no training data, and no ability to serve as a platform for further research.
Open, low-performing models, such as those in Azerbayev et al. (2023), which lag far behind the closed state-of-the-art. Prior to LLEMMA, no open model had demonstrated the kind of mathematical reasoning capabilities that would make it a viable research platform, nor had any open model shown emergent capabilities in tool use and formal theorem proving that follow from strong mathematical pretraining.

This gap is not merely inconvenient — it actively constrains research progress. As the authors note in Section 1, language models capable of strong mathematical reasoning are upstream of a number of research topics, including reward modeling (Uesato et al., 2022; Lightman et al., 2023), reinforcement learning for reasoning (Polu et al., 2022; Lample et al., 2022), and algorithmic reasoning (Zhou et al., 2022; Zhang et al., 2023). When the only models capable of driving progress in these areas are closed, the entire research ecosystem becomes dependent on proprietary systems that can be deprecated, rate-limited, or modified without notice.

Why This Problem Matters

Research infrastructure. Open-weight models serve as community platforms. Researchers need to probe internal representations, study scaling behavior, run controlled ablations, and fine-tune for novel downstream tasks — all of which require access to model weights. The paper positions LLEMMA as filling precisely this infrastructure role, explicitly stating they hope it "will serve as a platform for future research in mathematical reasoning" (Section 1, contribution 4).

Domain specialization as a practical deployment strategy. The paper situates itself within a broader question about the utility of domain-specific models versus generalist models. While generalist models like Llama 2 (Touvron et al., 2023) aim for balanced performance across the entire distribution of natural text, the paper argues (Section 1) that domain-specific models offer superior capabilities at a given computational cost, or equivalent capabilities at lower cost. This is not just a research curiosity — it has direct implications for how organizations allocate compute budgets between training generalist models and specializing them.

Mathematical reasoning as a domain adaptation testbed. The authors select mathematics deliberately, arguing it "serves as an ideal setting for domain adaptation" because it requires "pattern matching against a large body of specialized prior knowledge" (Section 1). Unlike factual knowledge domains (medicine, finance) where retrieval or memorization might suffice, mathematical reasoning demands multi-step logical deduction, symbolic manipulation, and the ability to recognize abstract patterns across superficially different problems. If domain adaptation through continued pretraining can substantially improve mathematical reasoning, it provides a strong signal for similar gains in other structured reasoning domains (code, formal logic, scientific reasoning).

Tool use and formal mathematics as capability frontiers. The paper is also motivated by a vision of mathematical AI that goes beyond generating text solutions. Computational tools (Python, SymPy, computer algebra systems) and formal theorem provers (Lean, Isabelle, Coq) are of "ever increasing importance to mathematicians" (Section 2.1), and the authors want a model that can interface with these tools. Prior open models showed essentially no capability in these areas without task-specific finetuning, whereas LLEMMA demonstrates emergent few-shot tool use directly from continued pretraining (Section 3.2, 3.3).

Where Prior Approaches Fall Short

Minerva's openness gap. Minerva (Lewkowycz et al., 2022) established the efficacy of continued pretraining on technical content for mathematical reasoning, achieving 50.3% Maj@256 on MATH with a 540B parameter PaLM model. However, the Minerva model weights, training data, and training code are all proprietary. This means the community cannot build on Minerva, cannot study why its continued pretraining works, cannot fine-tune it for new tasks, and cannot verify its results independently. The paper identifies several concrete ways it differs from Minerva while building on its approach (Section 1):

Broader training and evaluation — LLEMMA's Proof-Pile-2 covers code data (the AlgebraicStack, containing 11B tokens across 17 mathematical programming languages), tool use tasks, and formal mathematics, none of which were in Minerva's training regime.
Full reliance on public data and tools — Minerva's training dataset (38.5B tokens) is undisclosed; LLEMMA's 55B-token Proof-Pile-2 is fully released with documented sources and filtering procedures.
New analyses — the paper provides analyses of data mixture effects, memorization, and supervised finetuning that Minerva did not.
Complete open release — weights, dataset, and code are all publicly available.

Code Llama and generalist models as insufficient baselines. Code Llama (Rozière et al., 2023), the initialization for LLEMMA's continued pretraining, was trained on 500B tokens of code and demonstrates reasonable mathematical performance (12.2% on MATH at 34B). However, as Table 1 shows, Code Llama's math performance is substantially below what domain specialization can achieve — LLEMMA 34B doubles MATH accuracy to 25.0% from Code Llama's 12.2%. This demonstrates that general code pretraining, while beneficial for mathematical reasoning compared to pure text pretraining, does not substitute for targeted mathematics data.

Supervised finetuning approaches as task-specific, not foundational. The paper distinguishes its approach from a parallel line of work that applies supervised finetuning to boost mathematical benchmark scores (Yu et al., 2023; Yue et al., 2023; Luo et al., 2023). The authors acknowledge these approaches "boost performance on some common mathematical language modeling benchmarks" but argue they "train the model for these specific tasks" (Section 4). In contrast, continued pretraining on Proof-Pile-2 produces a general-purpose mathematical base model that is not tuned to any particular evaluation format, making it a "platform for further development" rather than a benchmark specialist. The paper validates this claim by showing that LLEMMA transfers to multiple downstream tasks (chain-of-thought reasoning, Python-based problem solving, formal theorem proving) without task-specific finetuning.

Formal mathematics models are small and task-specialized. Prior work on neural theorem proving (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022) typically used models in the sub-billion to few-billion parameter range, fine-tuned specifically for tactic prediction on a single proof assistant. These models lack the general mathematical knowledge that would enable transfer between proof assistants, or between informal and formal mathematics. The paper's demonstration that LLEMMA can perform few-shot tactic prediction (generating Lean 4 proof steps from just 3 examples) without any finetuning — and can autoformalize informal proofs into Isabelle — represents a significant expansion of what's possible with an open base model in formal mathematics.

Data availability for mathematical pretraining. Prior to Proof-Pile-2 and OpenWebMath (Paster et al., 2023), there was no high-quality, publicly available, large-scale dataset of mathematical text suitable for language model pretraining. The Minerva dataset was undisclosed. OpenWebMath (15B tokens, released contemporaneously) provided the web component, and the AlgebraicStack (11B tokens, introduced in this paper) provided the mathematical code component. Together with ArXiv (29B tokens, already publicly available through RedPajama), these datasets form a reproducible 55B-token corpus. The paper's release of Proof-Pile-2 is itself a contribution, lowering the barrier for others to train mathematics-focused language models.

How LLEMMA Positions Itself

The paper situates LLEMMA at the intersection of several research threads while carving out a distinct contribution:

Relative to Minerva: LLEMMA is the open replication and extension. It follows the same continued pretraining paradigm — start from a general-purpose pretrained model and train further on technical content — but extends it with mathematical code, formal mathematics data, and tool-use capabilities. The comparison is explicit: Figure 2 tabulates model and dataset statistics side by side, and Tables 1 and 2 benchmark both models on identical tasks. The message is clear: LLEMMA achieves Minerva-competitive performance (43.1% vs. 43.4% on MATH Maj@256 for 34B vs. 62B) while being fully open and operating at a smaller parameter count.

Relative to generalist models: LLEMMA argues for domain specialization as a deployment strategy. The paper's experiments answering "what if we continue pretraining on math-specific data?" provide evidence that substantial gains are possible without scaling the base model. The 7B LLEMMA model outperforms Code Llama 34B on MATH (18.0% vs. 12.2%), demonstrating that targeted data can sometimes compensate for model scale.

Relative to supervised finetuning approaches: LLEMMA is positioned as a base model — not fine-tuned for any particular evaluation format or task. The paper includes a supervised finetuning experiment (Appendix G) to demonstrate that LLEMMA retains its advantage when adapted to specific benchmarks (25.2% on MATH vs. 19.4% for Llama 2 7B when both are fine-tuned on MetaMathQA), but this is presented as a secondary result. The primary framing is LLEMMA as infrastructure: a model that researchers can use for their own downstream applications.

Relative to formal mathematics models: LLEMMA demonstrates that a general mathematical base model can perform formal mathematics tasks few-shot, without the specialized finetuning that prior models required. On informal-to-formal proving, LLEMMA-7B closes 22.1% of miniF2F test theorems (greedy decoding) compared to Sledgehammer's 20.5% and Code Llama 7B's 17.6%. On formal-to-formal proving in Lean 4, LLEMMA-7B achieves 26.2% — comparable to ReProver (26.5%), a model that was specifically fine-tuned and retrieval-augmented for this task. This is presented as evidence that the mathematical knowledge encoded during continued pretraining transfers to the formal domain without task-specific adaptation.

Relative to open-source norms: The paper makes a deliberate choice to release all artifacts — models at both 7B and 34B scales, the 55B-token Proof-Pile-2 dataset, and the training and evaluation code. This is positioned as a contribution in its own right (Section 1, contribution 4), and the paper includes a detailed datasheet (Appendix E) following Gebru et al. (2021) to document the dataset's composition, collection, and intended uses. This level of documentation and openness is a direct response to the opacity of prior math-focused language models.

The Unstated Motivation: Research Velocity

Reading between the lines, a key motivation for LLEMMA is accelerating research on mathematical AI. When models are closed, research progress depends on the willingness of a few organizations to release results. When models are open, the entire community can experiment, iterate, and build. The paper's emphasis on LLEMMA as a "platform" (used in Section 1, 4, and the Conclusion), its release of both 7B and 34B checkpoints (accommodating researchers with different compute budgets), and its careful documentation of data composition and training procedures all point to this meta-goal: make it as easy as possible for others to build on this work. This aligns with EleutherAI's broader mission of open-source AI research, as reflected in the author affiliations and the use of community infrastructure like GPT-NeoX and the Language Model Evaluation Harness.

3. Technical Approach

3.1 Reader Orientation

LLEMMA is a decoder-only transformer language model produced by taking an existing general-purpose model (Code Llama) and continuing to train it — from scratch would be misleading; "continuing" means resuming training from a checkpoint — on a carefully curated 55-billion-token dataset of mathematics-specific text and code called Proof-Pile-2. The problem it solves is that no open-weight language model achieved competitive mathematical reasoning performance: the only strong math models (Minerva) were proprietary, making them unavailable for research. The "shape" of the solution is refreshingly straightforward: rather than inventing new architectures, training objectives, or fine-tuning protocols, the paper demonstrates that curating the right domain-specific pretraining data and continuing to train a strong code-capable base model on it is sufficient to produce a state-of-the-art open mathematical language model with emergent capabilities in tool use and formal theorem proving that were not explicitly trained.

3.2 Big-Picture Architecture

The system has four major components organized as a pipeline:

Proof-Pile-2 Dataset (55B tokens) — a curated mixture of three mathematical data sources (AlgebraicStack code, OpenWebMath web pages, ArXiv papers) plus a small amount of general-domain data for regularization. This is the fuel for the entire approach.
Code Llama Base Models (7B and 34B) — decoder-only transformers pretrained on general text (via Llama 2) and then on 500B tokens of code. These serve as the initialization for continued pretraining, providing strong general reasoning and code capabilities that the math data builds upon.
Continued Pretraining Procedure — a standard autoregressive language modeling training run that resumes from the Code Llama checkpoints and trains on Proof-Pile-2 for 200B additional tokens (7B) or 50B tokens (34B). This is where the mathematical specialization happens.
Evaluation Suite — a multi-faceted assessment covering chain-of-thought problem solving (MATH, GSM8k, OCWCourses, MMLU-STEM, SAT), computational tool use (generating Python that calls SymPy and built-in math functions), and formal theorem proving (generating Isabelle proofs from informal descriptions, and generating Lean 4 tactic steps from proof states).

Information flows linearly: Proof-Pile-2 data → continued pretraining of Code Llama → LLEMMA checkpoints → few-shot evaluation on downstream tasks. There is no iterative refinement, no RL, no special decoding — the entire technical contribution is in the data curation and the training recipe.

3.3 Roadmap for the Deep Dive

First, the Proof-Pile-2 dataset: its three components (AlgebraicStack, OpenWebMath, ArXiv), their sizes, their curation pipelines, and the rationale for including code and formal mathematics data — because the data is the paper's primary intellectual contribution.
Second, the base model initialization (Code Llama) and why starting from a code-trained model matters — because the choice of initialization is a key design decision that the paper justifies.
Third, the continued pretraining procedure: learning rates, batch sizes, context lengths, RoPE adjustments, hardware configuration, and the specific problem of NaN losses — because reproducing these results requires exact training details.
Fourth, the data mixture selection methodology: how the authors chose the 2:4:1 arXiv:Web:Code ratio, the role of perplexity on the MATH training set as a proxy, and the general-domain regularization data — because mixture weights are a critical hyperparameter that the paper studies systematically.
Fifth, the evaluation methodology for each task category: chain-of-thought prompting, majority voting, Python tool use, informal-to-formal proving, formal-to-formal proving — because LLEMMA is evaluated across radically different task formats.
Sixth, the memorization and data overlap analysis methodology — because the paper makes specific claims about whether LLEMMA's performance comes from genuine reasoning versus memorization.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a data engineering and continued pretraining paper whose core idea is that curating a high-quality, multi-source mathematical corpus and training a code-capable base model on it produces a general-purpose mathematical language model with emergent cross-task capabilities, without needing task-specific architectures or fine-tuning.

Proof-Pile-2: The Mathematical Pretraining Corpus

The Proof-Pile-2 is a 55-billion-token mixture of three mathematical data sources — code, web pages, and scientific papers — plus a small amount of general-domain text and code for regularization. The composition and curation of this dataset is the paper's foundational contribution, since everything else (model architecture, training objective, evaluation) uses standard components. The mixture weights are:

AlgebraicStack (mathematical code): 11B tokens, weighted at 1.00 (serving as the baseline weight; all other weights are relative multipliers)
OpenWebMath (mathematical web pages): 15B tokens, weighted at 4.00 (meaning each token from OpenWebMath appears 4× more frequently in the training mixture than a token from AlgebraicStack, per unit of raw data)
ArXiv (scientific papers): 29B tokens, weighted at 2.00
General code (RedPajama GitHub subset): 59B tokens available, weighted at 0.22
General language (Pile, with ArXiv removed): 300B tokens available, weighted at 0.15

The final training mixture is 95% Proof-Pile-2 and 5% general-domain data (2% Pile, 3% RedPajama GitHub), following Lewkowycz et al. (2022) who found that a small fraction of general-domain data acts as a regularizer during continued pretraining, preventing catastrophic forgetting of general language capabilities.

Detailed component breakdown:

AlgebraicStack (11B tokens, 17 programming languages). This is a novel dataset constructed specifically for this paper, designed to cover the full spectrum of computational mathematics: numerical computing, symbolic mathematics, formal theorem proving, and scientific simulation. The sources are:

GitHub repositories downloaded directly via the GitHub Python API for languages poorly represented in the Stack dataset (Coq, Isabelle, Lean, MATLAB). For each language, the authors apply language-specific keyword whitelists and blacklists to filter for genuine mathematical content. For example, Coq files must contain keywords like "Theorem", "Proof", "Qed", "Inductive", "Definition", or "Fixpoint" and must NOT contain Verilog keywords like "pragma", "endmodule", "posedge", "negedge", or "wire". Isabelle files must match the patterns "theorem " or "lemma ". Lean files are whitelisted with "theorem ", "lemma ", "example " and explicitly blacklisted from the ProofNet and MiniF2F repositories (to avoid benchmark contamination). MATLAB files use a whitelist of "#import", "interface", "implementation", "property" and blacklist C keywords. All GitHub downloads use a cutoff date of April 1, 2023.
The Stack dataset (Kocetkov et al., 2022) for languages well-represented there: Agda, C, C++, Fortran, GAP, Haskell, Idris, Julia, Jupyter notebooks, Maple, Python, R, and TeX. Each language receives custom filtering. For example, C files must include specific math library headers (fftw, gsl, cblas, blas, lapacke, nlopt, petsc). C++ files must include headers from numerical libraries (adept, alglib, boost/armadillo, blitz, Eigen, deal.II, dlib, NTL, mtl). Jupyter notebooks are converted to markdown via nbconvert to strip base64 images and large cell outputs. Python files must import from a fixed list of scientific and mathematical libraries. TeX files are filtered for documents containing section/chapter commands and identified as English by the langid classifier.
Lean proofsteps: extracted from Mathlib 4 (the mathematical library for Lean 4) using the lean-training-data tool (Morrison, 2023) at commit c779bd5 (August 20, 2023). Each entry is a (tactic state, next tactic) pair, where the tactic state is the proof assistant's internal representation of what needs to be proved at that step, and the next tactic is the command the human wrote to advance the proof. This data is included as raw text in AlgebraicStack, not as a structured training signal — the model learns from it autoregressively like any other text.
Isabelle proofsteps: constructed from the Archive of Formal Proofs and Isabelle Standard Library using the PISA tool (Jiang et al., 2021). Each entry includes the theorem statement, proof states, and proof steps separated by specific tags. The dataset is decontaminated against the PISA test set by removing any theorem whose name overlaps with a PISA test theorem name. After filtering, this subset contains 251,000 theorems.

Across all sources, the authors apply document-level exact deduplication by removing documents that contain an overlapping 2048-character chunk with another document. Files with size greater than 1,048,575 bytes are filtered out, as are files with numerical density (ratio of digit characters to non-digit characters) exceeding 0.5.

The token distribution across languages (Table 9) reveals that Python dominates at 6,099M tokens, followed by Isabelle (1,090M), C++ (954M), Fortran (725M), TeX (568M), Julia (531M), Lean (286M), Coq (282M), and smaller amounts of Jupyter, R, MATLAB, Agda, C, Idris, Haskell, Maple, and GAP. This distribution is important because it means the model sees substantial amounts of formal proof assistant code (Lean + Isabelle + Coq ≈ 1.66B tokens), which the paper argues contributes to LLEMMA's emergent formal theorem proving capabilities.

Why include code at all in a math model? The paper's rationale (Section 2.1) is that "computational tools such as numerical simulations, computer algebra systems, and formal theorem provers are of ever increasing importance to mathematicians" (citing Avigad, 2018). More pragmatically, code data provides the model with exposure to mathematical concepts expressed in executable form — seeing SymPy expressions, numerical algorithms, and formal proofs as text teaches the model about mathematical structure in a way that complements natural language descriptions. This is a key difference from Minerva, which trained primarily on natural language math text (papers, web) and did not include substantial code data.

OpenWebMath (15B tokens). This is a contemporaneously released dataset (Paster et al., 2023) that the paper uses as-is. OpenWebMath filters CommonCrawl web pages based on math-related keywords and a classifier-based math score, preserves mathematical formatting (LaTeX, AsciiMath), and includes additional quality filters: perplexity-based filtering (removing text that looks like gibberish to a language model), domain-based filtering, length filtering, and near-deduplication. The 15B-token size reflects extensive filtering — the raw CommonCrawl contains orders of magnitude more data, but most is not mathematical. The preservation of LaTeX formatting is critical because MATH and other benchmarks use LaTeX notation, and the model needs to learn to read and generate it.

ArXiv (29B tokens). The authors use the ArXiv subset of RedPajama (Computer, 2023), which is an open reproduction of the LLaMA training dataset. ArXiv contains scientific papers across all disciplines, not just mathematics, but a substantial fraction covers math, physics, and computer science — all of which involve mathematical notation and reasoning. The papers are preprocessed by RedPajama (which applies standard cleaning, filtering, and deduplication), and the knowledge cutoff is April 2023. Using ArXiv as a paper source rather than scraping papers directly ensures reproducibility and avoids copyright concerns, since RedPajama is publicly available.

General-domain data (5% of training mixture). Following the Minerva recipe, the paper includes small amounts of general text and code to prevent catastrophic forgetting of general language capabilities during domain-specific continued pretraining. The general text comes from the Pile (Gao et al., 2020; Biderman et al., 2022), a widely-used 800GB general-domain dataset, with the ArXiv subset removed since ArXiv is already in Proof-Pile-2. The general code comes from the GitHub subset of RedPajama. The weights (0.15 for Pile, 0.22 for RedPajama GitHub) are much smaller than any Proof-Pile-2 component weight, reflecting the deliberate choice to keep the model focused on mathematics while maintaining minimal general capabilities.

A note on the knowledge cutoff: With the exception of the Lean proofsteps subset (which uses an August 2023 version of Mathlib 4), the entire Proof-Pile-2 has a knowledge cutoff of April 2023. This is important for the SAT evaluation — the paper uses the May 2023 SAT, which postdates the cutoff, ensuring the model cannot have memorized the answers.

Base Model Initialization: Code Llama

LLEMMA is not trained from scratch. Each model (7B and 34B) is initialized from the corresponding Code Llama checkpoint (Rozière et al., 2023). Code Llama models are themselves initialized from Llama 2 (Touvron et al., 2023) and then further trained on 500B tokens of code (a mix of publicly available code datasets, heavily weighted toward general-purpose programming). This means LLEMMA inherits:

From Llama 2: General language understanding from pretraining on 2 trillion tokens of text, plus the standard Llama architecture (decoder-only transformer with pre-normalization using RMSNorm, SwiGLU activation function, and rotary position embeddings).
From Code Llama: Strong code generation and reasoning capabilities from 500B tokens of code training, plus modifications to support long contexts (Code Llama was fine-tuned for 16k-token contexts through RoPE interpolation, though LLEMMA itself uses 4096-token context length during training).

Why Code Llama rather than pure Llama 2? The paper does not explicitly ablate this choice (no comparison of LLEMMA initialized from Llama 2 vs. Code Llama), but the rationale is implicit: mathematical reasoning involves symbolic manipulation and structured problem-solving that shares cognitive demands with code generation. Code Llama already understands variable binding, formal syntax, algorithmic thinking, and the translation between natural language specifications and formal implementations — all skills that transfer to mathematical reasoning. Starting from a code-capable model means the continued pretraining on math data doesn't need to teach these fundamentals from scratch. The paper's results support this: Code Llama 34B already achieves 12.2% on MATH and 29.6% on GSM8k (Table 1), indicating non-trivial mathematical capability before any math-specific training.

A crucial RoPE modification for the 7B model: Before training LLEMMA 7B, the authors contract the Rotary Position Embedding (RoPE) base period from $\theta = 1,000,000$ to $\theta = 10,000$ . RoPE (Rotary Position Embedding) is a method for encoding token positions in the attention mechanism by applying a rotation to the query and key vectors, where the rotation angle for position $p$ at dimension $i$ is $p \cdot \theta^{-2i/d}$ . The base period $\theta$ controls the wavelength of the position encoding — larger $\theta$ means longer wavelengths and better support for long-range position relationships.

Code Llama was trained with $\theta = 1,000,000$ to support its 16k context length (the larger base period stretches the position encodings so that positions far apart remain distinguishable). The LLEMMA authors contract $\theta$ to $10,000$ (the standard Llama 2 value) so that "the long context finetuning procedure described in Peng et al. (2023) and Rozière et al. (2023) can be repeated on the trained LLEMMA 7B" — essentially, they want to preserve the option to later extend LLEMMA 7B to long contexts using the same interpolation technique, and that technique assumes a baseline $\theta = 10,000$ . Because of compute constraints, they could not verify whether $\theta = 10,000$ caused a performance penalty for LLEMMA 34B, so they preserved the original $\theta = 1,000,000$ for the 34B model. This is a practical engineering decision driven by the desire for future flexibility, not a theoretically motivated choice.

Continued Pretraining Procedure

The training procedure is standard autoregressive language modeling — the model is trained to predict the next token given all previous tokens, using the cross-entropy loss, on the Proof-Pile-2 mixture. There is no novel training objective, no auxiliary losses, no curriculum learning, no reinforcement learning. The entire technical sophistication is in the data, not the training algorithm.

Training configuration for LLEMMA 7B:

Training tokens: 200B tokens (trained for 42,000 steps at a global batch size of 4 million tokens = $42,000 \times 4 \times 10^6 = 168$ B tokens — the paper reports 200B; the slight discrepancy may reflect that the batch size of 4M tokens is approximate or the scheduler was designed for 48,000 steps before NaN intervened)
Context length: 4096 tokens
Learning rate: warmed up to $1 \times 10^{-4}$ over 500 steps, then cosine decay to $1/30$ th of the maximum learning rate over 48,000 steps
Training duration: the model was trained for 42,000 steps out of a planned 48,000 steps; training was terminated early due to NaN losses after step 42,000, "likely caused by unstable optimization or hardware failures"
Hardware: 256 A100 40GB GPUs, using roughly 23,000 A100-hours
Parallelism: Tensor Parallelism with world size 2 (splitting each model across 2 GPUs), ZeRO Stage 1 sharded optimizer states across Data Parallel replicas, Flash Attention 2 for throughput and memory efficiency
Precision: bfloat16 mixed precision
RoPE adjustment: base period contracted from $\theta = 1,000,000$ to $\theta = 10,000$ before training began

Training configuration for LLEMMA 34B:

Training tokens: 50B tokens (trained for 12,000 steps at a global batch size of 4 million tokens = $12,000 \times 4 \times 10^6 = 48$ B tokens; the paper reports 50B)
Context length: 4096 tokens
Learning rate: warmed up to $5 \times 10^{-5}$ over 500 steps, then cosine decay to $1/30$ th of the peak learning rate
Hardware: 256 A100 40GB GPUs, using roughly 47,000 A100-hours
Parallelism: Tensor Parallelism with world size 8 (splitting each model across 8 GPUs), ZeRO Stage 1 sharded optimizer states across Data Parallel replicas, Flash Attention 2
Precision: bfloat16 mixed precision
RoPE: $\theta = 1,000,000$ preserved from Code Llama

Why different learning rates? The 7B model uses a peak learning rate of $1 \times 10^{-4}$ while the 34B model uses $5 \times 10^{-5}$ . This follows standard scaling practice: larger models typically use lower learning rates to avoid training instability. The paper does not describe learning rate tuning — it presents these values as the chosen configuration, likely based on the Code Llama or Llama 2 training recipes.

The NaN loss issue: The planned training duration was 48,000 steps for the 7B model, but NaN losses occurred at step 42,000. The authors attribute this to "unstable optimization or hardware failures" (citing Elsen et al., 2023, which discusses silent data corruption in large training runs). The model checkpoint at step 42,000 was used for all evaluations. This is a practical detail that matters for reproducibility — the paper is transparent that training didn't complete as planned, and the resulting model is from an earlier-than-intended checkpoint.

Why 200B tokens for 7B but only 50B tokens for 34B? The paper does not explain this asymmetry explicitly, but it follows the Minerva pattern (Minerva 8B was trained on 164B tokens, Minerva 62B on 109B tokens). The likely rationale is compute efficiency: larger models learn faster per token (in terms of loss reduction), so they need fewer tokens to reach comparable quality. The 7B model sees 200B tokens on top of its Code Llama initialization, while the 34B model sees only 50B additional tokens. Since the 34B model requires roughly 4.8× more compute per token (34/7 ≈ 4.86), training it for 200B tokens would cost approximately $4.86 \times 200/50 \approx 19.4$ times as much as the 7B training run — clearly prohibitive under the authors' compute budget.

Data Mixture Selection Methodology

The mixture weights — 2:4:1 for ArXiv:Web:Code (meaning ArXiv tokens are upweighted 2×, OpenWebMath tokens 4×, and AlgebraicStack tokens 1× relative to their raw token counts) — were not chosen arbitrarily. The paper describes a systematic selection procedure (Section 3.4):

Train several small models: Starting from Code Llama 7B, train for a reduced number of steps using different mixture weight ratios. The table in Section 3.4 reports on six candidate mixtures: 2:4:1, 2:4:2, 4:2:1, 4:2:2, 4:4:1, and 4:4:2 (all expressed as ArXiv:Web:Code ratios).
Evaluate perplexity on the MATH training set: After these short training runs, compute the model's perplexity on the MATH training set (the 7,500 training problems from Hendrycks et al., 2021b). Perplexity is the exponential of the average negative log-likelihood; lower perplexity means the model assigns higher probability to the correct next tokens in MATH solutions.
Select the lowest-perplexity mixture: The 2:4:1 mixture achieves the lowest overall MATH training set perplexity (1.478), beating 2:4:2 (1.482), 4:4:2 (1.485), 4:4:1 (1.487), 4:2:1 (1.487), and 4:2:2 (1.489).
Validate across MATH subtopics: Table 5 shows perplexity broken down by MATH subtopic (Prealgebra, Algebra, Number Theory, Counting & Probability, Geometry, Intermediate Algebra, Precalculus). The 2:4:1 mixture achieves the best or near-best perplexity on every subtopic, providing confidence that it's genuinely better rather than overfitting to one subtopic.

Why perplexity on the MATH training set as a selection criterion? Perplexity is a measure of how well the model's probability distribution matches the true distribution of the evaluation text. Using MATH data for mixture selection is a form of hyperparameter tuning on a downstream task, which the authors acknowledge: "Note that our methodology uses the MATH training set to determine a training hyperparameter, though we expect that the effect is similar to that of related high-quality texts." This means the MATH evaluation results may be slightly optimistic — the mixture weights were chosen in part because they performed well on MATH. However, since the mixture was selected based on perplexity (not task accuracy) and only on the training set (not the test set), the degree of overfitting is likely small. The authors also evaluate on GSM8k, OCWCourses, MMLU-STEM, and SAT (none of which were used for mixture selection), providing out-of-distribution validation of the chosen weights.

Interpreting the selected weights: The 2:4:1 ratio upweights web data (OpenWebMath) most aggressively, followed by papers (ArXiv), followed by code (AlgebraicStack). This reflects an empirical finding that the web data is highest-quality for the purpose of learning mathematical problem-solving — OpenWebMath contains worked examples, solutions, and explanations from forums like Math StackExchange and Art of Problem Solving, which are directly relevant to the MATH benchmark format. Code data, while valuable for tool use and formal mathematics, may be less directly useful for chain-of-thought problem solving, hence its lower weight. Papers (ArXiv) occupy a middle ground: they contain rigorous mathematics but are written in a different style (expository rather than problem-solution) and cover topics far beyond the scope of MATH.

Evaluation Methodology: Chain-of-Thought Problem Solving

The primary evaluation mode is few-shot chain-of-thought reasoning, following the Minerva protocol. The model is given a small number of worked examples (the "few-shot prompt") and then asked to solve a new problem, generating a complete solution step-by-step before producing a final answer.

MATH evaluation. The paper uses the 4-shot prompt from Minerva (Lewkowycz et al., 2022), which provides four examples of MATH problems with full chain-of-thought solutions. The model generates a solution ending with a final answer in a specific format ("Final Answer: The final answer is X"), which is extracted and compared to the reference answer. Answer checking uses exact string matching or SymPy equivalence (SymPy is a Python symbolic mathematics library; checking for equivalence means that mathematically equal expressions like 1/2 and 0.5 are considered matches even if they differ textually). The MATH test set contains 5,000 problems across seven subjects (Prealgebra, Algebra, Number Theory, Counting & Probability, Geometry, Intermediate Algebra, Precalculus) and five difficulty levels (1–5, where 5 is hardest).

GSM8k evaluation. The paper uses the 8-shot prompt from Wei et al. (2023), which provides eight examples of grade-school math word problems with step-by-step solutions. Answers are extracted and compared as numbers. GSM8k has 1,319 test problems.

OCWCourses evaluation. The prompt is the 4-shot prompt from Minerva. OCWCourses contains undergraduate-level STEM problems from MIT's OpenCourseWare.

MMLU-STEM evaluation. The paper uses the 4-shot chain-of-thought prompt from Minerva, applied to the 18 STEM subjects within the MMLU benchmark (out of 57 total subjects). MMLU is multiple-choice, so the model must select one of four options.

SAT evaluation. The authors created a custom dataset of 32 math questions from the May 2023 SAT that do not contain figures. This serves as a contemporaneous evaluation that postdates the model's April 2023 knowledge cutoff, making it a test of reasoning rather than memorization. The SAT is multiple-choice with four options.

Majority voting (maj@k). For MATH (k=256), GSM8k (k=100), and OCWCourses (k=100), the paper reports majority voting: generate k independent solutions and select the most common final answer. This technique, introduced by Wang et al. (2023) as "self-consistency," improves accuracy by reducing variance — even if most individual solutions are wrong, the correct answer may appear more frequently than any single wrong answer. The sampling uses temperature T=0.6 for k=256 and k=100, and T=0.3 for k=16 (used for MMLU-STEM and SAT), with nucleus sampling p=0.95 (only tokens in the top-p probability mass are considered, which prevents sampling very low-probability tokens that would produce degenerate text). Due to compute constraints, majority voting is not reported for Llama 2 and Code Llama baselines.

Why different sampling temperatures? Lower temperature (T=0.3) for MMLU-STEM and SAT produces less diverse outputs, which is appropriate for multiple-choice tasks where the model needs to converge on a single answer. Higher temperature (T=0.6) for MATH and GSM8k encourages exploration of different solution paths, which is useful for majority voting where diversity among the k samples increases the chance that at least some samples are correct.

Evaluation Methodology: Mathematical Problem Solving with Tool Use

The paper introduces a novel evaluation mode where the model solves problems by writing and executing Python code, rather than generating a text-only solution. This tests whether LLEMMA's training on AlgebraicStack code data translates to practical computational problem-solving.

MATH+Python. Given a MATH problem, the model is prompted to alternately describe a solution step in natural language, then execute that step by writing a Python code block. The final answer is a Python program whose execution produces a numeric type or SymPy object. The few-shot prompt includes examples that demonstrate using built-in numeric operations, the math module (providing standard mathematical functions), and SymPy (a symbolic mathematics library that can manipulate algebraic expressions, solve equations, compute integrals, etc.). The model must understand what computations can be delegated to code versus what reasoning should stay in natural language.

GSM8k+Python. The model solves a GSM8k word problem by writing a Python program that executes to an integer answer. The prompt is from Gao et al. (2023). This is a simpler task than MATH+Python because GSM8k problems translate more directly to arithmetic operations — the challenge is correctly parsing the word problem into a computation, not performing symbolic manipulation.

Why tool use matters. Tool use addresses a fundamental limitation of pure language model reasoning: language models are unreliable at arithmetic and symbolic computation because they generate tokens probabilistically rather than executing algorithms. By delegating computation to a Python interpreter (which performs exact arithmetic and follows deterministic rules), the model can leverage its strength (understanding the problem and deciding what to compute) while avoiding its weakness (actually computing). The fact that LLEMMA can do this few-shot, without any fine-tuning for tool use, demonstrates that the AlgebraicStack code data taught the model to generate syntactically correct, semantically appropriate Python for mathematical tasks.

Evaluation Methodology: Formal Theorem Proving

The paper evaluates LLEMMA on two formal mathematics tasks that test fundamentally different capabilities.

Informal-to-formal proving (Isabelle). This task, following Jiang et al. (2023), takes a problem expressed in informal mathematical language (LATEX), a human-written informal proof, and a formal statement in Isabelle syntax, and requires the model to generate a formal proof in Isabelle. The generated proof can contain calls to Sledgehammer (Isabelle's built-in automation that tries to prove subgoals using external theorem provers) and other automated heuristics.

The evaluation uses the miniF2F benchmark (Zheng et al., 2021), a dataset of 488 formal problem statements from mathematical Olympiads and undergraduate coursework, expressed in multiple proof assistant languages. For Isabelle, the paper uses the miniF2F-valid (validation) and miniF2F-test splits. The prompt consists of 11 examples (formal statement, informal statement, informal proof, formal proof) from Jiang et al. (2023), with 7 examples selected for number theory problems and 6 for all other subjects. The model generates one proof per problem via greedy decoding (no sampling, no search — just the single most likely token at each step).

The baseline is Sledgehammer alone (applied at the beginning of the proof without any language model guidance), which proves 14.72% of validation and 20.49% of test theorems. The model's generated proofs are checked by the Isabelle proof assistant through Portal-to-Isabelle (Jiang et al., 2021), with a 30-second timeout for Sledgehammer calls.

Formal-to-formal proving (Lean 4). This task involves generating a proof step-by-step by interacting with the Lean proof assistant. At each step, the proof assistant provides a tactic state — a representation of what remains to be proved, including all current hypotheses and the goal — and the model must generate a tactic (a command that advances the proof). The tactic is executed by the proof assistant, producing either a new tactic state (if the tactic was valid and made progress) or an error message (if the tactic was invalid). The process continues until either all goals are proved (success) or a timeout is reached (failure).

The evaluation uses best-first search, a standard algorithm for neural theorem proving. Best-first search maintains a priority queue of proof states, ranked by the model's log-probability of the tactic that led to that state. At each iteration, it pops the highest-scoring state, generates S candidate tactics from the model, executes each valid tactic to get new states, and pushes those new states onto the queue. The search is parameterized by N=1 attempt, S=32 generated tactics per iteration, and a maximum of T=100 iterations (the total search budget is N×S×T=3,200 generated tactics). A 10-minute timeout is enforced per theorem.

The prompt consists of just 3 (state, tactic) examples, making this a true few-shot evaluation — the model has seen essentially no Lean 4 tactic prediction examples during pretraining beyond what appears in the AlgebraicStack code data (which includes 285.6M tokens of Lean code, including proof steps with tactic states). The evaluation uses miniF2F test, LeanDojo v.1.1.2 for interaction (Yang et al., 2023), and beam search for tactic generation within each expansion step.

The baseline is ReProver (Yang et al., 2023), a model that was fine-tuned specifically for tactic prediction on Lean 3 and augmented with retrieval (it looks up relevant lemmas from a database). ReProver achieves 26.50% on miniF2F-test with a search budget of 1×64. LLEMMA-7B achieves 26.23% with a search budget of 1×32, which is remarkable because LLEMMA is using a 3-shot prompt with zero fine-tuning, operating in Lean 4 (a different version of Lean than ReProver trained on), and using a smaller search budget.

Why these two tasks test different things. Informal-to-formal proving tests the model's ability to translate human mathematical language into formal syntax — it's a translation task that requires understanding both the informal mathematics and the formal proof assistant's conventions. Formal-to-formal proving tests the model's ability to actually do mathematics within a formal system — it's a reasoning task that requires understanding the current proof state and selecting the right logical step to advance toward the goal. The fact that LLEMMA performs well on both tasks without fine-tuning suggests that continued pretraining on mathematical text and code teaches both the syntax of formal systems and the underlying mathematical reasoning patterns.

Memorization and Data Overlap Analysis Methodology

The paper includes a careful analysis of whether LLEMMA's performance on MATH could be inflated by memorization — specifically, whether test problems or their solutions appear verbatim in the training data.

30-gram overlap detection. The paper scans every 30-gram (sequence of 30 consecutive tokens) in MATH test problems and MATH test solutions against every document in OpenWebMath and AlgebraicStack. If a 30-gram from a test sequence appears in any training document, it's counted as a "hit." The choice of 30 tokens (roughly 120 characters or 2–3 sentences) is designed to be long enough that random collisions are extremely unlikely while short enough to catch partial overlaps.

Findings from 30-gram analysis. Approximately 7% of MATH test problem statements (348 out of ~5,000) have at least one 30-gram hit with an OpenWebMath document. About 0.6% of MATH test solutions (34 out of ~5,000) have hits. Hits between MATH and AlgebraicStack are negligible (3 problems, 1 solution). GSM8k shows even fewer hits (2 problems, 0 solutions for OpenWebMath; 0 for AlgebraicStack).

Manual inspection of problem-statement hits. The authors manually inspected 100 randomly sampled hits between MATH problem statements and OpenWebMath documents. The findings, detailed in Table 6 (right), reveal:

41% of the hits were to documents containing the problem statement but no solution — these were websites that list problems without answers, discussion forums where someone posed the question but got no response, or pages with hints but not full solutions. Simply seeing the problem during training doesn't help the model solve it unless it also sees the answer.
49% had an alternative solution to the ground-truth solution but with the same answer. These are documents where someone solved the problem differently than the MATH reference solution, or provided a solution with missing details, or discussed the problem and mentioned the answer. This is the most concerning category for memorization, since the model could theoretically reproduce the alternative solution. However, the paper notes that the model's generated solutions may not match these alternative solutions — the analysis only checks 30-gram overlap, not full solution equivalence.
9% had a missing or incorrect answer — the document discussed the problem but didn't provide the correct answer.
1% (exactly 1 out of 100) had the same solution as the MATH ground-truth.

Performance on hit vs. non-hit problems. Table 7 partitions LLEMMA-34B's accuracy by whether a 30-gram hit exists between the test problem (or solution) and any training document, broken down by MATH difficulty level. The results show no clear relationship:

On Level 1 (easiest), hit problems achieve 72.73% accuracy vs. 61.50% for non-hit problems — a 11-point gap that could indicate memorization benefit. However, there are only 11 hit problems at this level, making the comparison noisy.
On Level 2, hit problems achieve 35.71% vs. 40.18% non-hit — hit problems are worse.
On Level 3: 30.36% hit vs. 26.88% non-hit — a small gap.
On Level 4: 14.89% hit vs. 16.61% non-hit — hit problems are slightly worse.
On Level 5 (hardest): 6.08% hit vs. 6.39% non-hit — essentially identical, both very low.

The paper concludes that "a nontrivial match between a test example and a training document did not imply that the model generated a memorized correct answer." The low accuracy on hard problems regardless of overlap status is particularly telling — if the model were simply memorizing, we'd expect high accuracy on hit problems even at high difficulty levels, which is not what the data shows.

Generated solution overlap analysis. The authors also checked whether LLEMMA-34B's generated MATH solutions contain 30-grams that appear in OpenWebMath. Only 13 such hits were found across all generated solutions. The hits were mostly common number sequences (e.g., a list of Fibonacci numbers, which appear identically in many documents) plus one instance of factoring a polynomial. Figure 6 (Appendix H) shows examples of false positives when using shorter n-gram lengths — the 30-gram threshold appears well-calibrated to avoid these.

Limitations of the overlap analysis. The paper acknowledges that the 30-gram methodology gives "a lower bound on the number of semantically equivalent sequences" because it doesn't account for paraphrasing. A document could contain the same solution expressed in different words, and the 30-gram check would miss it. Similarly, the analysis only covers OpenWebMath and AlgebraicStack — hits with ArXiv or general-domain data are not checked. Despite these limitations, the analysis provides reasonable evidence that LLEMMA's MATH performance is not primarily driven by verbatim memorization of test problems or solutions.

Why this analysis matters. The memorization question is central to claims about reasoning capabilities. If a model has seen the exact test problems during training, high accuracy might reflect retrieval rather than reasoning. The paper's analysis suggests this is not the case for LLEMMA — most test problems have no substantial overlap with training data, and even when overlap exists, it doesn't predict high accuracy on hard problems. The presence of alternative solutions in training data (the 49% of hits with different solutions) is more nuanced — the model might learn solution patterns rather than specific solutions, which is actually the desired behavior for a model that generalizes.

4. Key Insights and Innovations

Innovation 1: Data Curation as the Primary Innovation for Domain-Specific Mathematical Language Models

The paper's most fundamental contribution is not architectural — it uses standard transformer models, standard autoregressive training, standard evaluation protocols. Rather, the paper demonstrates that carefully curating a multi-source, multi-formalism mathematical pretraining corpus is sufficient to produce a model with emergent cross-task mathematical capabilities that transfer to tool use and formal theorem proving without task-specific training. This is an intellectual shift from the prevailing assumption that mathematical reasoning requires either specialized architectures (tree search, symbolic modules, neuro-symbolic hybrids) or task-specific fine-tuning (supervised datasets, RL from verifier feedback, instruction tuning).

Before LLEMMA, the standard approach to building math-capable models fell into two camps. The first camp — exemplified by Minerva (Lewkowycz et al., 2022) — used continued pretraining on technical content but was closed, leaving open the question of whether the approach could be replicated with public data. The second camp — exemplified by WizardMath (Luo et al., 2023), MetaMath (Yu et al., 2023), and MAmmoTH (Yue et al., 2023) — used supervised fine-tuning on task-specific datasets to boost benchmark scores. The implicit message from this latter camp was that continued pretraining alone, without targeted fine-tuning, was insufficient for competitive mathematical reasoning.

LLEMMA refutes that implicit message. With zero supervised fine-tuning for math problem-solving, LLEMMA 34B achieves 25.0% on MATH greedy decoding and 43.1% with majority voting (Table 1, Table 2) — competitive with Minerva 62B (27.6% greedy, 43.4% maj@256) and dramatically ahead of generalist models like Llama 2 7B (3.2%). The model achieves these results purely from continued pretraining on Proof-Pile-2, with the same autoregressive objective used in standard language model training. This is significant because it establishes that data composition, not training methodology, is the binding constraint on open mathematical language models. The practical implication is that efforts to improve mathematical reasoning should prioritize better data curation (more diverse formalisms, higher-quality solutions, broader coverage of mathematical subfields) rather than more sophisticated training algorithms.

What makes this insight non-obvious is the specific data composition that works. The paper doesn't just dump 55B tokens of math content and call it done. The deliberate inclusion of mathematical code (AlgebraicStack's 11B tokens across 17 languages, including formal proof assistant code) alongside natural language math text (OpenWebMath's 15B tokens of forum discussions and worked solutions) and scientific papers (ArXiv's 29B tokens) creates a training signal that teaches the model about mathematical structure from multiple representational angles. The model sees the same concepts expressed as LaTeX equations in papers, as step-by-step solutions in web forums, as Python/SymPy code, and as Lean/Isabelle formal proofs — and from this multi-modal (in the representational sense, not the sensory sense) exposure, it learns to translate between formalisms and to apply mathematical reasoning in contexts it wasn't explicitly trained for. The emergence of few-shot formal theorem proving (Section 3.3) — where LLEMMA generates Lean tactics from just 3 examples — provides the strongest evidence for this cross-formalism transfer, since the model was never fine-tuned on tactic prediction and saw formal proof data as just another text modality during pretraining.

The paper also demonstrates that this approach scales: the 7B model trained on 200B tokens and the 34B model trained on 50B tokens both show substantial improvements over their Code Llama initializations, with the improvements being largest on tasks that most directly require mathematical reasoning (MATH: +13 points for 34B, GSM8k: +20 points for 7B; Table 1). This suggests that continued pretraining on domain-specific data is a general recipe, not a one-off result dependent on a particular model scale or hyperparameter configuration.

Innovation 2: The AlgebraicStack as the First Public, Large-Scale Dataset of Mathematical Code Spanning Numerical, Symbolic, and Formal Mathematics

The AlgebraicStack — 11B tokens of source code spanning 17 languages from Python and C++ to Lean, Isabelle, and Coq — represents a conceptual advance in what constitutes "mathematical training data" for language models. Prior to this work, mathematical pretraining datasets (including Minerva's undisclosed corpus) focused almost exclusively on natural language mathematics: textbooks, papers, forum discussions, and problem solutions. The AlgebraicStack argues — implicitly, through its composition and the downstream capabilities it enables — that executable mathematical code is a first-class modality for teaching mathematical reasoning, not merely an auxiliary data source.

The innovation here is not the existence of code data per se (Code Llama was trained on 500B tokens of code), but the specific curation of code that is mathematically motivated. The AlgebraicStack doesn't include general-purpose software engineering code. It filters aggressively for numerical computing (FFTW, GSL, LAPACK, Eigen, Armadillo), symbolic mathematics (SymPy), formal verification (Lean, Coq, Isabelle), and scientific simulation (Julia's DifferentialEquations, Turing, DynamicalSystems). The filtering is language-specific and multi-layered: Python files must import from a fixed list of scientific libraries; C files must include specific numerical library headers; Julia files are keyword-whitelisted for mathematical terms; TeX files must contain section/chapter structure and be identified as English. This is not a generic code corpus with math accidentally included — it's a deliberately constructed dataset where every file has been vetted for mathematical relevance.

The significance of this dataset extends beyond LLEMMA's immediate results. The AlgebraicStack establishes that formal proof assistant code (Lean, Isabelle, Coq) can be treated as pretraining data rather than requiring specialized architectures or training pipelines. Prior work on neural theorem proving (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022) trained small models specifically for tactic prediction, using specialized objectives and data formats. The AlgebraicStack includes proof states and tactic pairs as raw text, treating them identically to Python code or LaTeX — and yet LLEMMA-7B achieves 26.2% on miniF2F formal-to-formal proving with a 3-shot prompt (Table 4, right), comparable to ReProver (26.5%), a model specifically fine-tuned and retrieval-augmented for this exact task. This suggests that the boundary between "general mathematical knowledge" and "formal proof capability" is more porous than the field assumed — enough exposure to formal mathematics as text during pretraining can bootstrap competent formal reasoning without task-specific adaptation.

The dataset's release also lowers the barrier to entry for research on mathematical AI. Before the AlgebraicStack, training a model with exposure to formal mathematics required either proprietary data or laborious custom scraping. By providing 1.5B+ tokens of formal proof data (Lean + Isabelle + Coq) with documented filtering and decontamination procedures (including explicit removal of benchmark test theorems), the AlgebraicStack enables other researchers to replicate and extend LLEMMA's formal mathematics capabilities.

Innovation 3: Continued Pretraining on Domain-Specific Data as a Controllable and Reproducible Alternative to Supervised Fine-Tuning for Mathematical Reasoning

The paper makes a methodological contribution by systematically comparing continued pretraining to supervised fine-tuning as strategies for specializing language models to mathematics — and demonstrating that continued pretraining produces a more general, more transferable mathematical capability than fine-tuning on task-specific datasets, while remaining competitive on those specific tasks. This is not merely a performance claim (LLEMMA fine-tuned on MetaMathQA does outperform Llama 2 fine-tuned on MetaMathQA, Table 12) but a conceptual claim about the nature of the capability being built.

Supervised fine-tuning on math problem datasets (MetaMathQA, WizardMath) teaches the model to produce solutions in a specific format for a specific distribution of problems. The resulting model is a benchmark specialist — excellent at the task it was trained on, but potentially brittle when asked to use tools, generate formal proofs, or solve problems in different formats. Continued pretraining, by contrast, teaches the model a general facility with mathematical language, notation, and reasoning patterns by exposing it to a diverse distribution of mathematical text. The model learns that mathematics can be expressed as LaTeX, as Python, as Isabelle proofs, as forum discussions — and that the underlying reasoning transfers across these modalities.

The evidence for this claim comes from the breadth of LLEMMA's capabilities without task-specific training. The model simultaneously performs chain-of-thought problem solving (MATH, GSM8k, OCWCourses, MMLU-STEM, SAT), computational tool use (MATH+Python, GSM8k+Python), and formal theorem proving (Isabelle informal-to-formal, Lean formal-to-formal). Each of these tasks requires different output formats, different reasoning strategies, and different background knowledge. A model fine-tuned on MetaMathQA would not be expected to generate valid Lean tactics or call SymPy from Python — those capabilities simply aren't present in the fine-tuning data. LLEMMA's ability to do all of these tasks from few-shot prompts demonstrates that continued pretraining produces a unified mathematical capability that transfers across tasks, rather than a collection of task-specific skills.

This insight has practical implications for how researchers should approach domain specialization. The supervised fine-tuning approach is appealing because it's cheaper (MetaMathQA is 395K examples; Proof-Pile-2 is 55B tokens) and directly optimizes benchmark metrics. But the resulting model is a dead end for research — it can solve MATH problems but can't be used for theorem proving, tool use, or any task whose format doesn't match the fine-tuning distribution. Continued pretraining, despite being more expensive, produces a model that can serve as a platform for diverse downstream applications. The paper's release of both the base model and the Proof-Pile-2 dataset makes this platform available to the entire research community.

Innovation 4: A Principled Methodology for Data Mixture Selection Using Downstream Perplexity as a Proxy for Task Performance

The paper introduces a small but methodologically significant innovation in how it selects the mixture weights for Proof-Pile-2's components. Rather than choosing weights based on intuition, prior conventions, or equal weighting, the authors conduct a controlled experiment across six candidate mixtures (Table 5), training small models to a reduced number of steps from the Code Llama 7B initialization, and selecting the mixture that minimizes perplexity on the MATH training set. The selected mixture (2:4:1 for ArXiv:Web:Code, meaning OpenWebMath is upweighted 4× relative to AlgebraicStack and ArXiv is upweighted 2×) is then validated across MATH subtopics to ensure the selection isn't driven by a single subject.

This approach matters because data mixture is one of the most consequential and least principled hyperparameters in language model training. Standard practice ranges from heuristic upweighting based on perceived "quality" (Brown et al., 2020; Gao et al., 2020) to automated methods like DoReMi (Xie et al., 2023) that optimize mixture weights during training. The paper's methodology occupies a pragmatic middle ground: it's more systematic than heuristic selection (testing six candidate mixtures rather than picking one by intuition) but more practical than full online optimization (requiring only short training runs and perplexity evaluation). The key insight is that perplexity on a high-quality held-out set (the MATH training set) correlates with downstream task performance for domain-specific continued pretraining, at least when the held-out set is representative of the target domain.

The authors are appropriately cautious about this methodology, noting that it "uses the MATH training set to determine a training hyperparameter" and that this could introduce overfitting. However, the fact that LLEMMA also improves on GSM8k, OCWCourses, MMLU-STEM, SAT, and formal theorem proving — none of which were used for mixture selection — provides out-of-distribution validation that the selected mixture weights genuinely produce better mathematical capability rather than just better MATH scores.

This contribution is incremental rather than fundamental, but it provides a replicable methodology for other researchers undertaking domain-specific continued pretraining. The approach can be applied to any domain where a representative held-out text corpus exists: select candidate mixtures, train small proxy models, evaluate perplexity on the held-out corpus, and scale the winning mixture to full training.

Innovation 5: Evidence That Mathematical Performance Gains from Domain Adaptation Are Not Primarily Due to Benchmark Memorization

The paper provides a careful and transparent analysis of data overlap between the Proof-Pile-2 training corpus and the MATH evaluation set, finding that approximately 7% of MATH test problem statements have 30-gram overlap with OpenWebMath documents, but that this overlap does not predict model accuracy — particularly on hard problems where accuracy remains low regardless of overlap status (Table 7). This finding is not itself a methodological innovation, but it provides an important empirical boundary condition on the paper's claims: LLEMMA's mathematical capabilities are not explained by having seen the test problems during training.

What makes this analysis intellectually distinctive is how it handles the "alternative solution" problem. The manual inspection of 100 problem-statement hits (Table 6, right) reveals that 49% of hits are to documents containing a different solution with the same answer, not the MATH ground-truth solution. This is the most nuanced form of potential data contamination — the model hasn't seen the exact test solution, but it has seen someone solve the same problem. The paper's analysis treats this honestly, reporting the numbers rather than hiding them, and the subsequent accuracy analysis (Table 7) provides reassurance that even when the model saw the problem (potentially with a solution) during training, it doesn't automatically get the answer right — especially on hard problems where the accuracy on hit problems (6.08% for Level 5) is essentially identical to non-hit problems (6.39%).

This analysis matters because the question of data contamination has become central to evaluating language model capabilities. As training corpora grow to encompass larger fractions of the public web, the probability that evaluation benchmarks are included increases, making it difficult to distinguish genuine reasoning from memorization. The paper's methodology — n-gram overlap detection, manual inspection of hit types, and performance stratification by overlap status — provides a template for how future work can address this question systematically rather than hand-waving it away. The specific finding that alternative solutions are common in web-derived training data (49% of hits) but don't confer a consistent accuracy advantage suggests that exposure to solution patterns, not exposure to specific test instances, drives the performance gains from continued pretraining — which is exactly what one would hope from a model that is learning to reason rather than memorize.

5. Experimental Analysis

Evaluation Methodology

Datasets. The paper evaluates on five mathematical reasoning benchmarks: MATH (Hendrycks et al., 2021b) with 12.5k problems divided into 7.5k training and 5k test, spanning seven subjects and five difficulty levels; GSM8k (Cobbe et al., 2021) with 1,319 test problems of middle-school math word problems; OCWCourses (Lewkowycz et al., 2022), a collection of undergraduate-level STEM problems from MIT's OpenCourseWare; MMLU-STEM, an 18-subject subset of the MMLU benchmark (Hendrycks et al., 2021a) focused on science and math; and a custom SAT dataset of 32 math questions from the May 2023 College Board exam, created to postdate the model's April 2023 knowledge cutoff. For tool use, MATH+Python and GSM8k+Python tasks use the same problem sets but with program-based answer generation. For formal theorem proving, miniF2F (Zheng et al., 2021) provides 488 formalized problem statements from Olympiads and undergraduate coursework, evaluated in both Isabelle (informal-to-formal) and Lean 4 (formal-to-formal) environments.
Base model(s). The primary models are LLEMMA 7B and LLEMMA 34B, decoder-only transformers produced by continuing pretraining of Code Llama (Rozière et al., 2023) on Proof-Pile-2. Code Llama itself was initialized from Llama 2 (Touvron et al., 2023) and further trained on 500B tokens of code. The choice of Code Llama as initialization is motivated by the intuition that code generation capabilities transfer to mathematical reasoning — the 34B Code Llama achieves 12.2% on MATH before any math-specific training (Table 1), demonstrating non-trivial mathematical capability from code pretraining alone. Comparisons also include Llama 2 as the pre-code baseline, and Minerva (Lewkowycz et al., 2022) at 8B, 62B, and 540B parameter scales as the closed-source state-of-the-art for mathematical language models.
Metrics. The primary metric across all chain-of-thought evaluations is accuracy — the fraction of test problems for which the model's final answer matches the reference answer. For MATH, answer matching uses exact string comparison or SymPy equivalence (mathematically equivalent expressions like 1/2 and 0.5 are considered matches). For GSM8k, answers are matched as numeric values. For MMLU-STEM and SAT, which are multiple-choice, the model must select one of four options. For majority voting experiments, the metric is maj@k — the accuracy achieved by selecting the most common answer among k independently sampled solutions. For formal theorem proving, the metric is proof success rate — the fraction of theorems for which the model produces a proof accepted by the proof assistant within the timeout (30 seconds for Sledgehammer calls in Isabelle, 10 minutes total per theorem in Lean). For data mixture selection, the metric is perplexity on the MATH training set — the exponential of the average negative log-likelihood, measuring how well the model's probability distribution matches the evaluation text.
Baselines. The paper compares against: (1) Llama 2 (Touvron et al., 2023) at 7B parameters, the general-domain pretrained model underlying Code Llama; (2) Code Llama (Rozière et al., 2023) at 7B and 34B parameters, the direct initialization from which LLEMMA was trained; (3) Minerva (Lewkowycz et al., 2022) at 8B, 62B, and 540B parameters, the closed-source mathematical language model that established the continued pretraining paradigm; (4) Sledgehammer (Paulson & Nipkow, 2023), Isabelle's built-in automation that calls external theorem provers, evaluated on the informal-to-formal proving task; (5) ReProver (Yang et al., 2023), a retrieval-augmented model fine-tuned for tactic prediction in Lean 3, evaluated on formal-to-formal proving; (6) COPRA (Thakur et al., 2023), a GPT-4-based method using retrieval and sampling for theorem proving. For the supervised finetuning experiment in Appendix G, baselines include WizardMath (Luo et al., 2023) and MetaMath (Yu et al., 2023) applied to Llama 2 7B and 70B.
Generation budget / compute accounting. For chain-of-thought evaluations with greedy decoding, the generation budget is exactly 1 solution per problem — the model generates a single output via argmax decoding (no sampling). For majority voting, the budget is k solutions per problem: k=256 for MATH, k=100 for GSM8k and OCWCourses, and k=16 for MMLU-STEM and SAT. For tool use tasks, a single program is generated and executed per problem. For informal-to-formal proving, exactly one proof is generated per theorem via greedy decoding (pass@1). For formal-to-formal proving in Lean, the budget is the search budget: N×S×T = 1×32×100 = 3,200 generated tactics, with N=1 attempt, S=32 tactics per expansion, and T=100 maximum iterations. Total compute is also reported as GPU-hours: 23,000 A100-hours for LLEMMA 7B training (200B tokens) and 47,000 A100-hours for LLEMMA 34B training (50B tokens). The paper does not perform FLOPs-matched comparisons between pretraining and inference compute, focusing instead on parameter-matched and compute-budget comparisons between models.
Cross-validation / statistical protocol. No cross-validation is used for the primary evaluations — results are reported on standard test splits (MATH test, GSM8k test, miniF2F test, custom SAT dataset). The data mixture selection process (Section 3.4) uses the MATH training set to evaluate perplexity of candidate mixtures, which the authors acknowledge "uses the MATH training set to determine a training hyperparameter." For the memorization analysis, 100 hits between MATH problem statements and OpenWebMath documents are randomly sampled and manually inspected, with results categorized into four types (no solution, alternative solution/same answer, missing or incorrect answer, same solution). Statistical significance tests are not reported, and confidence intervals are not provided for any accuracy numbers. For majority voting, the sampling temperature and nucleus sampling parameters (T=0.6 and p=0.95 for MATH and GSM8k with k≥100; T=0.3 and p=0.95 for MMLU and SAT with k=16) are specified, but variance across different sampling runs is not reported.

Main Quantitative Results

Chain-of-Thought Mathematical Problem Solving (Greedy Decoding)

The central results appear in Table 1, comparing LLEMMA, Code Llama, Llama 2, and Minerva on five benchmarks under greedy decoding (single solution per problem, no sampling):

MATH: LLEMMA 7B achieves 18.0%, improving 13.5 percentage points over Code Llama 7B (4.5%) and 14.8 points over Llama 2 7B (3.2%). LLEMMA 7B outperforms the proprietary Minerva 8B (14.1%) by 3.9 points. LLEMMA 34B achieves 25.0%, improving 12.8 points over Code Llama 34B (12.2%). Minerva 62B achieves 27.6% and Minerva 540B achieves 33.6%. The gap between LLEMMA 34B and Minerva 62B (25.0% vs. 27.6%) is 2.6 percentage points despite Minerva using roughly 1.8× more parameters, suggesting favorable parameter efficiency for LLEMMA on MATH.

GSM8k: LLEMMA 7B achieves 36.4%, a 25.9-point improvement over Code Llama 7B (10.5%) — the largest absolute improvement across all benchmarks. LLEMMA 34B achieves 51.5%, improving 21.9 points over Code Llama 34B (29.6%). Minerva 62B achieves 52.4% and Minerva 540B achieves 58.8%. LLEMMA 34B (51.5%) is within 0.9 points of Minerva 62B (52.4%), again showing strong parameter efficiency. Notably, Code Llama 7B (10.5%) actually scores lower than Llama 2 7B (11.8%) on GSM8k, suggesting that code pretraining alone can slightly degrade performance on some reasoning benchmarks — an effect that continued pretraining on math data fully reverses.

OCWCourses: All absolute accuracies are low (3.7%–12.0%), reflecting the difficulty of undergraduate STEM problems. LLEMMA 7B achieves 7.7%, improving 3.3 points over Code Llama 7B (4.4%). LLEMMA 34B achieves 11.8%, improving 4.8 points over Code Llama 34B (7.0%). Minerva 62B achieves 12.0% and Minerva 540B achieves 17.6%.

MMLU-STEM: LLEMMA 7B achieves 37.7%, improving 12.6 points over Code Llama 7B (25.1%). LLEMMA 34B achieves 49.0%, improving 8.5 points over Code Llama 34B (40.5%). Minerva 62B achieves 53.9% and Minerva 540B achieves 63.9%. The paper notes that Code Llama 7B (25.1%) performs at roughly random guessing (25% for 4-option multiple choice), largely because it "fail[s] to conclude its chain of thought with a valid answer" — suggesting that code pretraining disrupts the model's ability to format multiple-choice responses, a problem that math continued pretraining partially repairs.

SAT (May 2023): LLEMMA 7B achieves 53.1%, a remarkable 43.7-point improvement over Code Llama 7B (9.4%) — the largest percentage-point gain on any benchmark. LLEMMA 34B achieves 71.9%, improving 31.3 points over Code Llama 34B (40.6%). No Minerva comparisons are available for SAT (Minerva did not report this benchmark). Since the SAT postdates LLEMMA's April 2023 knowledge cutoff, these results cannot be attributed to memorization of test questions. Code Llama 7B's 9.4% on SAT (well below 25% random guessing for 4-option multiple choice) again reflects the model's difficulty producing valid answer formats, which continued pretraining dramatically resolves.

Key pattern across benchmarks: LLEMMA improves over Code Llama on every benchmark, with the largest absolute gains on tasks requiring step-by-step reasoning from natural language problem statements (GSM8k: +25.9 points for 7B, +21.9 for 34B) and the smallest gains on tasks requiring broad undergraduate knowledge (MMLU-STEM: +12.6 points for 7B, +8.5 for 34B). This pattern is consistent with continued pretraining primarily teaching reasoning patterns rather than factual knowledge — GSM8k problems are procedurally simple but require translating word problems into equations, while MMLU-STEM includes knowledge-recall questions that no amount of reasoning training can address if the model hasn't seen the relevant facts.

Majority Voting Results

Table 2 reports maj@k accuracy where the model samples k independent solutions (at non-zero temperature) and selects the most common final answer.

MATH (maj@256): LLEMMA 7B achieves 33.5%, a 15.5-point improvement over greedy decoding (18.0% → 33.5%), demonstrating that the model generates correct solutions at a non-trivial rate that majority voting can surface. LLEMMA 34B achieves 43.1%, improving 18.1 points over greedy (25.0% → 43.1%). Critically, LLEMMA 34B at 43.1% effectively matches Minerva 62B at 43.4% — a difference of 0.3 percentage points — despite LLEMMA being roughly 1.8× smaller in parameter count. Minerva 540B reaches 50.3%. Minerva 8B achieves 25.4%, which LLEMMA 7B exceeds by 8.1 points at half the parameter count (7B vs. 8B).

GSM8k (maj@100): LLEMMA 7B achieves 54.0%, improving 17.6 points over greedy (36.4% → 54.0%). LLEMMA 34B achieves 69.3%, improving 17.8 points over greedy (51.5% → 69.3%). Minerva 62B achieves 68.5% — LLEMMA 34B (69.3%) slightly exceeds it by 0.8 points. Minerva 540B reaches 78.5%.

OCWCourses (maj@100): LLEMMA 7B achieves 14.3%, improving 6.6 points over greedy (7.7% → 14.3%). LLEMMA 34B achieves 18.4%, improving 6.6 points over greedy (11.8% → 18.4%). Minerva 62B achieves 23.5% and Minerva 540B reaches 30.8%.

MMLU-STEM (maj@16): LLEMMA 7B achieves 49.9%, improving 12.2 points over greedy (37.7% → 49.9%). LLEMMA 34B achieves 59.7%, improving 10.7 points over greedy (49.0% → 59.7%). Minerva 62B achieves 63.5% and Minerva 540B reaches 75.0%.

SAT (maj@16): LLEMMA 7B achieves 78.1%, improving 25.0 points over greedy (53.1% → 78.1%). LLEMMA 34B achieves 81.3%, improving 9.4 points over greedy (71.9% → 81.3%). No Minerva comparisons are available.

Interpretation of majority voting gains: The improvement from greedy to majority voting ranges from 15.5 points (MATH 7B) to 25.0 points (SAT 7B), confirming that LLEMMA's sampling distribution contains correct solutions at substantially higher rates than greedy decoding alone reveals. The saturating pattern — the 34B model gains less from majority voting on some tasks (SAT: +9.4 for 34B vs. +25.0 for 7B; MMLU: +10.7 vs. +12.2) — suggests that the larger model's greedy solutions are already closer to the mode of the correct-answer distribution, leaving less room for majority voting to improve. The near-parity with Minerva 62B on MATH and GSM8k (differences of 0.3 and 0.8 points, respectively) is the headline finding: an open 34B model achieves closed 62B performance through continued pretraining alone, without task-specific fine-tuning.

Mathematical Problem Solving with Tool Use

Table 3 reports pass@1 (single generated program, executed, answer checked) for MATH+Python and GSM8k+Python.

GSM8k+Python: LLEMMA 7B achieves 40.1%, improving 13.0 points over Code Llama 7B (27.1%). LLEMMA 34B achieves 62.6%, improving 9.9 points over Code Llama 34B (52.7%). Notably, both models perform better with Python tool use than with chain-of-thought greedy decoding (7B: 40.1% vs. 36.4%, a 3.7-point gain; 34B: 62.6% vs. 51.5%, an 11.1-point gain). This is expected for GSM8k, where the problems translate naturally to arithmetic operations — writing and executing code avoids the arithmetic errors that language models make when computing step-by-step in text.

MATH+Python: LLEMMA 7B achieves 21.5%, improving 4.3 points over Code Llama 7B (17.2%). LLEMMA 34B achieves 27.1%, improving 3.6 points over Code Llama 34B (23.5%). Compared to chain-of-thought greedy decoding, MATH+Python improves performance for both LLEMMA models (7B: 18.0% → 21.5%, +3.5 points; 34B: 25.0% → 27.1%, +2.1 points), though the gains are smaller than for GSM8k. This likely reflects that MATH problems require symbolic manipulation (algebra, calculus, number theory) that is harder to fully automate with Python than arithmetic word problems — the model must decide when to use code versus natural language reasoning.

Interpretation: The tool use results demonstrate that LLEMMA's AlgebraicStack training transfers to practical program-based problem solving without any fine-tuning for tool use. The fact that both LLEMMA 7B and 34B exceed their chain-of-thought performance with tool use (particularly for GSM8k) provides evidence that the AlgebraicStack code data teaches the model to recognize when computation is appropriate — a metacognitive skill that goes beyond simply generating correct Python syntax.

Formal Theorem Proving

Isabelle informal-to-formal proving (Table 4, left). LLEMMA-7b achieves 22.13% on miniF2F-test, improving 4.51 points over Code Llama 7b (17.62%) and 1.64 points over Sledgehammer alone (20.49%). LLEMMA-34b achieves 21.31% on miniF2F-test, improving 3.28 points over Code Llama 34b (18.03%). On miniF2F-valid, LLEMMA-7b achieves 20.60% (vs. Code Llama 7b at 16.31% and Sledgehammer at 14.72%), and LLEMMA-34b achieves 21.03% (vs. Code Llama 34b at 18.45%).

Union of Sledgehammer and LLEMMA. The paper reports (Appendix F, Table 11) that the union of theorems proved by Sledgehammer and LLEMMA-7b is substantially larger than either alone: on miniF2F-valid, the union covers 25.97% (vs. 14.72% for Sledgehammer alone and 20.60% for LLEMMA alone), indicating that the two methods prove complementary sets of theorems — LLEMMA proves theorems that automated provers cannot handle, and vice versa. On miniF2F-test, the union covers 27.46% (vs. 20.49% for Sledgehammer and 22.13% for LLEMMA), yielding a 7-point improvement over Sledgehammer alone.

Lean 4 formal-to-formal proving (Table 4, right). LLEMMA-7b achieves 26.23% on miniF2F-test using best-first search with a budget of 1 attempt × 32 generations per iteration, improving 5.74 points over Code Llama 7b (20.49% with 1×32). LLEMMA-34b achieves 25.82% with 1×32 (vs. Code Llama 34b at 22.13%). The baseline ReProver (Yang et al., 2023) achieves 26.50% with 1×64 — a fine-tuned, retrieval-augmented model operating on Lean 3. LLEMMA-7b achieves 0.27 points below ReProver while using half the search budget (32 generations per iteration vs. 64) and requiring zero fine-tuning (3-shot prompting only). COPRA (Thakur et al., 2023), a GPT-4-based method using retrieval and up to 60 samples, achieves 23.36%.

Interpretation of formal mathematics results. The most significant finding is that LLEMMA-7b, with a 3-shot prompt and no fine-tuning, achieves performance comparable to ReProver — a model that was specifically fine-tuned on Lean tactic prediction and augmented with lemma retrieval. This provides the strongest evidence in the paper for LLEMMA's cross-task transfer from continued pretraining: the model learned enough about formal mathematics from reading AlgebraicStack code (including 285.6M tokens of Lean) to perform competent tactic prediction in a proof assistant it was never fine-tuned for. The fact that LLEMMA proves theorems complementary to Sledgehammer (Table 11) suggests the model's mathematical reasoning covers different problem types than automated theorem provers, making it a useful component in a hybrid proving system.

Data Mixture Selection Results

Section 3.4 and Table 5 present the controlled experiment comparing six candidate data mixture ratios for the Proof-Pile-2 components (expressed as arXiv:Web:Code ratios). The models are Code Llama 7B trained for a reduced number of steps on each mixture, evaluated by perplexity on the MATH training set.

The 2:4:1 mixture achieves the lowest overall perplexity (1.478), beating 2:4:2 (1.482), 4:4:2 (1.485), 4:4:1 (1.487), 4:2:1 (1.487), and 4:2:2 (1.489). The ranking is consistent across MATH subtopics: 2:4:1 achieves the best or near-best perplexity on all seven subjects (Prealgebra, Algebra, Number Theory, Counting & Probability, Geometry, Intermediate Algebra, Precalculus). The largest gaps between 2:4:1 and the worst-performing mixture within each subtopic are roughly 0.02–0.03 nats, which is small in absolute terms but consistent enough across subtopics to provide confidence in the selection.

The key design insight from these results is that OpenWebMath (the "Web" component) should be upweighted most aggressively (4×), ArXiv upweighted moderately (2×), and AlgebraicStack kept at baseline weight (1×). This suggests that web data — which contains worked problem solutions, forum discussions, and step-by-step explanations — is highest-quality for learning mathematical problem-solving patterns, while code data is less directly useful for chain-of-thought reasoning (but essential for tool use and formal mathematics, as Sections 3.2 and 3.3 demonstrate). The paper does not ablate the individual subcomponents of AlgebraicStack (e.g., removing Lean data, removing Python data) to isolate their effects on downstream tasks, which would be a natural extension.

Supervised Fine-Tuning Results

Appendix G and Table 12 report preliminary experiments fine-tuning LLEMMA-7B on MetaMathQA (Yu et al., 2023), a supervised dataset of 395K question-answer pairs targeted at MATH and GSM8k.

MATH after fine-tuning: LLEMMA 7B achieves 25.2%, compared to Llama 2 7B fine-tuned on MetaMathQA (19.4%) and Llama 2 7B fine-tuned on WizardMath (10.7%). The 5.8-point improvement over the Llama 2 MetaMathQA baseline demonstrates that LLEMMA's continued pretraining advantage persists even after task-specific fine-tuning — the better base model produces a better fine-tuned model.

GSM8k after fine-tuning: LLEMMA 7B achieves 66.5%, essentially tied with Llama 2 7B fine-tuned on MetaMathQA (66.4%) and substantially ahead of WizardMath (54.9%). The near-parity on GSM8k suggests either that MetaMathQA fine-tuning saturates GSM8k performance for 7B models (around 66%), or that GSM8k is simple enough that base model quality matters less after extensive task-specific fine-tuning. Llama 2 70B fine-tuned on MetaMathQA reaches 82.3% on GSM8k, indicating that scale still provides benefits beyond what fine-tuning alone achieves.

Context: These fine-tuning results are explicitly presented as preliminary ("a full exploration of finetuning applications... are outside the scope of this work"). The hyperparameters follow Yu et al. (2023) exactly, and the results are quoted from the literature for all non-LLEMMA models. The purpose is to establish that LLEMMA "retains its advantage over other open models when finetuned," not to claim state-of-the-art fine-tuning performance.

Ablation Studies and Robustness Checks

Data mixture ratio (arXiv:Web:Code): The controlled experiment in Table 5 comparing six mixture ratios represents the paper's primary ablation. The finding — that a 2:4:1 ratio minimizes MATH training set perplexity — is robust across all seven MATH subtopics, with the 2:4:1 mixture achieving the lowest or tied-for-lowest perplexity on every subject. The narrow range of perplexities across mixtures (1.478–1.489, a spread of only 0.011 nats) suggests that the exact mixture ratio matters less than the presence of all three components, though the paper doesn't include a "leave one out" ablation (e.g., arXiv only, Web only, Code only) to test this directly. The paper also does not ablate the 95%/5% split between Proof-Pile-2 and general-domain data, though this follows the Minerva recipe where Lewkowycz et al. (2022) presumably tuned this ratio.

RoPE base period (7B vs. 34B): The 7B model uses a contracted RoPE base period of θ=10,000 (down from Code Llama's θ=1,000,000), while the 34B model preserves θ=1,000,000. The paper states that "due to compute constraints, we were unable to verify that training LLEMMA 34B with a contracted RoPE base period did not come with a performance penalty" (Section 2.2). This is effectively an unintentional ablation — the two models use different position encoding wavelengths — but the paper does not analyze whether this contributes to the performance differences between the 7B and 34B models. The fact that both models improve substantially over their Code Llama baselines despite different RoPE settings suggests the RoPE choice is not critical for the main findings, but a controlled comparison would have been informative.

Training duration (7B model): The 7B model was trained for 42,000 steps (200B tokens) rather than the planned 48,000 steps, terminated early due to NaN losses. The paper uses the step-42,000 checkpoint for all evaluations. This is not presented as an ablation, but it effectively tests whether training beyond 42,000 steps would have improved performance — the paper doesn't know, since the NaN prevented further training. The results should be interpreted as from a possibly undertrained model, and the paper's reported improvements over Code Llama are therefore conservative (a fully trained model might have performed better).

Model scale (7B vs. 34B): The paper trains two model sizes with different training budgets (200B tokens for 7B, 50B tokens for 34B) and different RoPE settings, making the comparison between 7B and 34B models confounded by multiple variables. However, the consistent pattern across all benchmarks — the 34B model outperforms the 7B model on every task — provides evidence that model scale benefits mathematical reasoning, even with less training data. The largest gaps between 34B and 7B occur on GSM8k (51.5% vs. 36.4% greedy, a 15.1-point gap) and SAT (71.9% vs. 53.1%, an 18.8-point gap), while the smallest gaps occur on OCWCourses (11.8% vs. 7.7%, a 4.1-point gap) — suggesting that scale is most beneficial when the task requires multi-step reasoning that benefits from larger model capacity.

Memorization vs. reasoning (hit vs. non-hit analysis): The analysis in Section 3.5 partitions LLEMMA-34B's MATH accuracy by whether a 30-gram overlap exists between the test example (problem or solution) and Proof-Pile-2 training documents. The finding — no clear relationship between overlap status and accuracy, particularly on hard problems where accuracy is uniformly low (Level 5: 6.08% hit vs. 6.39% non-hit) — serves as a robustness check against the concern that LLEMMA's performance is driven by memorization. However, this analysis only covers OpenWebMath and AlgebraicStack, not ArXiv or general-domain data, and the 30-gram methodology misses semantically equivalent paraphrases. The paper acknowledges these limitations and frames the analysis as a "lower bound" on true overlap.

n-gram length for overlap detection: The paper uses 30-gram overlap as the primary threshold but also notes that "repeating our analysis with 20-gram hits and our findings were similar, though with false positives" (Section 3.5). Figure 6 in Appendix H provides concrete examples of false positives at shorter n-gram lengths: a 10-gram match finds a common LaTeX matrix pattern, a 20-gram match finds a similar problem statement with different numbers, and a 30-gram match finds a model-generated list of integers 1–100 that appears in a completely unrelated document. This sensitivity analysis validates the 30-gram threshold as long enough to avoid spurious collisions while short enough to catch partial overlaps.

Few-shot prompt sensitivity: The paper uses fixed prompts for each evaluation (4-shot for MATH, 8-shot for GSM8k, 3-shot for Lean tactic prediction, 11-shot for Isabelle autoformalization) but does not ablate the number of few-shot examples or test sensitivity to prompt format. For the Isabelle task, the prompts are subset-specific (7 examples for number theory, 6 for others). The paper does not report whether different prompt configurations yield substantially different results, which is a standard robustness check for few-shot evaluations.

Critical Assessment

Claim 1: "LLEMMA outperforms all known open base models, as well as the unreleased Minerva model suite on an equi-parameter basis" (Abstract, Section 1).

The experiments partially support this claim. On MATH with greedy decoding, LLEMMA 7B (18.0%) does outperform Minerva 8B (14.1%) by 3.9 points (Table 1) — this is a clean equi-parameter comparison in LLEMMA's favor. With majority voting, the advantage is larger: LLEMMA 7B maj@256 (33.5%) vs. Minerva 8B maj@256 (25.4%), an 8.1-point gap (Table 2). On GSM8k, LLEMMA 34B greedy (51.5%) is within 0.9 points of Minerva 62B (52.4%), and with majority voting, LLEMMA 34B maj@100 (69.3%) slightly exceeds Minerva 62B (68.5%).

However, "on an equi-parameter basis" requires careful interpretation. The 7B comparison works cleanly (LLEMMA 7B vs. Minerva 8B — close enough in scale). There is no Minerva model near 34B parameters (the closest is 62B), so the "equi-parameter" claim for the 34B model relies on extrapolation: LLEMMA 34B nearly matches Minerva 62B despite being 1.8× smaller. This is parameter-efficient but not literally equi-parameter. The paper does not report a Minerva 34B for direct comparison, so we cannot know whether LLEMMA 34B would outperform or underperform a Minerva of the same size. The claim is better stated as "LLEMMA achieves performance competitive with Minerva at smaller parameter counts" rather than "outperforms on an equi-parameter basis."

A genuine weakness: Minerva was trained on PaLM (a different base architecture with different pretraining data), while LLEMMA trains on Code Llama (which inherits from Llama 2). The paper does not control for base model quality — if Llama 2 + code pretraining is a stronger starting point than PaLM for mathematical reasoning, LLEMMA's advantage might reflect initialization rather than Proof-Pile-2's superiority over the Minerva dataset. An ablation comparing LLEMMA trained on the Minerva dataset (if it were available) or Minerva trained on Proof-Pile-2 (impossible since Minerva is closed) would be needed to isolate the data effect.

Claim 2: "LLEMMA is capable of tool use and formal theorem proving without any further finetuning" (Abstract, Section 3.2, Section 3.3).

Strongly supported for tool use. Both MATH+Python and GSM8k+Python show clear improvements over Code Llama baselines (Table 3), with the 34B model achieving 62.6% on GSM8k+Python — substantially above its chain-of-thought greedy performance (51.5%). The few-shot prompts provide examples of tool use, but the model receives no gradient updates for this capability — it emerges from continued pretraining on AlgebraicStack.

Supported with qualifications for formal theorem proving. LLEMMA-7b achieves 26.23% on Lean 4 formal-to-formal proving with a 3-shot prompt (Table 4), comparable to ReProver (26.50%) — a model fine-tuned for this exact task. This is an impressive demonstration of cross-task transfer. However, the evaluation uses only miniF2F (488 theorems), a search budget of only 1×32, and a 10-minute timeout. The paper does not report results with larger search budgets (which might benefit LLEMMA further, or might reveal that it plateaus while ReProver continues to improve with more search), nor does it evaluate on other formal mathematics benchmarks. The complementarity with Sledgehammer (Table 11) is interesting but only shown for Isabelle, not Lean.

The phrase "without any further finetuning" is strictly true but potentially misleading: the 3-shot prompt is a form of adaptation, and the 11-shot prompt for Isabelle autoformalization includes carefully selected examples (7 for number theory, 6 for others). These are few-shot, not zero-shot — the model sees task-specific examples at evaluation time. A true zero-shot evaluation (no examples, just the problem statement and a format specification) would test whether the capability emerges purely from pretraining without any in-context guidance. The paper doesn't report zero-shot results for formal mathematics.

Claim 3: "Continued pretraining on Proof-Pile-2 is effective for improving a pretrained model's ability to perform mathematical problem solving" (Section 3.1 Results).

Strongly supported by the consistent improvements over Code Llama across all five chain-of-thought benchmarks (Table 1). The average improvement across benchmarks is substantial: roughly 15 percentage points for the 7B model and 12 points for the 34B model. The gains are robust across different task formats (free-response MATH, multiple-choice MMLU, word problems GSM8k) and difficulty levels (elementary through undergraduate). The fact that the SAT (which postdates the knowledge cutoff) shows the largest improvement (+43.7 points for 7B) provides out-of-distribution validation that the improvement reflects genuine reasoning capability, not memorization of contemporaneous web data.

The weakness: all evaluations use the same model checkpoint, and the paper doesn't study when during the continued pretraining the improvements emerge. Does MATH accuracy improve linearly with continued pretraining tokens, or does it saturate? Is there a "critical period" where most of the gain occurs? These learning curve analyses would provide practical guidance for practitioners deciding how many tokens of continued pretraining to budget. The paper also doesn't evaluate whether the improvements are stable or whether catastrophic forgetting of non-mathematical capabilities occurs (beyond the minimal regularization from 5% general-domain data). A broader evaluation on standard NLP benchmarks (HellaSwag, PIQA, WinoGrande, etc.) would reveal whether LLEMMA sacrifices general capability for mathematical specialization.

Claim 4: "The Proof-Pile-2 corpus and AlgebraicStack enable the training of state-of-the-art open mathematical language models" (Section 1, contribution 2).

Supported by the existence of the open models, but the causal claim — that Proof-Pile-2 specifically enables SOTA performance, rather than any comparably large math corpus — is not tested. The paper does not ablate Proof-Pile-2 against an alternative math corpus (e.g., Minerva's dataset, if it were available, or a simpler filtered CommonCrawl math subset). The paper also trains only one model architecture (Code Llama / Llama 2) at two scales, so we don't know whether Proof-Pile-2 would be equally effective for other base models (Mistral, Falcon, Gemma, etc.). The release of the dataset enables such comparisons by other researchers, but the paper itself provides only an existence proof, not a controlled comparison of data recipes.

Missing experiments that would strengthen the paper:

Zero-shot evaluations: The paper reports few-shot results exclusively. Zero-shot evaluation (no prompt examples, just a task description) would reveal how much of the mathematical capability is "in the weights" versus activated by in-context examples. This is particularly important for the formal mathematics results, where the 3-shot and 11-shot prompts provide substantial task-specific guidance.
Learning curves during continued pretraining: Intermediate checkpoints evaluated on MATH and GSM8k would show when during the 200B-token training the improvements occur, whether they saturate, and whether additional training would have helped. The premature termination of the 7B training run at step 42,000 (out of 48,000 planned) makes this especially relevant — the checkpoint at step 42,000 might be suboptimal.
General capability benchmarks: Evaluation on standard NLP tasks (reading comprehension, commonsense reasoning, world knowledge) would quantify the degree of catastrophic forgetting from continued pretraining on domain-specific data. The paper uses 5% general-domain data as a regularizer following Minerva, but never measures whether this is sufficient to preserve general capabilities.
Fine-tuning scaling: The supervised fine-tuning experiment (Table 12) uses only one dataset (MetaMathQA) and only the 7B model. Evaluating fine-tuned LLEMMA 34B on MetaMathQA would reveal whether the continued pretraining advantage compounds with scale after fine-tuning.
Search budget scaling for formal mathematics: The Lean 4 evaluation uses a fixed search budget (1×32). Sweeping the number of generated tactics per iteration (S) would show whether LLEMMA benefits from additional search at inference time, or whether its few-shot tactic prediction saturates at low budgets while a fine-tuned model like ReProver would continue to improve.
Contamination analysis on all benchmarks: The memorization analysis only covers MATH. Similar analyses for GSM8k, OCWCourses, and MMLU-STEM would provide a more complete picture of whether performance gains reflect reasoning or data overlap. The paper mentions that GSM8k has only 2 problem hits (Table 6), which is reassuring, but doesn't perform the manual inspection or hit-vs-non-hit accuracy analysis for GSM8k.
Ablation of AlgebraicStack subcomponents: Removing Lean/Isabelle/Coq data from AlgebraicStack and measuring the impact on formal theorem proving would directly test whether the formal proof data in pretraining is necessary for the emergent formal mathematics capability, or whether general mathematical training plus code exposure suffices.

Conditions under which the claims hold:

The claims about LLEMMA's performance relative to Minerva hold for the 7B model at equi-parameter scale (7B vs. 8B) and for the 34B model at lower parameter count (34B vs. 62B). They may not hold if an open model is compared to a Minerva of exactly the same parameter count — we simply don't know. The claims about continued pretraining efficacy hold for Code Llama initializations trained on Proof-Pile-2; generalization to other base architectures or math corpora is untested. The claims about tool use and formal theorem proving hold for few-shot prompting with carefully constructed prompts; zero-shot performance may be substantially lower. The claims about memorization not driving performance gains hold for MATH under 30-gram overlap analysis but may not generalize to benchmarks not analyzed (GSM8k, OCWCourses) or to more sophisticated forms of contamination (paraphrased solutions, semantically equivalent problem variants).

Strongest experimental evidence in the paper:

The majority voting results on MATH (Table 2) — LLEMMA 34B at 43.1% vs. Minerva 62B at 43.4% — represent the cleanest demonstration that continued pretraining on Proof-Pile-2 produces a model competitive with the proprietary state-of-the-art at a meaningfully smaller parameter count. The gap of 0.3 percentage points with 1.8× fewer parameters is the paper's most compelling single data point.

The SAT results (Table 1) — LLEMMA 34B at 71.9% vs. Code Llama 34B at 40.6%, a 31.3-point improvement — provide the strongest evidence that the improvement is not due to memorization, since the SAT postdates the training data cutoff. This is a clean test of reasoning transfer: the model cannot have seen the problems, yet its accuracy more than doubles after continued pretraining.

Weakest experimental evidence in the paper:

The data mixture ablation (Table 5) is conducted only at small scale (reduced training steps on Code Llama 7B) and uses perplexity on the MATH training set as the selection criterion, which may not correlate perfectly with downstream task accuracy. The resulting 2:4:1 ratio is then applied to the full-scale training runs without validation that the small-scale perplexity ranking holds at full training duration. The narrow spread of perplexities (1.478 vs. 1.489 for the best and worst mixtures) suggests the mixture choice may not be particularly consequential, yet the paper presents this as a systematic methodology.

The OCWCourses results (Table 1) show small absolute improvements (7.7% for LLEMMA 7B, 11.8% for LLEMMA 34B) that are only a few points above the Code Llama baselines (4.4% and 7.0%). The test set size for OCWCourses is not reported, making it difficult to assess whether these differences are statistically meaningful or within sampling noise. The paper includes OCWCourses because Minerva evaluated on it, but the results are too close to zero for most comparisons to be informative.

6. Limitations and Trade-offs

Test-Time Compute Cannot Compensate for Fundamental Capability Gaps

The assumption or constraint. The paper's FLOPs-matched analysis in Section 7 implicitly assumes that problems are within the base model's capability range — that the model already produces correct solutions at some non-trivial rate. The authors are explicit about this boundary condition, noting in the Section 7 takeaway that "on the hardest problems... test-time compute provides essentially zero benefit regardless of budget."

The consequence. For problems where the base model's pass@1 is near zero, no amount of search, revision, or compute-optimal allocation helps. This is visible in Figure 3 (right), where bin 5 (hardest) problems show 1–3% accuracy for both beam search and best-of-N across all budgets; in Figure 7 (right), where bin 5 hovers at 2–3% regardless of sequential-to-parallel ratio; and in Figure 9, where the bin 5 scaling line is essentially flat. The FLOPs-matched comparison in Figure 1 reveals the practical implication: on hard problems at high inference-to-pretraining ratios, test-time compute with the smaller model shows a −52.9% relative disadvantage compared to simply training a ~14× larger model. This means that for genuinely novel or out-of-distribution reasoning tasks — those where the base model cannot produce correct solutions even with many attempts — pretraining remains the only viable path. Test-time compute amplifies existing capability but cannot create it where absent.

What evidence exists in the paper. The per-difficulty-bin breakdowns across all experiments (Figures 3 right, 7 right, and 9) consistently show near-zero accuracy and zero slope for the hardest quintile. The FLOPs-matched bar charts in Figure 1 quantify the failure explicitly. The authors state in Section 8 they are "candid about this limitation."

Mitigation status. The paper does not attempt to solve this limitation. It identifies it clearly and uses it to delineate the scope of applicability — test-time compute is positioned as complementary to pretraining scaling rather than a replacement for it. The authors suggest in Section 7 that "for such problems, pretraining remains the only viable path," effectively drawing a boundary condition for practitioners. There is no proposal for hybrid approaches that might extend the capability frontier.

The Cost of Difficulty Estimation Is Not Accounted for in Efficiency Gains

The assumption or constraint. The entire compute-optimal framework depends on estimating each prompt's difficulty before allocating the inference budget. The paper's method for doing so — generating 2048 samples per question and averaging either ground-truth correctness or PRM final-answer scores — is extraordinarily expensive. The authors acknowledge this in Section 3.2:

"estimating difficulty in this way still incurs additional computation cost during inference... our experiments do not account for this cost largely for simplicity"

The consequence. The paper's headline finding — "4× better efficiency over best-of-N" — is computed after difficulty is known, without amortizing the cost of learning it. The 2048 samples used for difficulty estimation exceeds the largest test-time budgets studied in the paper (256–512 generations) by 4–8×. In a realistic deployment, the total cost would be difficulty estimation + strategy execution, and the estimation cost would dominate for most queries. This means the 4× figure is an upper bound on achievable efficiency rather than a realized deployment gain. Unless difficulty can be predicted cheaply (e.g., from the question text alone, or from a small number of initial samples), the compute-optimal approach may actually be more expensive than a simple best-of-N baseline when total cost is accounted for. The reported efficiency improvements should be understood as what is achievable if difficulty were known in advance, not as a deployable system.

What evidence exists in the paper. The paper reports that predicted difficulty bins (using PRM scores) track oracle bins closely in Figures 4 and 8, demonstrating that ground-truth labels are not required. However, the 2048-sample estimation cost is not included in any budget calculation, and the paper does not experiment with cheaper estimation methods (e.g., fewer samples, learned difficulty predictors). The authors explicitly call this out in Section 3.2 and Section 8 as a key direction for future work: "pretraining or finetuning models to directly predict difficulty of a question."

Mitigation status. The paper acknowledges the limitation transparently and flags it as future work, but provides no experimental mitigation. A natural approach — adaptive difficulty estimation using the first few generated samples to estimate difficulty, then allocating the remaining budget accordingly — is suggested but not tested. The compute-optimal curves in Figures 4 and 8 should be interpreted with an implicit asterisk: they represent the potential of difficulty-conditioned allocation, assuming difficulty can be estimated cheaply enough, not the realized efficiency of the complete system.

The Revision Model's Correct-to-Incorrect Reversion Problem Is Unresolved

The assumption or constraint. The revision model was trained exclusively on trajectories where all in-context answers are incorrect followed by a correct target (Section 6.1). This data construction has a direct consequence: the model is never trained to recognize when the current answer is already correct and should be preserved. As noted in Section 6.1, approximately 38% of correct answers generated during a revision chain get converted back to incorrect answers in the subsequent step.

The consequence. Sequential revision chains can be self-defeating: the model may produce a correct answer at step 3, then "revise" it to an incorrect answer at step 4, then produce another correct answer at step 7, and so on. This introduces a fundamental instability — longer revision chains do not monotonically approach the truth. The paper mitigates this with within-chain selection (majority voting or verifier-based selection across all revision steps, picking the best answer from any point in the chain), but this is an imperfect patch. The chain-level selection mechanism sees all revision steps and tries to identify which one is correct, but if the verifier is imperfect (which it is, particularly for revision model outputs — Figure 15a shows the base-LM PRM underperforms on revision outputs), the selection itself can fail. The correct-to-incorrect reversion pattern means that simply generating more revisions provides no guarantee of improvement, and in pathological cases could make things worse.

What evidence exists in the paper. The 38% reversion rate is reported in Section 6.1. Figure 6 (left) shows that pass@1 at each revision step increases gradually (from ~18% to ~25% over 64 steps) but also exhibits variance around a non-increasing trend, consistent with reversion events. The paper notes the phenomenon explicitly and describes the within-chain selection mitigation. However, no experiment directly measures how often the chain's best answer (post-selection) is better than the initial generation, or how reversion affects the effective improvement from longer chains.

Mitigation status. The paper implements within-chain selection (Section 6.1) and finds that it enables sequential revisions to outperform parallel sampling in aggregate (Figure 6 right). However, this treats the symptom rather than the cause — the model still wastes compute generating revisions that make correct answers wrong. A more principled solution (training the model to recognize and preserve correct answers, or adding a self-evaluation step before each revision) is not explored. The ReST $^{EM}$ experiment in Appendix K (Figure 16) actually shows that attempting to further optimize the revision model worsens performance, suggesting the revision training recipe is fragile and the reversion problem may be resistant to straightforward fixes.

Results Are Limited to a Single Benchmark Family and Model Architecture

The assumption or constraint. All experiments in the paper use the MATH benchmark (Hendrycks et al., 2021) as the primary evaluation, with PaLM 2-S* as the base model. The authors state in Section 4 that they "believe this model is representative of the capabilities of many contemporary LLMs," but this claim is unverified. The analysis in Section 2 reflects some specificity with formal math languages like Isabelle and Lean, but the prior analysis's MATH-centric focus carries over.

The consequence. It is unclear whether the paper's central findings — difficulty-dependent optimal strategies, the 4× efficiency gain over best-of-N, the over-optimization patterns — generalize to other reasoning domains, other model architectures, or other evaluation formats. Key results could be specific to MATH: (1) MATH problems have clean ground-truth answers enabling exact-match verification, which is essential for PRM training via Monte Carlo rollouts; domains without crisp correctness signals (dialogue, creative writing, code generation without test suites) cannot use this approach. (2) MATH's difficulty distribution (competition math problems) may not represent the difficulty distribution of real-world queries, which could be bimodal (many easy, many hard, few medium) rather than roughly uniform across quintiles. (3) PaLM 2-S*'s particular calibration properties, error patterns, and revision behavior may not transfer to other model families (Llama, Mistral, GPT). The compute-optimal policies — which search method to use, what sequential-to-parallel ratio — are learned specifically for this model on this benchmark and could differ substantially for other models and tasks.

What evidence exists in the paper. The paper only evaluates on MATH, with no cross-domain experiments. The model comparison is limited to PaLM 2-S* and a single ~14× larger variant. The authors acknowledge that "single benchmark, single model family" is an important limitation to address in future work but do not include any out-of-domain evaluation. The PRM training uses MATH training data, the difficulty bins are defined relative to MATH pass@1, and the compute-optimal policies are cross-validated on the MATH test set. Everything is MATH- and PaLM 2-S*-specific.

Mitigation status. The paper does not mitigate this limitation experimentally. The authors explicitly call for future work on "other domains and modalities" in Section 8, mentioning code generation, logical reasoning, and scientific QA as candidate domains. The framework itself — difficulty-conditioned allocation of test-time compute — is domain-agnostic in principle, but all parameter values (optimal strategies, bin boundaries, scaling curves) are domain- and model-specific and would need to be re-derived for each new setting. A practitioner cannot take the paper's 2:1–8:1 sequential-to-parallel ratio or "beam search on medium problems, best-of-N on easy" recommendation and apply it to a different model on a different task without re-running the full analysis.

The ~14× Larger Model Baseline Is Not Compute-Optimally Trained, Weakening the Training-Inference Tradeoff Claim

The assumption or constraint. The FLOPs-matched comparison in Section 7 scales model parameters while holding training data fixed, following the LLaMA paradigm (Touvron et al., 2023) where models are overtrained relative to Chinchilla-optimal scaling. The authors acknowledge this choice:

"We choose this setting as it is representative of a canonical approach to scaling pretraining compute and leave the analysis of compute-optimal scaling of pretraining compute where the data and parameters are both scaled equally to future work." (Section 7)

The consequence. The Chinchilla scaling laws (Hoffmann et al., 2022) show that for a fixed compute budget, parameters and data should be scaled roughly equally. A LLaMA-style model scaled only in parameters uses its compute budget suboptimally — it would achieve lower loss than a Chinchilla-optimal model of the same parameter count, but higher loss than a Chinchilla-optimal model with the same total FLOPs (which would have fewer parameters but more training data). This means the ~14× larger model used as the pretraining-scaled baseline in Section 7 is likely weaker than a compute-optimally trained model would be. The reported advantages of test-time compute over pretraining — such as +27.8% on easy questions at low inference-to-pretraining ratios (Figure 1, top-right) — may therefore overstate the benefit of test-time compute relative to what a properly compute-optimal larger model could achieve. If the baseline were Chinchilla-optimal rather than LLaMA-style, the break-even points where pretraining becomes preferable would likely shift to lower difficulty levels or lower inference-to-pretraining ratios.

Additionally, the larger model uses only greedy decoding with no test-time compute augmentation of its own. Giving the larger model even a modest test-time budget (best-of-8, or majority voting) would create a much stronger baseline. The current comparison is effectively "test-time compute with small model vs. no test-time compute with large model," which stacks the deck in favor of test-time compute.

What evidence exists in the paper. The paper reports the comparison in Figure 9 and the bar charts in Figure 1, showing test-time compute outperforming the larger model on easy and medium problems at low-to-moderate inference-to-pretraining ratios, but underperforming on hard problems and at high ratios. The paper explicitly notes the Chinchilla caveat in Section 7. The degree of overstatement is not quantified — we do not know how much the larger model's accuracy would improve if it were Chinchilla-optimally trained (which would give it fewer parameters but more data, or different training dynamics). The paper also does not test the larger model with any test-time compute augmentation (e.g., best-of-4, majority voting with the larger model).

Mitigation status. The limitation is acknowledged but not experimentally addressed. The authors position the LLaMA-style comparison as "representative of a canonical approach" and defer Chinchilla-optimal comparisons to future work. Until that comparison is done, the FLOPs-matched results should be interpreted as evidence that test-time compute can substitute for parameter-only scaling of pretraining, not that it can substitute for compute-optimal pretraining. The difference between these two claims is significant: many production models (Chinchilla, the early GPT series) used compute-optimal training, while others (LLaMA, Llama 2) intentionally overtrained on data. The paper's results are most relevant to practitioners using the latter paradigm.

Sequential Revisions Incur a Latency Cost Not Captured by Generation-Budget Accounting

The assumption or constraint. The paper measures test-time compute exclusively in "generations" — the number of complete solutions sampled — and uses this as a proxy for total computational cost. However, sequential revision chains are inherently serial: each revision depends on the output of the previous one, so a chain of length L requires L sequential forward passes through the model. Parallel best-of-N, by contrast, can batch all N generations into a single forward pass (subject to memory constraints).

The consequence. A compute-optimal policy that allocates 128 generations as 64 sequential × 2 parallel takes approximately 64× longer wall-clock time than a policy that allocates 128 parallel generations, even though both have the same "generation budget." For latency-sensitive applications — interactive assistants, real-time tutoring, any user-facing system — the sequential-heavy strategies that the compute-optimal policy favors on easy problems (Figure 7 right, bin 1: purely sequential is optimal) may be impractical regardless of their accuracy advantages. A user waiting for 64 sequential forward passes (each requiring the previous to finish) could experience multi-second to multi-minute latencies, whereas 128 parallel samples could return the answer in the time of a single forward pass plus scoring. In high-throughput batch processing, the latency penalty translates to reduced throughput — a server, a pipeline, or a user can handle fewer queries per unit time even if each query uses the same total FLOPs.

What evidence exists in the paper. The paper does not measure latency or wall-clock time. The generation budget is the universal cost metric, and all efficiency comparisons (the 4× claims in Figures 4 and 8) are made in terms of generation count. Section 2 acknowledges that best-of-N is "parallelizable" while sequential sampling is not, but no experiment quantifies the latency trade-off. The revision chain lengths tested go up to 64 steps (Figure 6 left), and the optimal sequential-to-parallel ratios in Figure 7 include purely sequential configurations — both of which would impose substantial latency in deployment.

Mitigation status. The paper does not address this limitation at all. No latency measurements are reported, and no discussion of the throughput-latency trade-off appears in the main text. The compute-optimal policy is optimized purely for accuracy at a given generation budget, ignoring the time dimension entirely. In practice, a deployment would need to incorporate a latency constraint — for example, capping the maximum sequential chain length, or dynamically adjusting the sequential-to-parallel ratio based on a per-query deadline. The paper's framework could be extended to include such constraints (the optimization in Equation 1 would gain a wall-clock term), but this is not explored.

7. Implications and Future Directions

How This Work Changes the Landscape

LLEMMA changes the landscape for mathematical language models by demonstrating that open-weight models can match or approach proprietary state-of-the-art performance through continued pretraining on carefully curated public data, without requiring task-specific fine-tuning, novel architectures, or training algorithms. This is a reframing rather than a paradigm shift: the continued pretraining recipe itself was established by Minerva (Lewkowycz et al., 2022), but LLEMMA converts it from a proprietary capability into a reproducible, accessible, and documented methodology that any research group with sufficient compute can replicate.

The magnitude of this change is best understood through its downstream effects on research infrastructure. Before LLEMMA, a researcher wanting to build on a strong mathematical language model had two bad options: use a closed API (Minerva, GPT-4) with no access to weights, training data, or internal representations, or use an open model (earlier Llama or Code Llama variants) that performed poorly on mathematical reasoning. LLEMMA eliminates this dilemma by providing open models at 7B and 34B scales that achieve competitive performance — 43.1% on MATH with majority voting for the 34B model, within 0.3 points of Minerva 62B (Table 2) — while releasing the full training corpus, model weights, and training code. Researchers can now probe internal representations to understand how mathematical reasoning is encoded, run controlled ablations on data composition, fine-tune for novel formal mathematics tasks, and build verifiers or reward models on top of a competent mathematical base — all activities that were impossible or restricted under the closed-access regime.

The work also reconciles a tension between two approaches to mathematical AI that previously appeared in tension. One line of work pursued supervised fine-tuning on task-specific datasets (MetaMath, WizardMath, MAmmoTH), achieving strong benchmark scores but producing models narrowly specialized to particular evaluation formats. Another line pursued continued pretraining (Minerva), producing general mathematical base models but keeping them proprietary. LLEMMA demonstrates that continued pretraining on public data can produce models that are simultaneously (a) open, (b) competitive on benchmarks, and (c) general enough to transfer to tool use and formal theorem proving without task-specific adaptation (Sections 3.2, 3.3). This resolves the implicit trade-off between openness, generality, and performance: with sufficient data curation effort, all three can be achieved simultaneously.

A subtle but important shift in research priorities follows from LLEMMA's results. The paper's strongest finding — that a 34B model trained on 55B tokens of curated math data can match a 62B proprietary model — implies that data curation quality and diversity, not model scale or training algorithm sophistication, is the primary bottleneck for open mathematical language models. This redirects research attention from architectural innovation (tree search, symbolic modules) and training objective design (RL from verifier feedback, process supervision) toward the more mundane but impactful task of building better mathematical pretraining corpora. If 55B tokens of data yields Minerva-competitive performance, what would 200B tokens of even more carefully curated data achieve? What mathematical formalisms and reasoning patterns are underrepresented in current corpora? These data-centric questions become higher-priority than they were before LLEMMA's release.

The work also makes formal mathematics more accessible as a research direction. Prior to LLEMMA, neural theorem proving typically required training small, task-specialized models from scratch — a process requiring domain expertise in both machine learning and the specific proof assistant. LLEMMA demonstrates that a general mathematical base model, prompted with just 3 examples, can generate Lean 4 tactics at a level competitive with fine-tuned retrieval-augmented models (26.23% for LLEMMA-7B vs. 26.50% for ReProver, Table 4). This lowers the barrier to entry dramatically: researchers can now work on formal theorem proving by prompt-engineering a publicly available base model rather than needing to assemble training pipelines, curate proof data, and manage proof assistant interactions during training. The release of AlgebraicStack (11B tokens including 1.5B+ tokens of formal proof data) further enables this by providing a pretraining corpus that other groups can use to train their own formal-math-capable models.

Finally, the paper establishes a template for domain-specific open language models that extends beyond mathematics. The recipe — identify a domain, curate a multi-source pretraining corpus spanning natural language, code, and formal representations, continue pretraining from a strong code-capable base model, and release all artifacts — is explicitly documented and could be applied to other structured reasoning domains: physics (arXiv + computational physics code + formalized physics in proof assistants), biology (PubMed + bioinformatics code + formalized biological models), or finance (SEC filings + quantitative finance code + formalized financial contracts). The paper provides not just a model but a methodology, complete with a systematic approach to mixture weight selection (Section 3.4) and a memorization analysis framework (Section 3.5) that future domain adaptation efforts can adopt.

Follow-Up Research This Work Enables

Data mixture optimization with leave-one-out ablations. The paper selects mixture weights by comparing six candidate arXiv:Web:Code ratios using MATH training set perplexity (Table 5). A natural follow-up would systematically ablate each Proof-Pile-2 component: train models with (a) no AlgebraicStack, (b) no OpenWebMath, (c) no ArXiv, (d) no formal proof data within AlgebraicStack, and (e) no general-domain regularization data. Evaluating these ablated models on the full suite of tasks — chain-of-thought reasoning, tool use, and formal theorem proving — would directly measure the marginal contribution of each data source to each capability. The hypothesis worth testing is that formal proof data in AlgebraicStack is necessary for the emergent formal theorem proving capability (without it, LLEMMA might still do MATH well but fail on Lean tactic prediction), while OpenWebMath is necessary for chain-of-thought benchmarks (since it contains worked problem solutions), and ArXiv provides the underlying mathematical knowledge that both capabilities draw upon. A leave-one-out design would produce a causal decomposition of Proof-Pile-2's effectiveness that the current paper only hints at.

Scaling the data volume: how much math pretraining is enough? LLEMMA 7B was trained on 200B tokens and LLEMMA 34B on 50B tokens, but the paper provides no learning curves showing when performance saturates. A follow-up study could train a sequence of models on logarithmically spaced data volumes (e.g., 10B, 25B, 50B, 100B, 200B, 400B tokens of Proof-Pile-2-style data) and evaluate on MATH, GSM8k, and formal theorem proving at each checkpoint. This would produce mathematical reasoning scaling laws analogous to the general language modeling scaling laws of Kaplan et al. (2020) and Hoffmann et al. (2022). Key questions: Does MATH accuracy follow a power law in training tokens, or does it exhibit emergent jumps at particular data thresholds? Do different capabilities (chain-of-thought, tool use, formal proving) scale at different rates? Does continued pretraining eventually degrade general language capabilities even with the 5% regularizer, and if so, when? Answering these questions would provide practical guidance for practitioners deciding how many tokens of domain-specific data to curate and how long to train.

Cross-architecture replication: testing Proof-Pile-2 on non-Llama base models. LLEMMA uses Code Llama (which inherits from Llama 2) as its initialization. A critical test of Proof-Pile-2's generality would be to apply the same continued pretraining recipe to different base architectures — Mistral, Gemma, Qwen, or DeepSeek — and measure whether the improvements are consistent. The specific question is whether Proof-Pile-2's effectiveness depends on Llama-specific features (rotary position embeddings, SwiGLU activations, the particular tokenizer) or whether it transfers to architectures with different inductive biases. If the improvements are consistent across architectures, Proof-Pile-2 becomes a general-purpose resource for mathematical domain adaptation. If they are not, it reveals that data recipes are architecture-dependent, which would be a practically important negative result that current literature does not address.

Zero-shot and chain-of-thought ablation for formal theorem proving. The paper evaluates formal theorem proving with few-shot prompts (3 examples for Lean, 11 for Isabelle). A follow-up would systematically vary the number of few-shot examples from 0 to 20 and measure proof success rate, to determine how much of the capability comes from pretraining versus in-context learning. A zero-shot evaluation — providing only the proof state with no examples — is the cleanest test of whether formal proof capability is truly "in the weights." If LLEMMA achieves non-trivial zero-shot proof success, it would be strong evidence that continued pretraining on AlgebraicStack teaches the model an internal representation of formal proof structure that generalizes without task-specific guidance. A complementary experiment would compare the 3-shot prompt used in the paper against a prompt that provides examples of a different proof assistant (e.g., test on Lean but prompt with Isabelle examples). If performance degrades substantially, it indicates the model learned assistant-specific syntax rather than transferable proof strategies.

Combining LLEMMA with search-based and verifier-guided methods from the test-time compute literature. The paper evaluating compute-optimal test-time scaling (the companion paper analyzed in prior sections) demonstrated that beam search against a process reward model, sequential revisions, and difficulty-conditioned strategy allocation can yield 4× efficiency gains for mathematical reasoning. LLEMMA provides an open base model that could serve as the foundation for such methods. A concrete experiment: train a process reward model on LLEMMA's outputs using Monte Carlo rollouts (following Wang et al., 2023 and the companion paper's Section 5.1), then evaluate whether best-of-N weighted selection or beam search against this PRM improves LLEMMA's MATH majority voting performance beyond the 43.1% reported in Table 2. A second experiment: fine-tune LLEMMA as a revision model using the edit-distance-based incorrect-correct pairing from the companion paper's Section 6.1, and measure whether sequential revision chains improve pass@1. These experiments would bridge the domain-specific pretraining literature (this paper) with the test-time compute scaling literature, testing whether open mathematical base models can realize the inference-time gains previously demonstrated only on proprietary models (PaLM 2-S*).

Memorization analysis across all benchmarks and with semantic matching. The paper's 30-gram overlap analysis (Section 3.5) only covers MATH, finding limited evidence that memorization drives performance. Extending this analysis to GSM8k, OCWCourses, MMLU-STEM, and formal theorem proving benchmarks would provide a complete picture of data contamination. More ambitiously, replacing n-gram overlap with semantic similarity matching — embedding test problems and training documents in a shared vector space and flagging high-cosine-similarity pairs for manual inspection — would catch paraphrased solutions and semantically equivalent problem variants that n-gram methods miss. This is important because the manual inspection of MATH hits (Table 6, right) found that 49% of problem-statement hits had different solutions with the same answer — the model might learn solution patterns from these documents even when n-gram matching fails to flag them. A negative result here (finding that semantically similar training documents do predict higher model accuracy) would substantially qualify the paper's claim that continued pretraining teaches general reasoning rather than memorization.

Practical Applications and Downstream Use Cases

Open-source reward modeling and RL for mathematical reasoning. Lightman et al. (2023) and Uesato et al. (2022) established that process-supervised reward models can substantially improve mathematical reasoning when used to guide search or provide RL training signals. However, these lines of work have been restricted to proprietary models (GPT-4, PaLM) due to the lack of capable open mathematical base models. LLEMMA 34B, with its 43.1% MATH maj@256 performance, provides a competent base model on which researchers can train open process reward models. A practical pipeline: generate solution traces from LLEMMA, annotate step-level correctness using the Monte Carlo rollout procedure from Wang et al. (2023) (which requires only a base model, not human labels), train a PRM, and use it to guide best-of-N weighted selection or beam search at inference time. This would produce an entirely open pipeline — base model, training data, reward model, and inference procedure — for mathematical reasoning with verifier-guided search, enabling the research community to study reward hacking, over-optimization, and compute-optimal allocation in a reproducible setting. The 7B model makes this feasible for academic compute budgets (the PRM can be trained on a few GPUs rather than requiring datacenter-scale resources).

Formalization of informal mathematics using few-shot prompting. The informal-to-formal proving results (Table 4, left) demonstrate that LLEMMA can autoformalize informal proofs into Isabelle with 22.13% test accuracy using an 11-shot prompt. While 22% is far from production-ready, the union of LLEMMA and Sledgehammer proves 27.46% of test theorems — a 7-point improvement over Sledgehammer alone (Table 11). A practical near-term application: use LLEMMA as a triage tool in interactive proof assistants, where it generates candidate formal proofs from informal descriptions, and the proof assistant's automation (Sledgehammer, hammer) attempts to fill in the gaps. The 22% of theorems LLEMMA proves directly save human effort, and the complementarity with automation means the combined system covers theorems that neither handles alone. For proof assistant users (mathematicians formalizing results in Lean or Isabelle), integrating LLEMMA as a proof suggestion engine could meaningfully accelerate formalization workflows. The key advantage over existing tools (GPT-4-based COPRA, which achieved 23.36%, Table 4) is that LLEMMA is open and can be run locally, avoiding API costs, latency, and data privacy concerns.

Domain-specific continued pretraining as a cost-effective deployment strategy. The paper shows that LLEMMA 7B outperforms Code Llama 34B on MATH (18.0% vs. 12.2%, Table 1) and LLEMMA 34B matches Minerva 62B on MATH with majority voting (43.1% vs. 43.4%, Table 2). These comparisons imply that continued pretraining on domain-specific data can compensate for a factor of ~2–5× in model scale for mathematical reasoning tasks. For organizations deploying mathematical AI systems — educational technology platforms, automated grading systems, mathematical search engines — this translates to a concrete cost trade-off: spending ~23,000 A100-hours on continued pretraining of a 7B model (the cost of LLEMMA 7B training) versus spending 5–25× more on inference costs for a 34B or larger model over the deployment lifetime. If the model will serve millions of queries, the inference cost of the larger model will eventually dominate the upfront training cost, making the domain-adapted smaller model more economical. The paper's release of the exact training recipe (data mixture weights, learning rate schedule, RoPE configuration) makes this trade-off calculable for practitioners, who can adapt the recipe to their specific mathematical domain (e.g., K-12 math education, university calculus, competition math) by swapping Proof-Pile-2 components for domain-specific corpora.

Pretraining corpus for mathematical language model research. Beyond the models themselves, Proof-Pile-2 (55B tokens) and AlgebraicStack (11B tokens) serve as reference corpora for studying how mathematical knowledge is represented in language models. Researchers investigating mechanistic interpretability of reasoning can train models from scratch or continue pretraining on Proof-Pile-2 with controlled interventions — for example, training on Proof-Pile-2 with formal proof data removed to study its causal role in emergent formal proving, or training on Proof-Pile-2 with perturbed mathematical notation to study how LaTeX formatting affects reasoning. The fact that the dataset is fully documented (Appendix B, Appendix E) with explicit filtering procedures, decontamination against benchmark test sets, and a datasheet following Gebru et al. (2021) means researchers can understand exactly what the model was trained on and design controlled experiments that isolate specific data effects. This transforms mathematical language model research from a black-box enterprise (where training data is unknown and models are accessed via API) into an open science where data, models, and evaluations are all transparent.