Llemma: An Open Language Model For Mathematics

Introduction

Language models trained on diverse mixtures of text display remarkably general language understanding and generation capabilities (Brown et al., 2020; Chowdhery et al., 2022), serving as base models that are adapted to a wide range of applications (Raffel et al., 2023). Applications such as open-ended dialogue (Thoppilan et al., 2022; Touvron et al., 2023) or instruction following (Ouyang et al., 2022; Wei et al., 2022) require balanced performance across the entire distribution of natural text, thus favoring generalist models. However, if we seek to maximize performance within one domain, such as medicine (Singhal et al., 2022; 2023), finance (Wu et al., 2023), or science (Taylor et al., 2022), a domain-specific language model may offer superior capabilities for a given computational cost, or lower computational cost for a given level of capability.

In this work, we train a domain-specific language model for mathematics. We have several motivations for doing so. First, solving mathematical problems requires pattern matching against a large body of specialized prior knowledge, thus serving as an ideal setting for domain adaptation. Second, mathematical reasoning is in itself a central AI task, its study dating back to at least Gelernter (1959) and Wang (1960) and continuing to today (Lu et al., 2023). Third, language models capable of strong mathematical reasoning are upstream of a number of research topics, such as 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).

Although domain-specific models for mathematics have been trained in the past, they have either been closed access (Lewkowycz et al., 2022), limiting their ability to become a platform for further research, or have lagged far behind the closed access state-of-the-art (Azerbayev et al., 2023).

We present a recipe for adapting a language model to mathematics through continued pretraining (Lewkowycz et al., 2022; Rozière et al., 2023) on $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$, a diverse mixture of math-related text and code. Applying the recipe to Code Llama (Rozière et al., 2023) yields Llemma: 7 billion and 34 billion parameter base language models with substantially improved mathematical capabilities.

Specifically, our contributions are as follows:

We train and release the Llemma models: 7B and 34B parameter language models specialized for mathematics. The Llemma models are a new state-of-the-art for publicly released base models on MATH (Lewkowycz et al., 2022).

We release the $\mathsf{AlgebraicStack}$, a dataset of 11B tokens of code specifically related to mathematics.

We demonstrate that Llemma is capable of using computational tools to solve mathematical problems, namely, the Python interpreter and formal theorem provers.

Unlike prior mathematics language models such as Minerva (Lewkowycz et al., 2022), the Llemma models are open access and we open source our training data and code. This allows Llemma to serve as a platform for future research in mathematical reasoning.

Our work builds on findings in Minerva (Lewkowycz et al., 2022), but differs in several ways: (1) Llemma’s training and evaluation covers a wider range of data and tasks, notably code data (e.g., the $\mathsf{AlgebraicStack}$), tool use, and formal mathematics; (2) our work only depends on publicly accessible tools and data; (3) we provide new analyses related to the continued training data mixture, memorization, and additional supervised finetuning; (4) we make all artifacts publicly available.

Approach

Llemma models are 7 billion and 34 billion parameter language models specialized for mathematics. Our approach is to continue pretraining Code Llama (Rozière et al., 2023) on the $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$.

We form the $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$, a 55B-token mixture of scientific papers, web data containing mathematics, and mathematical code. With the exception of the Lean proofsteps subset (see Appendix B), the $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ has a knowledge cutoff of April 2023.

Computational tools such as numerical simulations, computer algebra systems, and formal theorem provers are of ever increasing importance to mathematicians (Avigad, 2018). Motivated by this fact, we create $\mathsf{AlgebraicStack}$, an 11B-token dataset of source code from 17 languages, spanning numerical, symbolic, and formal math. The dataset consists of filtered code from the Stack (Kocetkov et al., 2022), public GitHub repositories, and formal proofstep data. Table 9 shows the number of tokens by language in $\mathsf{AlgebraicStack}$. See Appendix B.1 for further details on $\mathsf{AlgebraicStack}$.

We use OpenWebMath (Paster et al., 2023), a 15B-token dataset of high-quality web pages filtered for mathematical content. OpenWebMath filters CommonCrawl web pages based on math-related keywords and a classifier-based math score, preserves mathematical formatting (e.g., LaTeX, AsciiMath), and includes additional quality filters (e.g., perplexity, domain, length) and near-deduplication. Refer to Paster et al. (2023) for a full description of OpenWebMath.

We use the ArXiv subset of RedPajama (Computer, 2023), an open-access reproduction of the LLaMA training dataset. The ArXiv subset contains 29B tokens.

Following Lewkowycz et al. (2022), our training mixture consists of a small amount of general domain data, which functions as a form of regularization. Since the pretraining dataset for LLaMA 2 is undisclosed, we use the Pile (Gao et al., 2020; Biderman et al., 2022) as a surrogate training dataset. We set 95% of our training mixture to be the $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$, 2% to be from the Pile (with ArXiv removed, as it is separately in $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$), and 3% to be the GitHub subset of RedPajama (Computer, 2023).

Further information on dataset composition and a datasheet are in Appendix B and Appendix E, respectively. We publicly release $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ at hf.co/datasets/EleutherAI/proof-pile-2.

2 Model and Training

Each model is initialized from Code Llama (Rozière et al., 2023). Code Llama models are decoder-only transformer language models initialized from Llama 2 (Touvron et al., 2023) and further trained on 500B tokens of code. We continue training the Code Llama models on $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ using a standard autoregressive language modeling objective. We train the 7B model for 200B tokens, and the 34B model for 50B tokens.

We train all models in $\mathsf{bfloat16}$ mixed precision using the GPT-NeoX library (Andonian et al., 2023) across 256 A100 40GB GPUs. We use Tensor Parallelism (Shoeybi et al., 2019) with a world size of 2 for Llemma-7B , and a world size of 8 for Llemma-34B, alongside ZeRO Stage 1 sharded optimizer states (Rajbhandari et al., 2020) across Data Parallel (Goyal et al., 2017) replicas. We use Flash Attention 2 (Dao, 2023) to improve throughput and further reduce memory requirements.

Llemma 7B is trained for $42,000$ steps with a global batch size of 4 million tokens and a 4096 token context length. This corresponds to roughly $23,000$ A100-hours. The learning rate is warmed up to $1\cdot 10^{-4}$ over $500$ steps, then set to cosine decay to $1/30$th of the maximum learning rate over $48,000$ steps. The reason for the discrepancy between the number of training steps and the scheduler length is that we planned to train for $48,000$ steps, but encountered NaN losses after step $42,000$, likely caused by unstable optimization or hardware failures (Elsen et al., 2023).

Llemma 34B is trained for $12,000$ steps with a global batch size of 4 million tokens and a 4096 context length. This corresponds to roughly $47,000$ A100-hours. The learning rate is warmed up to $5\cdot 10^{-5}$ over $500$ steps, then decayed to $1/30$th the peak learning rate.

Before training Llemma 7B, we contract the RoPE (Su et al., 2022) base period of the Code Llama 7B initialization from $\theta=1,000,000$ to $\theta=10,000$. This is 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 (we leave actually doing so to future work). 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, therefore for that model we preserved $\theta=1,000,000$.

Evaluation

Our goal is to evaluate Llemma as a base model for mathematical text. To this end, we compare Llemma models using few-shot evaluation (Brown et al., 2020), and primarily focus on state-of-the-art models that have not been finetuned on supervised examples for the task. First, we evaluate the model’s ability to solve mathematics problems using chain of thought reasoning (Wei et al., 2023) and majority voting (Wang et al., 2023). Our evaluations include MATH (Hendrycks et al., 2021b) and GSM8k (Cobbe et al., 2021), the de-facto standard benchmarks for evaluating quantitative reasoning in language models (Lewkowycz et al., 2022). Second, we explore few-shot tool use and formal theorem proving. Third, we study the effects of memorization and the data mixture. Appendix G contains a preliminary study of supervised finetuning with Llemma.

These tasks involve generating self-contained text solutions to problems expressed in LaTeX or natural language, without using external tools (Lewkowycz et al., 2022). We use the following evaluation:

MATH (Hendrycks et al., 2021b), a dataset with 12.5k problems (5k evaluation) from high-school math competitions. Given a problem statement, the model generates a LaTeXsolution and an answer that must match a reference answer. We follow a similar task implementation to Lewkowycz et al. (2022), using their four-example prompt and evaluating answers for exact string match or SymPy equivalence.

GSM8k (Cobbe et al., 2021), a dataset of middle-school level math word problems. We use the 8-shot prompt from Wei et al. (2023), as Lewkowycz et al. (2022) do not specify their evaluation prompt or number of few-shot examples.

OCWCourses (Lewkowycz et al., 2022), a collection of undergraduate-level STEM problems harvested from MIT’s OpenCourseWare. We use the four-example prompt provided by (Lewkowycz et al., 2022).

MMLU-STEM (Hendrycks et al., 2021a), a subset of 18 out of 57 subjects in the MMLU benchmark. We follow Lewkowycz et al. (2022) and use their provided four-example chain-of-thought prompt.

SAT, we create a dataset consisting of the 32 math questions that do not contain figures from the May 2023 College Board SAT examination, which is after our model’s knowledge cutoff.

We compare with Minerva (Lewkowycz et al., 2022), which continued pretraining the PaLM language model on a dataset of technical content; Code Llama, the initialization of Llemma’s continued pretraining; and Llama 2, the initialization of Code Llama’s continued pretraining on code. For open access models, we report scores computed using our evaluation suite, which is implemented as a fork of the Language Model Evaluation Harness (Gao et al., 2021). For Minerva models, we report benchmark scores from Lewkowycz et al. (2022).

Llemma’s continued pretraining on $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ improves few-shot performance on the five mathematical benchmarks. Llemma 34B improves over Code Llama by 20 percentage points on GSM8k and 13 points on MATH, and Llemma 7B outperforms the proprietary Minerva model. Our approach also outperforms all open-weight language models at the time of writing. We conclude that continued pretraining on $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ is effective for improving a pretrained model’s ability to perform mathematical problem solving.

Llemma is pretrained on a diverse distribution of mathematics-related data, and is not tuned for a particular task. Therefore, we expect that Llemma can adapt to many other tasks via task-specific finetuning and few-shot prompting.

2 Mathematical problem solving with tool use

These tasks involve solving problems with access to computational tools. We evaluate the following:

MATH+Python, the model is prompted to alternately describe a solution step in natural language, then execute that step with code. The final answer is a program that executes to a numeric type or a SymPy object. Our few-shot prompt includes examples that use built-in numeric operations, the math module, and SymPy.

GSM8k+Python, solving a GSM8k word problem by writing a Python program that executes to an integer answer. We use the prompt from Gao et al. (2023).

As seen in Table 3, Llemma improves over Code Llama on both tasks. Its performance on MATH and GSM8k with tools is also higher than its performance on these datasets without tools.

3 Formal mathematics

Interactive proof assistants such as Lean (de Moura et al., 2015), Isabelle (Wenzel et al., 2008), and Coq (Paulin-Mohring, 1989a; b) express mathematics in programming languages that allow for verification. These languages are data scarce compared to mainstream languages, especially in the context of pretraining. For instance, the Stack dataset used to pretrain language models in the BigCode project (Allal et al., 2023) has over 700 gigabytes of Python, compared to 322 megabytes of Lean. Proof assistants also require models to leverage information that is not present in raw source code, such as goal states that contain information about each step of a proof.

$\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$’s $\mathsf{AlgebraicStack}$ contains over 1.5 billion tokens of formal mathematics data, including proof states extracted from Lean and Isabelle formalizations. While a full investigation of formal math is outside the scope of this paper, we evaluate Llemma few-shot on two tasks:

Informal-to-formal proving (Jiang et al., 2023), the task of generating a formal proof, given a formal statement, an informal LaTeX statement, and an informal LaTeX proof. The formal proof is checked by the proof assistant. We use the Isabelle proof assistant and evaluate on miniF2F (Zheng et al., 2021), a benchmark consisting of problem statements from Olympiads and undergraduate coursework. For the prompt, we use 11 (formal statement, informal statement, informal proof, formal proof) examples from Jiang et al. (2023), selecting 7 examples for number theory problems, and 6 examples for all others. We generate a single proof with greedy decoding.

Formal-to-formal proving (e.g., Polu & Sutskever (2020)), the task of proving a formal statement by generating a sequence of proof steps (tactics). At each step, the input is a state $x_{t}$ given by the proof assistant, and the language model’s task is to generate a proof step $y_{t}$ (a sequence of code). The proof step is checked by the proof assistant, yielding a new state $x_{t+1}$ or an error message. The process continues, stopping if a proof is completed or a timeout is reached. We prompt the model using three $(x_{t},y_{t})$ examples. We evaluate on miniF2F (Zheng et al., 2021) using the Lean 4 proof assistant, and use a standard best first search. See Appendix D for more details.

As seen in Table 4, Llemma’s continued pretraining on $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ improved few-shot performance on the two formal theorem proving tasks.

On informal-to-formal proving, Llemma-7b closes 22.1% of the theorems, improving upon its Code Llama initialization and the Sledgehammer prover. The theorems that Llemma proves are often complementary to those proved with Sledgehammer: taking the union of Sledgehammer and Llemma proofs results in 26 new validation proofs (an 11 percentage-point increase), and 17 new test proofs (a 7 point increase); see Appendix Table 11. Prior to our work, the only demonstration of few-shot proof autoformalization used the proprietary Codex model (Jiang et al., 2023).

On Lean 4 formal-to-formal proving, Llemma-7b improves upon its Code Llama initialization, and performs similar to ReProver (Yang et al., 2023), a retrieval-augmented language model finetuned for tactic prediction. Llemma adapts to the task using a 3 example prompt, which to our knowledge is the first demonstration of few-shot tactic prediction for theorem proving by an open model.

4 Impact of data mixture

When training a language model, it is common to upsample high-quality subsets of the training data according to mixture weights (Brown et al., 2020; Gao et al., 2020; Xie et al., 2023). We select mixture weights by doing short training runs on several hand-picked mixture weights, then choosing the one which minimizes perplexity on a set of high-quality held-out text (we use the MATH training set). Table 5 shows the MATH training set perplexity of models trained using different mixtures of arXiv to web to code. Based on these results, we trained Llemma with a ratio of $2:4:1$. 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.

5 Dataset overlap and memorization

We check whether any 30-gram in a test sequence (either an input problem or an output solution) occurs in any OpenWebMath or $\mathsf{AlgebraicStack}$ document. If so, we say that a hit occurred between the sequence and the document. Table 6 shows hits between sequences from MATH and documents from $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$. Using our methodology, around 7% of MATH test problem statements and 0.6% of MATH test solutions have hits. Note that our methodology gives a lower bound on the number of semantically equivalent sequences (e.g., it does not account for alternative phrasing).

We manually inspected 100 uniformly sampled hits between a test problem statement and an OpenWebMath document. 41 of the cases had no solution, which included websites with a list of problems, discussions, or hints. 49 had an alternative solution to the MATH ground-truth solution, but with the same answer. These include solutions that solve the problem differently than the ground-truth, solutions with missing details, and discussions that include the answer. 9 cases had a missing or incorrect answer, and 1 had the same solution as in the ground-truth. In summary, we find that solutions can appear in a corpus derived from web documents, particularly alternative solutions to those in the evaluation set. We repeated our analysis with 20-gram hits and our findings were similar, though with false positives; see Appendix Figure 6 for examples.

Next, we evaluate Llemma-34b on the test examples with a 30-gram hit, and the test examples without a 30-gram hit. Table 7 shows the accuracy partitioned by MATH difficulty level. The model’s accuracy remains low on difficult problems (e.g., 6.08% on Level 5 problems with a hit, versus 6.39% on problems without a hit), and we observe no clear relationship between 30-gram hits and accuracy across difficulty levels. We conclude that a nontrivial match between a test example and a training document did not imply that the model generated a memorized correct answer. We repeated the analysis with 20-grams and with the 7b model, and our findings were analogous. Figure 7 shows an example.

Finally, we check 30-gram hits between Llemma’s MATH generations and OpenWebMath. There were 13 hits, which occurred when the model generated a common sequence of numbers (e.g., a list of Fibonacci numbers), plus one instance of factoring a polynomial. Appendix Figure 6 shows an example. We find all of these observations worthy of further study. Using Llemma and $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ to better understand data, memorization, and performance is an interesting future direction. We include the code for our analysis in the Llemma repository.

Related Work

Large-scale language modeling. Recent progress in large language models involves two connected threads: the increasing scale of models and data (Hoffmann et al., 2022; Kaplan et al., 2020; Chowdhery et al., 2022), and a progression toward more generalist models (Radford et al., 2019; Brown et al., 2020) which are capable of solving diverse problems and adapting quickly to novel tasks. A third thread relates to enabling open access to language models with these capabilities (Black et al., 2022; Biderman et al., 2023; Touvron et al., 2023; Rozière et al., 2023). Our work provides a recipe for specializing these language models to the domain of mathematics, providing a platform for further research and applications.

Domain adaptation. Language model applications typically require a general-domain pretraining step, followed by a shorter fine-tuning step. The finetuning step is often aimed at imbuing instruction-following ability (Sanh et al., 2022; Wei et al., 2022) or aligning a model’s outputs with human preferences (Ziegler et al., 2019; Ouyang et al., 2022; Bai et al., 2022). Other work explores adapting pretrained models to novel domains by continued training (Rozière et al., 2023; Beltagy et al., 2019), parameter-efficient finetuning methods (Yong et al., 2023), retrieval augmentation (Min et al., 2023; Asai et al., 2023), and other techniques. We provide an adaptation recipe involving continued training and targeted data collection.

Language models for mathematics. Applying large language models to problems in mathematics is an active subfield of machine learning, including benchmarking mathematical knowledge and reasoning at varying levels (Hendrycks et al., 2021b; Zheng et al., 2021; Welleck et al., 2022; Azerbayev et al., 2023). Although achieving strong mathematical reasoning is an important target, it is difficult to assess the correctness of models’ answers and processes, especially as models become more capable (Bowman et al., 2022; Uesato et al., 2022; Lightman et al., 2023; Cobbe et al., 2021).

A number of recent works focus on supervised finetuning on task-relevant (input, output) pairs (e.g.,Yu et al. (2023); Yue et al. (2023)). Doing so boosts performance on some common mathematical language modeling benchmarks, but trains the model for these specific tasks. In contrast, Lewkowycz et al. (2022) and our work seek to train a base language model as a platform for further development.

Language models for formal mathematics. An ongoing line of work explores integrating language models with interactive proof assistants in the context of mathematics. This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023). Due to high computational costs of search, language models applied to this domain have traditionally been small, but recent work has demonstrated promise in the use of larger models (First et al., 2023; Jiang et al., 2023). Our work provides a demonstration of few-shot proof autoformalization and tactic prediction, a large collection of formal mathematics data, along with an open access model for further exploring these directions.

Conclusion

We introduce Llemma and $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$, a novel base model and corpus for language modeling of mathematics. Our models, dataset, and code are openly available. We have shown that Llemma achieves state-of-the-art results for open-weights models on mathematical problem solving benchmarks, shown capabilities of using external tools via Python code, and demonstrated few-shot tactic prediction for theorem proving. We hope that Llemma and $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$ will be a useful base for future work on understanding language model generalization and dataset composition, investigating the limits of domain-specific language models, using language models as tools for mathematicians, and improving the mathematical capabilities of language models.

Acknowledgements

We would like to thank Dragomir Radev, Arman Cohan, Jesse Michael Han, and the Deepmind Blueshift team for valuable guidance. We thank Jonah Philion for the model name. We thank Aviya Skowron for advising us on ethical considerations in the development and release of our models. We thank Jonathan Laurent and Leo Du for contributions to our open-source code.

We would also like to thank several parties for donating computing resources for this project: Stability AI (training the Llemma models), CoreWeave (evaluations and finetuning), the Province of Ontario and companies sponsoring the Vector Institute for Artificial Intelligence (www.vectorinstitute.ai/partners), and Brigham Young University (finetuning). KP is supported by an NSERC PGS-D award.

References

Appendix A Author Contributions

Training Data. Zhangir Azerbayev, Keiran Paster, Marco Dos Santos, Sean Welleck.

Model training. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster.

Evaluations. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Sean Welleck.

Memorization analysis. Sean Welleck, Keiran Paster.

Senior Authorship and Advising. Jia Deng, Stella Biderman, Sean Welleck.

Appendix B Data: 𝖯𝗋𝗈𝗈𝖿𝖯𝗋𝗈𝗈𝖿\mathsf{Proof}-𝖯𝗂𝗅𝖾𝖯𝗂𝗅𝖾\mathsf{Pile}-𝟤2\mathsf{2}

$\mathsf{AlgebraicStack}$ contains roughly 11B tokens of code related to mathematics. We describe its sources, filtering, and content below. Table 9 shows the number of tokens per language in $\mathsf{AlgebraicStack}$.

The following programming languages were either barely present in the Stack or consisted of largely incorrect filetypes, so we downloaded data for these languages directly via the Github Python API.

Coq : We filter for files with the .v extension, and include Coq via including files that match a heuristic filter for the keywords "Theorem", "Proof", "Qed", "Inductive", "Definition", "Fixpoint" and exclude Verilog files via the keyword blacklist "pragma", "endmodule", "posedge", "negedge", "wire". We additionally exclude files noted as automatically generated.

Isabelle : We filter for files with the .thy extension and include files matching the keyword whitelist "theorem ", "lemma ". We keep only isabelle-prover/mirror-afp-devel and discard all other older copies of the Archive of Formal Proofs. We further remove theorem statements and proofs that have a theorem name in the PISA (Jiang et al., 2021) test set.

Lean : We filter for files with the .lean extension, using the keyword whitelist "theorem ", "lemma ", "example ". We remove all dependency files, and in order to avoid known benchmark contamination, we blacklist the ProofNet and MiniF2F repositories. We further remove theorems or lemmas that share a theorem name with the LeanDojo (Yang et al., 2023) val or test sets.

MATLAB : We filter for files with the .m extension, using the keyword whitelist "#import", "interface", "implementation", "property", and blacklist C files via the keywords "#include" and the regex r’ main$\backslash$(.*{$’

We implemented a cutoff date for our Github API downloads, and used a cutoff date of April 1, 2023.

For all languages, unless otherwise stated, we additionally filtered out files with a filesize greater than $1048575$ bytes or with a numerical density (ratio of digit characters to non-digit characters) of $0.5$. We additionally perform document-level exact deduplication by removing documents which contain an overlapping 2048-character chunk as another document.

B.1.2 Lean proofsteps

We extract a dataset of (tactic state, next tactic) pairs from Mathlib 4 (mathlib Community, 2020) using the lean-training-data (Morrison, 2023) tool. We use Mathlib 4 commit c779bd5, which was created on August 20th 2023.

B.1.3 Isabelle Proofsteps

We construct a dataset of Isabelle proofs, building upon the PISA dataset Jiang et al. (2021). Isabelle Proofsteps comprises proofs from the Archive of Formal Proofs and Isabelle Standard Library, scraped with PISA Jiang et al. (2021). Each entry in the dataset includes the theorem statement, the proof states and the proof steps, separated by specific tags. To maintain the integrity of evaluations using the PISA test set, we decontaminate Isabelle Proofsteps by removing theorems whose names overlap with those in the PISA test set. Although this approach results in a strict filtering – removing more than 10,000 theorems although there are only 3600 in the PISA test set – we consider it acceptable in order to mitigate data contamination. After filtering, Isabelle Proofsteps contains 251,000 theorems.

B.1.4 Stack Filtering

We source the following programming languages from the Stack (Kocetkov et al., 2022) dataset, and describe our filtering process and quality issues we chose to mitigate beyond our default quality heuristics:

C : We include documents based on a keyword whitelist, namely: "#include ", "#include ", "#include ", "#include ", "#include ", "#include ", "#include ", "#include ".

C++ : We include documents based on a keyword whitelist, namely: "#include ", "#include ", "#include , "#include

Haskell : We filtered the data to only contain files with the following imports: Numeric.LinearAlgebra, Numeric.SpecFunctions, Numeric.Vector, Statistics, Data.Complex.

Julia : We filtered out mislabeled JSON lines files. We removed files larger than 10,000 characters long which both were not files containing tests and which had a lower numerical density than $0.5$, and otherwise ignored numerical density. We additionally only accepted files within a specific keyword whitelist, to attempt to control relevance to scientific computing, namely: "LinearAlgebra", "DifferentialEquations", "Symbolics", "Distributions", "DataFrames", "DynamicalSystems", "Turing", "Gen", "JuMP", "sqrt", "abs", "zeros", "ones", "sin", "cos", "tan", "log", "exp", "integrate", "likelihood", "Matrix", $\pi$, "pi", "rand", "grad".

Jupyter : We found that many Jupyter notebook files were large due to containing long cell outputs, such as base64 images, long tracebacks, or other extra JSON cell metadata. We use nbconvert to convert notebooks to a markdown format, removing metadata.

Maple : We filtered out files with a size greater than $100,000$ bytes, and found that some files were XML. We filtered all files beginning with an XML declaration.

Python : We filtered notebooks and JSON files out by excluding documents with beginning "{" characters, and included only files importing from a fixed list of libraries.

R : We excluded all files beginning with an XML declaration. We additionally filtered out all notebooks, and filtered all files containing MacOS "Resource Fork" files.

Tex : We used a max file size of 10,000,000 bytes. We excluded tex files found in directories named "latex/" because these were often auto-generated files, and excluded documents using gnuplot. We included only documents containing one of the keywords " $\backslash$chapter{", "$\backslash$chapter*{", "$\backslash$section{", "$\backslash$section*{", "$\backslash$subsection{", "$\backslash$subsection*{", "$\backslash$subsubsection{", "$\backslash$subsubsection*{", "$\backslash$paragraph{", "$\backslash$subparagraph{", and additionally only included documents identified as English by a classifier from the langid package.

For all languages we used within the Stack, unless otherwise stated, we additionally filtered out files with a filesize greater than $1048575$ bytes or with a numerical density (ratio of digit characters to non-digit characters) of $0.5$.

We used v1.2 of the near-deduplicated Stack as a base for processing.

B.2 Papers: Arxiv

We use the entirety of ArXiv, as accessed by Computer (2023) in April 2023. For further information on preprocessing applied to ArXiv, see Computer (2023).

B.3 Web: OpenWebMath

For the web portion of our training dataset, we use OpenWebMath (Paster et al., 2023).

Appendix C Evaluation Harness

We implement a variety of math-related tasks and evaluation protocols into a public fork of the Language Model Evaluation Harness (Gao et al., 2021). The Harness provides a model-agnostic framework for standardized, reproducible evaluation of language models.

We add the following tasks for the evaluations in this paper:

hendrycks_math_ppl: Perplexity evaluation on MATH (Hendrycks et al., 2021a) sub-tasks.

minif2f_isabelle: Proof autoformalization in Isabelle on the miniF2F benchmark based on Jiang et al. (2023), with a Portal-to-Isabelle (Jiang et al., 2021) proof checker.

minerva_math: The MATH benchmark with the prompt and Sympy evaluation from Minerva (Lewkowycz et al., 2022).

minerva-hendrycksTest: MMLU-STEM tasks following Lewkowycz et al. (2022).

ocw_courses: The OCW Courses task from Lewkowycz et al. (2022).

python_gsm8k: GSM8k with Python, based on Gao et al. (2022).

We include a link to the implementations for these tasks, including full prompts, in our public codebase.

Appendix D Evaluation: Experiment Details

We follow Jiang et al. (2023), allowing the model to issue a call to built-in Isabelle automation in the output proof by generating sledgehammer. This calls Sledgehammer (Paulson & Nipkow, 2023) and the list of heuristics listed in Jiang et al. (2023). Following Jiang et al. (2023), as a baseline we use Sledgehammer and the heuristics executed at the beginning of the proof (referred to as Sledgehammer in the main text for brevity). We use a 30-second timeout for Sledgehammer and implement proof checking via Portal-to-Isabelle (Jiang et al., 2021). Refer to the implementation in the Evaluation Harness for further details.

D.2 Lean Theorem Proving

Theorem proving via tactic prediction involves interacting with a proof assistant after each step of a proof. Implementing these interactions within the evaluation harness is outside the scope of this work. Therefore, for the Lean theorem proving task we use a separate evaluation setup based on an open-source implementation (Welleck, 2023). We include our evaluation code in our public codebase.

We evaluate on miniF2F (Zheng et al., 2021), which consists of 488 formalized statements from math competitions and undergraduate coursework. Given a formalized statement, the task is to generate a formal proof that is checked by Lean.

We use best first search, commonly used for neural tactic prediction models (e.g., Polu & Sutskever (2020)). Best first search is parameterized by the number of attempts (N), generated tactics per iteration (S), and maximum iterations (T). We define the search budget to be the maximum number of generated tactics, $N\times S\times T$. We set our search budget to $N=1$, $S=32$, and $T=100$, less than that of the baseline model. Following Yang et al. (2023), we generate tactics with beam search and use a 10 minute timeout. We adapt the proof search implementation from Welleck (2023), which uses LeanDojo v.1.1.2 (Yang et al., 2023) for interaction. We use Lean 4 miniF2F, using https://github.com/rah4927/lean-dojo-mew commit d00c776260c77de7e70125ef0cd119de6c0ff1de. Note that the ReProver baseline from (Yang et al., 2023) reports performance with Lean 3.

Prompt. We prompt the model with three (state, tactic) examples, shown in Figure 5.

Appendix E Datasheet

We provide a datasheet for $\mathsf{Proof}$-$\mathsf{Pile}$-$\mathsf{2}$, following the framework in Gebru et al. (2021).

Appendix F Additional Results

Table 11 shows additional results on Isabelle proof autoformalization, including the union of theorems closed by Sledgehammer and the given language model.

Appendix G Supervised Finetuning

A full exploration of finetuning applications for Llemma, such as instruction following (Ouyang et al., 2022; Wei et al., 2022), dialogue modeling (Thoppilan et al., 2022; Touvron et al., 2023; Collins et al., 2023), and reward modeling (Cobbe et al., 2021; Lightman et al., 2023) are outside the scope of this work. However, to establish that Llemma retains its advantage over other open models when finetuned, we conduct preliminary experiments finetuning Llemma-7B on MetaMathQA (Yu et al., 2023), a supervised dataset targeted at the MATH and GSM8k benchmarks. Results are shown in Table 12.

Appendix H Qualitative Examples

Figure 6 shows example false positives when checking $n$-gram overlap with OpenWebMath documents for various $n$. Figure 7 shows an example OpenWebMath document that has 30-gram overlap with a MATH problem, and Llemma-7b’s generated solution.

Figure 8 shows a generated proof in the informal2formal theorem proving task.