Llemma: An Open Language Model for Mathematics
Authors: Zhangir Azerbayev
Hailey Schoelkopf
Keiran Paster
Marco Dos Santos
Stephen Marcus McAleer
Albert Q. Jiang
Jia Deng
Stella Biderman
Sean Welleck
Venue: ICLR 2024 poster (2024)
Keywords: reasoning
language models
pretraining
Primary area: generative models

Abstract: We present Llemma, a large language model for mathematics. We continue pretraining Code Llama on the Proof-Pile-2, a mixture of scientific papers, web data containing mathematics, and mathematical code, yielding Llemma. On the MATH benchmark Llemma outperforms all known openly released models, as well as the unreleased Minerva model suite on an equi-parameter basis. Moreover, Llemma is capable of tool use and formal theorem proving without any finetuning. We openly release all artifacts, including 7 billion and 34 billion parameter models, the Proof-Pile-2, and code to replicate our experiments.

Published as a conference paper at ICLR 2024
LLEMMA: AN OPEN LANGUAGE MODEL FOR MATHEMATICS
Zhangir Azerbayev 1.2
Hailey Schoelkopf"
Keiran Paster 3,4
Marco Dos Santos
Stephen McAleer
Albert Q. Jiang
Jia Deng'
Stella Biderman 2
Sean Welleck
Princeton University
EleutherAI
University of Toronto Vector Institute Uniiersity of Washington
5 University of Cambridge
Carnegie Mellon University
ABSTRACT
We present LLEMMA, large language model for mathematics. We continue pretraining Code Llama on Proof-Pile-2. a mixture scientific papers, web data containing mathematics, and mathematical code, yielding LLEMMA. On the MATH benchmark LLEMMA outperforms all known open base models, as well as the unreleased Minerva model suite is capable of tool use and formal theorem proving without any further finetuning. We openly release all artifacts, including 7 billion and 34 billion parameter models, the Proof-Pile-2 and code to replicate our experiments
equi-parameter basis. Moreover, LLEMMA
INTRODUCTION
4-Shot MATH Performance
Language models trained on diverse mixtures of text display remarkably general language understand- ing and generation capabilities (Brown al. 2020 Chowdhery et al. (2022), serving as base models that are adapted to a wide range of applications (Raffel
50%
45%
Llemma 34B
MATTH Maj@256 (Aecuracy)
Minerva 62B
jet al. 2023). Applications such open-ended dia-
logue (Thoppilan et al., 2022: Touvron et al. 2023
35%
or instruction following (Ouyang al. 2022 Wei
cet al. 2022) require balanced performance across the
Llemma 7B
entire distribution of natural text, thus favoring gen-
30%
eralist 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- domain-speciife language model may offer superior capabilities for a given computational cost, or lower computational cost for given level of capability.
25%
Minerva 8B
Params
Continued pretraining on Proof- Pile-2 yields LLEMMA, base model with improved mathematical capabilities.
Figure 1:
In this work, we train a domain-specinf 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 mathematical reasoning in itself central Al task, its study dating back to at least Gelernter (9559)
ideal setting for domain adaptation. Second,
and [Wang] (1960) and continuing to today (Lu al.) (023). Third, language models capable of strong mathematical reasoning are upstream of a number of research topics, such as reward modeling
(Uesato al.
2022 Lightman al. (202)), reinforcement learning for reasoning (Polu al. 2022
Lample et al. 2022 and algorithmic reasoning (Zhou et al. 2022 Zhang et al. 2023).
https::/github.ccmm

---

Published as a conference paper at ICLR 2024
Although commain-speciffe 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 ofate-of-the-art (Azerbayev et al. 2023).
We present a recipe for adapting a language model to mathematics through continued pretrain- ing (Lewkowyez al. 2022 Rozière et al. 2023) on Proof-Pile-2, diverse mixture of math-related text and code. Applying the recipe to Code Llama (Rozière et al.] (023) yields LLEMMA: 7 billion and 34 billion parameter base language models with substantially improved mathematical capabilities.
Specifically, our contributions are as follows:
1. We train and release the LLEMMA models: 7B and 34B parameter language models specialized for mathematics. The LLEMMA models are state-of-the-att for publicly released base models on MATH (Lewkowycz et al. 2022).
We release the AlgebraicStack, dataset of IIB 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.
4. Unlike prior mathematics language models such Minerva (Lewkowycz et al. 2022). the LLEMMA models are open access and we open source our training data and code. This allows LLEMMA to
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 's training and evaluation covers wider range of data and tasks, notably code data (e.g., the AlgebraicStack), tool use, and formal mathematics; (2) our work only depends publicly accessible tools and data; (3) we provide new analyses related to the continued training data mixture, memorization, and additional supervised finetuning: (4) 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 Proof-Pile.2
Dataset
Tokens Open
Model
Adaptation tokens Open
Minerva Dataset
38.5B
X
Minerva-8b
164B X
Proof-Piles (ours)
55B
/
Minerva-62b
109B
Code (AlgebraicStack)
11B
LLEMMA-7h (ours)
200B
V
OpenWebMath (Paster ArXiv (Computer 2023)
2023
15B
LLEMMA- (ours)
50B
29B
Figure 2: Comparison of LLEMMA and Minerva training
2.1
DATA: Proof-Pile-2
We form the Proof-Pile-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 Proof-Pile-2 has knowledge cutoff of April 2023.
Code. Computational tools such numerical simulations, computer algebra systems, and formal theorem provers are of ever increasing importance to mathematicians (Avigad 2018). Motivated by this fact, we create AlgebraicStack, numerical, symbolic, and formal math. The dataset consists of filtered code from the Stack (Kocetkov al.) 2022)), public GitHub repositories, and formal proofstep data. Table ( shows the number of tokens by language in AlgebraicStack. See Appendix B.I for further details on AlgebraicStack.
1BB-token dataset of source code from 17 languages, spanning
Web data. We use OpenWebMath (Paster et al. 2023). 15B-token dataset of high-quality web pages filtered for mathematical content. Open WebMath filters CommonCrawl web pages based
2

---

Published as a conference paper at ICLR 2024
on math-related keywords and classifier- based math score, preserves mathematical formatting (e.g., 15TE,, AsciiMath), and includes additional quality filters (c.g., perplexity, domain, length) and near-deduplication. Refer to Paster et al. (2023 for a full description of OpenWebMath.
Scientific papers. We use the ArXiv subset of RedPajama (Computer 2023), an open-access reproduction of the LLaMA training dataset. The ArXiv subset contains 29B tokens.
General natural language and code data. Following Lewkowycz et al. (2022), our training
mixture consists of small amount of general domain data, which functions as a form of regularization.
Since the pretraining dataset for LLaMA 2 undisclosed, we use the Pile (Gao al. 2020; Biderman et al. (022) as a surrogate training dataset. We set 95% of our training mixture to be the Proof-Piles
2% to from the Pile (with ArXiv removed, as it is separately in Proof-Pile-2), and 3% to be the
GitHub subset of RedPajama (Computer 2023).
Further information on dataset composition and a datasheet are in Appendip Appendd re- spectively. We publicly release Proof-Pile-2 at lff co/ htt//aaaatts/eecutttateee htt.aaacceeeeeltttaccaaaaroooooo
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 (Tuvronn et al. (023) and further trained on 500B tokens of code. We continue training the Code Llama models on Proof-Pile-2 using 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 bfloat16 mixed precision using the GPT-NeoX library (Andonian et al. 2023) across 256 A100 40GB GPUs. We use Tensor Parallelism (Shocybi et al. 2019) with world size of 2 for LLEMMA- TEEMA--B-- AB7B and a world size of 8 for LLEMMA-34B, alongside ZeRO Stage sharded optimizer states (Rajbhandari al., 2020) across Data Parallel (Goyal et al.) 2017) replicas. We use Flash Attention 2 (Dao (023) to improve throughput and further reduce memory requirements.
LLEMMA 7B is trained for 42, 000 steps with a global batch size of million tokens and a 4096 token context length. This corresponds to roughly 23, 000 A A100-hours. The learning rate is warmed up to 1-10-4 over 500 steps. then set to cosine decay to 1/30th of the maximum learning rate over 48, 000 steps. The reason for the discrepancy between the number of training steps and the scheduler length that we planned 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 trained for 12, 000 steps with global batch size of million tokens and a 4096 context length. This corresponds to roughly 47, 000 A100-hours. The learning rate is warmed up to 5 10-5 over 500 steps, then decayed to 1 1/30th 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 / = 1, 000, 000 to 0 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 performance penalty, therefore for that model we preserved 1, 000, 000.
3 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., (020). and primarily focus on of-te- 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. 202 and GSM8k (Cobbe et al. 2021). the de-facto standard benchmarks for evaluating quantitative reasoning in language models Lewkowyez et al.) (022). Second, explore few-shot tool use and formal theorem proving. Third, we study the effects of memorization and the data mixture. Appendix G contains preliminary study of supervised finetuning with L.FEMMA.
3

---

Published as a conference paper at ICLR 2024
3.1 CHAIN-OF-THOUGHH MATHEMATICAL PROBLEM SOLVING
These tasks involve generating self-contained text solutions to problems expressed in ВTμ or natural language, without using external tools (Lewkowyez et al. 2022). We use the following evaluation:
MATH (Hendrycks et al. 2021b), dataset with 12.5k problems (5k evaluation) from high-school math competitions. Given problem statement, the model generates a LSTpSsolution and an answer that must match reference answer. We follow similar task implementation to Lewkowyez et al. (2022). using their four-example prompt and evaluating answers for exact string match or SymPy equivalence.
dataset of middle-school level math word problems. We the 8-shot prompt from Wei et al. (022)) as Lewkowycz et al. (2022) do not specify their evaluation prompt number of few-shot examples.
GSM8k (Cobbe al. 2021
OCWCourses (Lewkowycz et al. 2022) collection of undergraduate- STEM problems
harvested from MIT's OpenCourse We use the four-example prompt provided by (Lewkowycz
et 2022).
MMLU-STEM (Hendrycks al. 202 subset of 18 of 57 subjects in the MMLU benchmark. We follow Lewkowyez et al. 2022) and use their provided four-example chain-of- thought prompt.
SAT, create dataset consisting of the 32 math questions that do contain figures from the May 2023 College Board SAT examination, which is after our model's knowledge cutoff.
Input:
2008 Let [(r) Σド=
Find Exe
2k=2 f(k).
LLEMMA 34B solution:
We have
8
((k)
ΣΣ
00
2008
2008 20
ΣΣ
Σ
2008
1
06
1
2008
j
k= j=2
j=2
J=2
3=2
2008
2008
Σ
Σ
J-2 j(j 1)
1-1 -
3
1
2 +
1
....
2 3
2007
2008
=
2008
2007
2008
Final Answer: The final answer is
2007
2008
Figure 3: Example of LLEEMAA 34B solution to MATH (Hendrycks et al. (021a) problem. This problem is tagged with difficulty level 5, the highest in MATH. The model was conditioned on the 4-shot prompt described in sssubeection 3.1] and the solution was produced by greedy decoding. The model had to apply two nontrivial steps solve this problem: (1) noticing that swapping the order of summation simplifies the problem, and (2) noticing that the resulting sum telescopes.
We compare with Minerva (Lewkowyez et al. 2022), which continued pretraining the PaLM language model on dataset of technical content; Code Llama, the initialization of LLEMMA'S 's continued pretraining; and Llama the initialization Code Llama's continued pretraining on code. For open access models, we report scores computed using evaluation suite, which is implemented fork of the Language Model Evaluation Harness (Gao et al. 202T). For Minerva models, we report benchmark scores from Lewkowycz et al. (2022
4

---

Published as a conference paper at ICLR 2024
Results. LLEMMA's continued pretraining Proof-Pile-2 improves few-shot performance the five mathematical benchmarks. LLEMMA 34B improves over Code Llama by 20 percentage points on GSM8K and 13 points MATH, and LLEMMA 7B outperforms the proprictary Minerva model. Our approach also outperforms all open-weight language models at the time of writing. We conclude that continued pretraining Proof-Pile-2 is effective for improving pretrained model's ability to perform mathematical problem solving.
diverse distribution of mathematics-rrlatee data, and tuned for particular task. Therefore, we expect that LLEMMA can adapt to many other tasks via task-specific finetuning and few-shot prompting.
LLEMMA is pretrained
GSM8k
OCW
MMLU-STEM
SAT
MATH
Llama 2
7B
11.8%
3.7%
29.9%
25.0%
3.2%
Code Llama
7B
10.5%
4.4%
25.1%
9.4%
4.5%
Minerva
8B
16.2%
7.7%
35.6%
14.1%
LLEMMA
7B
36.4%
7.7%
37.7% %
53.1%
18.0%
Code Llama
34B
29.6%
7.0%
40.5%
40.6%
12.2%
LLEMMA
34B
51.5%
11.8%
49.0%
71.9%
25.0%
Minerva
62B
52,4%
12.0%
53.9%
27.6%
Minerva
540B
58.8%
17.6%
63.9%
33.6%
Table 1: Results
five chain-of-thouge of-thought reasoning tasks with samples generated via greedy decoding. Minerva results are quoted from Lewkowycz et al. (2022). Note that CodeLlama 7B performs worse than random guessing (25%) MMLU and SAT, largely due failing conclude its chain of thought with valid answer.
GSM8k
OCW
MMLU-STEM maj @k
SAT maj@ mk
MATH maj @ k
maj @ le
maj @k
Minerva
8B
28.4%
12.5%
43.4%
25.4%
LLEMMA
7B
54.0% %
14.3%
49.9%
78.1%
33.5%
LLEMMA
34B
69.3%
18.4%
59.7%
81.3%
43.1%
Minerva
62B
68.5%
23.5%
63.5%
43.4%
Minerva
540B
78.5%
30.8%
75.0%
50.3%
Table 2: Majority voting results for LLEMMA and Minerva. Minerva results are quoted from Lewkowyez et al. (2022). Voting is done with 256 for MATH, k 100 for GSM8k and OCW, and & 16 for MMLU-STEN. and SAT. We sample with temperature
0.6 for i: 256 and k 100 and T 0.3 for & 16, and use nucleus sampling with p 0.95 (Holtzman et al. 2020). Due to compute constraints, we do not calculate majority voting scores for I.lama 2 and Code I.ama.
3.2 MATHEMATICAL PROBLEM SOLVING WITH TOOL USE
These tasks involve solving problems with access computational tools. We evaluate the following:
MATH+Python, the model is prompted alternately describe solution step in natural language, then execute that step with code. The final answer is program that executes to a numeric type or SymPy y object. Our few-shot prompt includes examples that built-in numeric operations, the math module, and SymPy.
GSM8k+Python, solving GSM8k word problem by writing Python program that executes an integer answer. We use the prompt from Gao et al. (2023).
Results. 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 these datasets without tools.
5

---

Published as a conference paper at ICLR 2024
GShon+Python pass @
MATH+PPthon
pass @ 1
Code Llama
7B
27.1%
17.2%
LLEMMA
7B
40.1%
21.5%
Code Llama
34B
52.7%
23.5%
LLEMMA
34B
62.6%
27.1%
Table 3: Mathematical problem solving with tool use.
3.3 FORMAL MATHEMATIC'
Interactive proof assistants such Lean (de Moura 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 scaree compared 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 proof.
Problem (MATH Number theory 185): When a number is divided by 5, the remainder 3. What is the remainder when twice the number is divided by 5? Show that it is
Human- informal proof: If our number n, then n = 3 (mod 5). This tells that
2n n + = 3 1
(mod 5).
The remainder is when the number is divided by 5.
Informal-to-forane (Isabelle): (Problem, human-written informal proof)
Formal-to-formal (Lean 4):
theorem mathd_nunberrheocyyuu (n : N) (ho n 3)
theorem mathi_ caanhhi_nnberthory__tt
fixes n ::nat
2 $
5
by
assumes "n mod 5 = 3"
shows n) mod 1"
INPUT (step 1):
n: N ho n 8
proof
} 2 x 8 5 Tw [mul_mod, bo]
have "2
n² <AIP>
also have " mod
(n mod + n mod 5) mod 5" <APP>
INPUT (step 2) N
also have "... (3 + 3) mod 5"
using assms <ATP>
ho n
also have ". 1" <ATP>
+ 2 8 3 1
finally show 7hessi <ATP>
simp only [ha, mul_one]
qed
Example formal proofs from LLEMMA-77 7b. Left: The model is given a problem, informal proof, and formal statement, following Jiang et al. (023). It generates formal proof (starting with proof -) containing Isabelle code and calls to automation (shown as <ATP>). Right: The model is given proof state, visualized grey comment, and generates the subsequent step (e.g. rw (..).
Figure 4:
Proof-Pile-2's 2'se-2's AlgebraicStack contains 1.5 billion tokens of formal mathematics data, including proof states extracted from Lean and Isabelle formalizations. While a full investigation formal math is outside the scope of this paper, we evaluate L.LEMMA few-shot on two tasks:

---

Published as a conference paper at ICLR 2024
Informal-to-format proving (Jiang al. 2023). the task of generating a formal proof, given formal statement, an informal L8TxX statement, and an informal 15T proof. The formal proof is checked by the proof assistant. We use the Isabelle proof assistant and evaluate miniF2F (Zheng (et al. 2021), a benchmark consisting of problem statements from Olympiads and undergraduate coursework. For the prompt,
11 (formal statement, informal statement, informal proof, formal proof) examples from Jiang et al. (2023), selecting 7 examples for number theory problems, and examples for all others. We generate single proof with greedy decoding.
Formal-to-formal proving (e.g., Polu & Sutskever (2020), the task of proving formal statement by generating sequence of proof steps (tactics). At each step, the input is state 2t given by the proof assistant, and the language model's task is to generate proof step y/ (a sequence of code). The proof step is checked by the proof assistant, yielding new state J++1 an error message. The process continues, stopping if a proof completed or a timeout is reached. We prompt the model using three (Ir, 1/5) 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 performance on the two formal theorem proving tasks.
Results.
LLEMMA'S 's continued pretraining on Proof-Pile-2 improved few-shot
Method
informal-to-orrmal
Method
Formal-to-formal
miniF2F-valid
miniF2F-test
Search
miniF2F-test
Sledgehammer
14.72%
20.49%
ReProver (fine-tuned)
1x
26.50%
Code Llama 7b
16.31%
17.62%
Code Llama 7b
1x32
20.49%
Code Llama 34b
18.45%
18.03%
Code Llama 34b
1x32 _1
22.13%
COPRA (GPT-4)
23.36%
LLEMMA-TH 7b
20.60%
22.13%
LLEMMA-344
21.03%
21.31%
LLEMMA-7b
1x32
26.23%
LLEMMA-346
1x32
25.82%
Table 4: Formal theorem proving tasks. Left: frormal-to-format proving in Isabelle, showing the percentage of proven theorems with greedy decoding. Right: tommal-oo-formal proving in Lean, showing the percentage of proven theorems with the given number of attempts x generations-pe -priiioo-------- iteration of best first search, and 10-minute timeout. Sledgehammer (Paulson & Nipkow 2023) is built-in Isabelle automation. ReProver (Yang et al.] 2023) is a supervised and -arimeee-- model. COPRA (Thakur et al. 2023) is retrieval-augmentte GPT-4 based method. COPRA does not use best first search, but instead samples from GPT-4 (OpenA 2023) maximum of 60 times.
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 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 17 Prior
On
work, the only demonstration of few-shot proof autoformalization used the proprictary 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-augmeened language model finetuned for tactic prediction. LLEMMA adapts 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.
3.4 IMPACT OF DATA MIXTURE
When training a language model, common upsample high-quality subsets of the training data according to mixture weights (Brown et al. 20200 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 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 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.
7

---

Published as a conference paper at ICLR 2024
Mixture
MATH training set perplexity
Number
Counting & Probability
Intermediate Algehra
Overall
Prealgebra
Algebra
Geometry
Precalculus
Theory
2:4:1
1.478
1.495
1.515
1.552
1.475
1.519
1.439
1.331
2:4:2
1.482
1.500
1.519
1.477
1.524
1.443
1.334
4:2:1
1.487
1.505
1.524
1.561
1,481
1.534
1.447
1.338
4:2:2
1.489
1.508
1.527
1.562
1.483
1.538
1.447
1.339
4:4:1
1.506
1.525
1.561
1.482
1.529
1.446
1.335
4:4:2
1.485
1.503
1.523
1.559
1,480
1.529
1.444
1.334
Table 5: MATH training set perplexity Code Llama 7B models trained using different data mixtures for reduced number of steps. Each mixture is represented by its noxe ratio.
3.5 DATASET OVERLAP AND MEMORIZATION
Do test problems or solutions appear in the corpus? We check whether any 30-gram in test sequence (either an input problem or an output solution) occurs in any GeetWhhtath or AlgebraicStack document. If so, we say that a hir occurred between the sequence and the document. Table shows hits between sequences from MATH and documents from Proof-Pile-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 lower bound on the number of semantically equivalent sequences (c.g., e.. does not account for alternative phrasing).
We manually inspected 100 uniformly sampled hits between a test problem statement and an Open- WebMath document. 41 of the cases had no solution, which included websites with 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 tround-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 in the ground-truth. In summary, 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.
find that
Problem Example Does Example Does
Solution
Same solution
Proof-Piles
Test
Different solution, answer Different solution, different answer No solution Different problem
49
OpenWebMath MATH
348
717
34
46
AlgebraicStack MATH
1
41
OpenWebMath GSM8K
AlgebraicStack GSM8k
0
0
Table 6: Left: 30-gram hits between MATH test problems or solutions and Proof-Pite Proof-Pile-2 documents. Example and Docs are the numbers of unique test examples and Proof-Pile-2 documents with a hit. Right: manual inspection of 100 hits between problem statement and Proof Proef-Pile-2 document.
How do problems in the corpus impact performance? Next, we evaluate LLEMMA-34b on the test examples with 30-gram hit, and the test examples without 30- gram hit. Table shows the accuracy partitioned by MATH difficulty level. The model's 's accuracy remains low on difficult problems (c.g., 6.08% on Level prob- lems with a hit, versus 6.39% on problems without hit), and we observe no clear relationship between 30-gram hits and accuracy across difficulty levels. We conclude that nontrivial match between test example and a training document did not imply that the model gen- erated memorized correct answer. We repeated the analysis with 20-grams and with the 7b model. and our findings analogous, Figure 7 shows example.
MATH
Hit
Nonhit Accuracy
# Hits
Level
Accuracy
Level
72.73
61.50
11
Level 2
35.71
40.18
28
Level 3
30.36
26.88
56
Level 4
14.89
16.61
94
Level
6.08
6.39
181
Table 7: LLEMMA-34b's accuracy on hits (a 30-gram overlap between a problem or solution and a training sequence) and non- hits by MATH difficulty level.
8

---

Published as a conference paper at ICLR 2024
Finally, we check 30-gram hits between LLEMMA'S MATH generations and Open WebMath. There were 13 hits, which occurred when the model generated a common sequence of numbers (c.g., a list of Fibonacci numbers), plus one instance of factoring polynomial. Appendix Figure 6 6/oows an example. We find all of these observations worthy of further study. Using LLEMMA and Proof-Pile-2 to better understand data, memorization, and performance is 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., 22020
Chowdhery et al. 2022). and a progression toward more generalist models (Radford et al. 2019
Brown 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 al., 2023 Rozière al. (023). 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 general -omaann pretraining step, followed by a shorter fin-ttnnin step. The finetuning step often aimed at imbuing instruction- following ability (Sanh et al., 2022, Wei et al. 2022) or aligning a model's 's outputs with human
preferences (Ziegler et [dl][2019) Ouyang et al. 2022 Bai et al. 2022). Other work explores adapting pretrained models to novel domains by continued training (Roziere 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 Icarning. including benchmarking mathematical knowledge and reasoning varying levels (Hendryeks al. 202 Zheng al. 2021; Welleck al. 2022
Azerbayev et al. 2023). Although achieving strong mathematical reasoning is an important target, it difficult 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 (c.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, [Lekkowcz
ct al. (222) and our work seek to train 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.) [022]] Lample et al.) [022] Jiang et al. (2022), autoformalization (Wu et al. 2022, Jiang et al. 2003). 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 autofor- malization and tactic prediction, a large collection of formal mathematics data, along with open access model for further exploring these directions.
CONCLUSION
We introduce LLEMMA and Proof-Pile-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-as results for open-weights models on mathematical problem solving bench- marks, shown capabilities of using external tools via Python code, and demonstrated few-shot tactic prediction for theorem proving. We hope that LLEMMA and Proof-Pile-2 will be a useful base for future work understanding language model generalization and dataset composition, investigating the limits of nomain-specific language models, using language models as tools for mathematicians, and improving the mathematical capabilities of language models.
9

---

Published as a conference paper at ICLR 2024
ACKNOWLED
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 open-source code.
We would also like to thank several parties for donating computing resources for this project: Stability AT (training the LLEMMA models), CoreWeave (evaluations and finetuning), the Province of Ontario and companies sponsoring the Vector Institute for Artificial Intelligence (www. www.orintiiiseim iritoorinnttttt ai/partners). and Brigham Young University (linetuning). KP is supported by an NSERC PGS-D award.
REFERENCES
Loubna Ben Allal, Raymond Li, Denis Kocetkov, Chenghao Mou, Christopher Akiki, Carlos Munoz Ferrandis, Niklas Muennighoff, Mayank Mishra, Alex Gu, Manan Dey, Logesh Kumar Umapathi, Carolyn Jane Anderson, Yangtian Zi, Joel Lamy Poirier, Hailey Schoelkopf, Sergey Troshin, Dmitry Abulkhanov, Manuel Romero, Michael Lappert, Francesco De Toni, Bernardo Garefa del Río, Qian Liu, Shamik Bose, Urvashi Bhattacharyya, Terry Yue Zhuo, Ian Yu, Paulo Villegas, Marco Zocca, Sourab Mangrulkar, David Lansky, Huu Nguyen, Danish Contractor, Luis Villa, Jia Li, Dzmitry Bahdanau, Yacine Jernite, Sean Hughes, Daniel Fried, Arjun Guha, Harm de Vries, and Leandro von Werra. Santacoder: don't 't reach for the stars! In Deep Learning for Code (DL4C) Workshop, 2023. 2023.
Alex Andonian, Quentin Anthony, Stella Biderman, Sid Black, Preetham Gali, Leo Gao, Eric Hallahan, Josh Levy-Krame'' Connor Leahy, Lucas Nestler, Kip Parker, Michael Pieler, Jason Phang. Shivanshu Purohit, Hailey Schoelkopf, Dashiell Stander, Tri Songz, Curt Tigges, Benjamin Thérien, Phil Wang, and Samuel Weinbach. GPT-NeoX: Large scale autoregressive language mod- cling in PyTorch. GitHub Repo, 9 2023. URL https: http:::/wwwwwttttttee github. com/ woom/eeeutee eleutherai gpt-neex
Akari Asai, Sewon Min, Zexuan Zhong, and Danqi Chen. Retrieval- based language models and applications. In Proceedings of the ōlst Annual Meeting of the Association for Computational
Linguistics (Volume 6: Tutorial Abstracts), pp. 41-46, Toronto, Canada, July 2023. Associ- ation for Computational Linguistics. doi: 10. http:///////222..ttttrrrrro
URL https
7/aclantho ogy. ogy.org/2023 acl tuttoitttrrall...
Jeremy Avigad. The mechanization of mathematics. Notices of the AMS, 65(6):681-90 2018.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir R. Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leve mathe- matics. ArXiv, abs/2302. 12433, 2023.
Yuntao Bai, Andy Jones, Kamal Ndousse, Amanda Askell, Anna Chen, Nova DasSarma, Dawn Drain, Stanislav Fort, Deep Ganguli, Tom Henighan, Nicholas Joseph, Saurav Kadavath, Jackson Kernion, Tom Conerly, Sheer El-Showk, Nelson Elhage, Zac Hatfield-Dodds, Danny Hernandez, Tristan Hume, Scott Johnston, Shauna Kravec, Liane Lovitt, Neel Nanda, Catherine Olsson, Dario Amodei, Tom Brown, Jack Clark, Sam McCandlish, Chris Olah, Ben Mann, and Jared Kaplan. Training a helpful and harmless assistant with reinforcement learning from human feedback. arXiv preprint arxiv:2204. 05862, 2022.
Iz Beltagy. Kyle Lo, and Arman Cohan. SciBERT: A pretrained language model for scientific text. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNNP)-JCNN.P), pp. 3615-3620. Hong Kong, China, November 2019. Association for Computational Linguistics. doi: 10.18653/v1/DIP
URL
1371
Stella Biderman, Hailey Schoelkopf, Quentin Gregory Anthony, Herbie Bradley, Kyle O' O'Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, USVSN Sai Prashanth, Edward Raff, et al. Pythia: A suite for analyzing large language models across training and scaling. In International Conference Machine Learning, pp. 2397-2430. PMLR, 2023.
10

---

Published as a conference paper at ICLR 2024
Stella Rose Biderman, Kieran Bicheno, and Leo Gao. Datasheet for the pile. ArXiv, abs/2201.07311, 2022.
Sidney Black, Stella Biderman, Eric Hallahan, Quentin Anthony, Leo Gao, Laurence Golding, Horace He, Connor Leahy, Kyle McDonell, Jason Phang, et al. Gpt-neox-20b. An open-source autoregressive language model. In Proceedings of BigScience Episode# 5-Workshop on Challenges & Perspectives in Creating Large Language Models, pp. 95-136, 2022.
Samuel Bowman, Jeeyoon Hyun, Ethan Perez, Edwin Chen, Craig Petti, Scott Heiner, Kamilé Lukošiūté, Amanda Askell, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, Christopher Olah, Daniela Amodei, Dario Amodei, Dawn Drain, Dustin Li, Eli Tran- Johnson, Jackson Kernion, Jamie Kerr, Jared Mueller, Jeffrey Ladish, Joshua Landau, Kamal Ndousse, Liane Lovitt, Nelson Elhage, Nicholas Schiefer, Nicholas Joseph, Noemí Mercado, Nova DasSarma, Robin Larson, Sam McCandlish, Sandipan Kundu, Scott Johnston, Shauna Kravec, Sheer Showk, Stanislav Fort, Timothy Telleen-Lawton Tom Brown, Tom Henighan, Tristan Hume, Yuntao Bai, Zac Hatfield-Dodde Ben Mann, and Jared Kaplan. Mcasuring progress scalable oversight for large language models. arXiv preprint 2rXiv:2211.03542 2022.
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, T. J. Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeff Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, llya Sutskever, and Dario Amodei. Language models are few-shot learners. ArXiv, abs/2005. 14165, 2020.
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung. Charles Sutton, Sebastian Gehrmann, et al. Palm: Scaling language modeling with pathways. arXiv preprint orXiv:2204.02311, 2022.
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv:21 10. 14168, 2021.
Katherine M. Collins, Albert Q Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B. Tenenbaum, William Hart, Timothy Gowers, Wenda Li, Adrian Weller, and Mateja Jamnik. Evaluating language models for mathematics through interactions. arXiv preprint 2rXiv:2306.01692 2023.
Together Computer. Redpajama: An open source recipe to reproduce llama training dataset, April 2023. URL.tttp:://gt thub. www.//////oooeeeeee teon/ttgtheerree htapeehherccooptte/eeeeeee
-Dama
Tri Dao. Flashattention-2: Faster attention with better parallelism and work partitioning. arXiv
preprint arXiv:2307.08691, 2023.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doomn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Aedduction-CADE-.. 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
Erich Elsen, Curtis Hawthome, and Arushi Somani. The adventure of the errant hardware, 2023.
URL httpttt/w//wwww... adept. a http/bloogshherlclcoe
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole proof generation and repair with large language models. arXiv preprint arXiv:2303.049100 2023.
Leo Gao, Stella Rose Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace Hc, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The pile: An 800gb dataset of diverse text for language modeling. ArXiv, abs/2101.00027. 2020.
Leo Gao, Jonathan Tow, Baber Abbasi, Stella Biderman, Sid Black, Anthony DiPofi, Charles Foster, Laurence Golding, Jeffrey Hsu, Alain Le Noac h, Haonan Li, Kyle McDonell, Niklas Muennighoff, Jason Ociepa, Chris Phang, Laria Reynolds, Hailey Schoelkopf, Aviya Skowron, Lintang Sutawika,
11

---

Published as a conference paper at ICLR 2024
Eric Tang, Anish Thite, Ben Wang. Kevin Wang. and Andy Zou. A framework for few-shot language model evaluation, September 2021. /tt.:p:://al..oo11115522222 5tt.:////..5222//eoooo00 5371628
Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided language models. arXiv preprint arXiv:2211.0443 2022.
Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided language models. arXiv preprint arXiv:2211.10433 2023.
Timmit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna Wallach, Hal Daumé III au2, and Kate Crawford. Datasheets for datasets, 2021.
Herbert L. Gelemntrr, Realization of a geometry theorem proving machine. In IFIP Congress, 1959. URL https://app. wew.ariccchooaarrr.ooooo wwwpechhoaaa..r/oooooooooo. :t:.:puusS.:11444999 18484295
Priya Goyal, Piotr Dollár, Ross B. Girshick, Pieter Noordhuis, Lukasz Wesolowski, Aapo Kyrola, Andrew Tulloch, Yangqing Jia, and Kaiming He, Accurate, large minibatch SGD: training imagenet in hour. CoRR, abs/l 726.0777.. 2017.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co- training for theorem proving with language models. In International Conference on Learning Representations, 2022. URL
Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. Measuring massive multitask language understanding. arXiv preprint arXiv:2009.03300. 2021a.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. NeurIPS. 2021b.
Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai. Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, Erich Elsen, Jack W. Rae, Oriol Vinyals, and Sifre. Training compute-optimal large language models. arXiv preprint 2rXiv:2203.1555: 2022.
Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The curious case of neural text degeneration, 2020.
Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021.
Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóćds, Piotr Mitos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint arXiv:2205. 10893, 2022.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023. URL
net. www.:oorrmmmdsmmm 9EAOVKMC
Jared Kaplan, Sam McCandlish, T. J. Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeff Wu, and Dario Amodei. Scaling laws for neural language models. arXiv preprint arXiv:2001.08300 2020.
Denis Kocetkov, Raymond Li, Loubna Ben Allal, Jía Li, Chenghao Mou, Carlos Muñoz Ferrandis, Yacine Jernite, Margaret Mitchell, Sean Hughes, Thomas Wolf, Dzmitry Bahdanau, Leandro von Werra, and Harm de Vries. The stack: tb of permissively licensed source code. Preprint, 2022.
Guillaume Lample, Marie-Ane Lachaux. Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. arXiv preprint arXiv:2205./ /141, 2022.
12

---

Published as a conference paper at ICLR 2024
Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022.
Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. arXiv preprini 2tti::3305.20050. 2023.
Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. 14605-14631, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10. 1/253////222...cloooog https: http:///aaaattoaoooooo/r///aaaaa acl-long...........
URL
org.
Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. Wizardmath: Empowering mathematical reasoning for large language models via reinforced evol-instruct. arXiv preprint "XXv:2308.09583 2023.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 97814503709744 doi: 10. 10.1/ 3372885.3373824 URL htt.thtts///...... ottp:/...rg11... 11t...1111/3388880 3373824
Sewon Min, Suchin Gururangan, Eric Wallace, Hannanch Hajishirzi, Noah A. Smith, and Luke Zettlemoyer. Silo language models: Isolating legal risk in nonparametric datastore, 2023.
Scott Morrison.
lean-training-data.
trannirainigg-datt. 2023.
OpenAl. Gpt-4 technical report, 2023.
Long Ouyang, Jeff Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul Christiano, Jan Leike, and Ryan Lowe. Training language models to follow instructions with human feedback. arXiv preprint arXiv:2203.02155. 2022.
Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba. Openwebmath: An open dataset of high-quality mathematical web text. CoRR, abs/2310.06786 2023, doi: 10.48550/ ARXIV.2310.06786 TRLptttp:://da
wwwpg............./.ooo// 48550/ arxiv wtw.eiii.....11.. 2310. 0677
Christine Paulin Mohhing Extracting w's programs from proofs in the calculus of constructions. In Proceedings of the 16th ACM SIGPLAN-SIGACE symposium Principles of programming languages, pp. 89-104, 1989a.
Christine Paulin-Mohring. Extraction de progranmes dans le Calcul des Constructions. PhD thesis, Université Diiis-Dideoot-Pariss VII, 1989b
Larry Paulson and Tobias Nipkow. The sledgehammer: Let automatic theorem provers write your isabelle scripts!, 2023. URL httis::/ in. tum. /e htt/sslddghaamme.r... .html
Bowen Peng, Jeffrey Quesnelle, Honglu Fan, and Enrico Shippole. Yam: Efficient context window extension of large language models. arXiv preprint (txxi:2309.0007/, 2023.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and llya
Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344 2022.
13

---

Published as a conference paper at ICLR 2024
Alec Radford, Jeff Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAl Blog, 2019.
Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. Exploring the limits of transfer learning with a unified text-to-text transformer, 2023.
Samyam Rajbhandari, Jeff Rasley, Olatunji Ruwase, and Yuxiong He. ZeRO: Memory optimizations toward training trillion parameter models. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC '20. IEEE Press, 2020. ISBN URL https::/ acm. org/ htrg//oi//t /10
01817281999888 doi: (..555/3433701.3433777777 5555/343317 3433727
Baptiste Rozière, Jonas Gehring. Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, Artyom Kozhevnikov, Ivan Evtimov, Joanna Bitton, Manish Bhatt, Cristian Canton Ferrer, Aaron Grattafiori, Wenhan Xiong, Alexandre Défossez, Jade Copet, Faisal Azhar, Hugo Touvron, Louis Martin, Nicolas Usumier, Thomas Scialom, and Gabriel Synnaeve. Code Ilama: Open foundation models for code. arXiv preprint arXiv:2308. 12950, 2023.
Victor Sanh, Albert Webson, Colin Raffel, Stephen H. Bach, Lintang Sutawika, Zaid Alyafeai, Antoine Chaffin, Arnaud Stiegler, Teven Scao, Arun Raja, Manan Dey, M Saiful Bari, Canwen Xu, Urmish Thakker, Shanya Sharma Sharma, Eliza Szezechla, Taewoon Kim, Gunjan Chhablani, Nihal Nayak, Debajyoti Datta, Jonathan Chang, Mike Tian-Jian Jiang, Han Wang, Matteo Manica, Sheng Shen, Zheng Xin Yong. Harshit Pandey, Rachel Bawden, Thomas Wang. Trishala Neeraj, Jos Rozen, Abheesht Sharma, Andrea Santilli, Thibault Fevry, Jason Alan Fries, Ryan Teehan, Tali Bers, Stella Biderman, Leo Gao, Thomas Wolf, and Alexander M. Rush. Multitask prompted training enables zero-shot task generalization. arXiv preprint urXiv:2110.08200) 2022.
Mohammad Shoeybi, Mostofa Patwary, Raul Puri, Patrick LeGresley, Jared Casper, and Bryan Catanzaro. Megatron-LM: Training multi-billion parameter language models using model par- allelism. Computing Research Repository, 2019. doi: 10.48550/rxxi..1990.o 1909.0853. URL
htttps://axiv.. org. abs/ 1909. 08053v4 Version 4.
Karan Singhal, Shekoofeh Azizi, Tao Tu, S. Sara Mahdavi, Jason Wei, Hyung Won Chung, Nathan Scales, Ajay Tanwani, Heather Cole-Lewis, Stephen Pfohl, Perry Payne. Martin Seneviratne, Paul Gamble, Chris Kelly, Nathaneal Scharli, Aakanksha Chowdhery. Philip Mansfield, Blaise Aguera y Arcas, Dale Webster, Greg S. Corrado, Yossi Matias, Katherine Chou, Juraj Gottweis, Nenad Tomasev, Yun Liu, Alvin Rajkomar, Joelle Barral, Christopher Semturs, Alan Karthikesalingam, and Vivek Natarajan. Large language models encode clinical knowledge, 2022.
Karan Singhal, Tao Tu, Juraj Gottweis, Rory Sayres, Ellery Wulczyn, Le Hou, Kevin Clark, Stephen Pfohl, Heather Cole-Lewis, Darlene Neal, Mike Schaekermano, Amy Wang. Mohamed Amin, Sami Lachgar, Philip Mansfield, Sushant Prakash, Bradley Green, Ewa Dominowska, Blaise Aguera y Arcas, Nenad Tomasev, Yun Liu, Renee Wong, Christopher Semturs, S. Sara Mahdavi, Joelle Barral, Dale Webster, Greg S. Corrado, Yossi Matias, Shekoofch Azizi, Alan Karthikesalingam, and Vivek Natarajan. Towards expert-level medical question answering with large language models, 2023.
Jianlin Su, Yu Lu, Shengfeng Pan, Ahmed Murtadha, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. arXiv preprint (x.iv:2004009860 2022.
Ross Taylor, Marcin Kardas, Guillem Cucurull, Thomas Scialom, Anthony Hartshorn, Elvis Saravia, Andrew Poulton, Viktor Kerkez, and Robert Stojnic. Galactica: A large language model for science, 2022.
Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language- agent approach to formal prrovin. 2023.
Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng- Reng-Tze Cheng, Alicia Jin, Taylor Bos. Leslie Baker, Yu Du, YaGuang Li, Hongrae Lee, Huaixiu Steven Zheng, Amin Ghafouri, Marcelo Menegali, Yanping Huang, Maxim Krikun, Dmitry Lepikhin, James Qin, Dehao Chen, Yuanzhong Xu, Zhifeng Chen, Adam Roberts, Maarten Bosma, Vincent
14

---

Published as a conference paper at ICLR 2024
Zhao, Yanqi Zhou, Chung-Ching Chang, Igor Krivokon, Will Rusch, Mare Pickett, Pranesh Srinivasan, Laichee Man, Kathleen Meier-Hellstern Meredith Ringel Morris, Tulsee Doshi, Renelito Delos Santos, Toju Duke, Johnny Soraker, Ben Zevenbergen, Vinodkumar Prabhakaran, Mark Diaz, Ben Hutchinson, Kristen Olson, Alejandra Molina, Erin Hoffman-John, Josh Lee, Lora Aroyo, Ravi Rajakumar, Alena Butryna, Matthew Lamm, Viktoriya Kuzmina, Joe Fenton, Aaron Cohen, Rachel Bernstein, Ray Kurzweil, Blaise Aguera-Arcas, Claire Cui, Marian Croak, Ed Chi, and Quoc Le. Lamda: Language models for dialog applications. arXiv preprint ar arXiv:2201.000 0822999 2022.
Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cris- tian Canton Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami, Naman Goyal, Anthony Hartshorn. Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Marie-Anne Lachaux, Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog, Yixin Nie, Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiaoqing Ellen Tan, Binh Tang, Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, Iliyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aurelien Rodriguez, Robert Stojnic, Sergey Edunov, and Thomas Scialom. Llama 2: Open foundation and fine-tunet chat models. arXiv preprint arXiv:2307.00 092888, 2023.
Jonathan Uesato, Nate Kushman, Ramana Kumar, Francis Song, Noah Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. Solving math word problems with process- and outcome-based feedback, 2022.
H. Wang. Toward mechanical mathematics. IBM Journal of Research and Development, 4(1):2-22, 1960. doi: 1.1114///..4.000
Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, 2023. URL fictps://opereest ew net wowt:/oorummldd
Jason Wei, Maarten Bosma, Vincent Y. Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M. Dai, and Quoe V. Le. Finetuned language models are zero-shot learners. arXiv preprint arXiv:2109.01552, 2022.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc Le, and Denny Zhou. Chain-of-thougee prompting elicits reasoning in large language models, 2023.
Sean Welleck. Neural theorem proving tutorial. ntptutorial 2023.
Sean Welleck and Rahul Saha. Ilmstep: Llm proofstep suggestions in lean. attps://github com well lecks/ moocks/llmsseese mssee 2023.
Sean Welleck, Jiacheng I Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (. in Neural Information Processing Systems, 2022. URLLAttps:/opeeevvieee net/ wttp://eee/oomomeeeeeeeeeee
Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow. The isabelle framework. In Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21, pp. 33-38. Springer, 2008
Shijie Wa, Ozan Irsoy, Steven Lu, Vadim Dabravolski, Mark Dredze, Sebastian Gehrmann, Prabhan- jan Kambadur, David Rosenberg, and Gideon Mann. Bloomberggpt: A large language model for finance, 2023.
15

---

Published as a conference paper at ICLR 2024
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL http:::::: /ownr//veeeeeveveeeeeeee net forrff d= d= TJikebJl BfO
Sang Michael Xie, Hieu Pham, Xuanyi Dong, Nan Du, Hanxiao Liu, Yifeng Lu, Percy Liang, Quoc V. Le. Tengyu Ma, and Adams Wei Yu. Doremi: Optimizing data mixtures speeds up language model pretraining, arXiv preprint arXiv:2305.10422 2023.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023.
Zheng Xin Yong, Hailey Schoelkopf, Niklas Muennighoff, Alham Fikri Aji, David Ifeoluwa Adelani, Khalid Almubarak, M Saiful Bari, Lintang Sutawika, Jungo Kasai, Ahmed Baruwa, Genta Winata, Stella Biderman, Edward Raff, Dragomir Radev, and Vassilina Nikoulina. BLOOM+1: Adding language support to BLOOM for zero-shot prompting. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume Long Papers), pp. 11682-11703, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10. 186116611/2222.. acl-long.653. URL htttt::t//////. //ac a anthology wwsgy.org/22333 acl acl-iong 653
Longhui Yu, Weisen Jiang. Han Shi. Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309. 12284, 2023.
Xiang Yue, Xingwei Qu, Ge Zhang, Yao Fu, Wenhao Huang, Huan Sun, Yu Su, and Wenhu Chen. Mammoth: Building math generalist models through hybrid instruction tuning. CoRR. abs/2309.05653,, 2023. doi: 10.48550/a2Xiv2230.00666 48550/arXiv. 2309. 2309.05653
URL
Shizhuo Dylan Zhang, Curt Tigges, Stella Biderman, Maxim Raginsky, and Talia Ringer. Can transformers learn to solve problems recursively?, 2023.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: cross system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.001 10, 2021.
Hattie Zhou, Azade Nova, Hugo Larochelle, Aaron Courville, Behnam Neyshabur, and Hanie Sedghi. Teaching algorithmic reasoning via in-context learning, 2022.
Daniel Ziegler, Nisan Stiennon, Jeffrey Wu, Tom Brown, Alec Radford, Dario Amodei, Paul Christiano, and Geoffrey Irving. Fine-tuning language models from human preferences. arXiv preprint arXiv: 08593, 2019.
16

---

Published as a conference paper at ICLR 2024
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.
Formal math evaluations. Sean Welleck.
Memorization analysis. Sean Welleck, Keiran Paster.
Senior Authorship and Advising, Jia Deng, Stella Biderman, Sean Welleck.
B DATA: Proof-Pile-2
Data source
Tokens
Weight
Proof-Pile-2
55B
Code (AlgebraicStack)
11B
1.00
Web (OpenWebMathh)
15B
4.00
Papers (ArXiv)
29B
2.00
General code (RedPajama)
59B
0.22
General language (Pile)
300B
0.15
Table 8: Proof-Pile-2 data sources (top), general language and code data included during training (bottom), and the mixture weights each component during training.
B. MATHEMATTCCA CODE: AlgebraicStack
AlgebraicStack contains roughly 11B tokens of code related to mathematics. We describe its sources, filtering, and content below. Table shows number of tokens per language in AlgebraicStack.
Language
AlgebraicStack tokens
Language
AlgebraicStack tokens
Agda
35.2 M
Julia
531.0 M
C
25.1 M
Jupyter
199.1 M
C++
954.1 M
Lean
285.6 M
Coq
281.9 M
Maple
2.0 M
Fortran
724.9
Matlab
65.8
GAP
3.6 M
Python
6,098.8 8 M
Haskell
9.1
R
71.3
Idris
10.9 M
Tex
567.7 M
Isabelle
1,089.7 M
Total
10,955.7 M
Table 9: Tokens in AlgebraicStack, computed with the Llama tokenizer.
B.1.1
GITHUB CODE
The following programming languages either barely present in the Stack 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 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.
17

---

Published as a conference paper at ICLR 2024
Isabelle We filter for files with the -thy extension and include files matching the keyword whitelist "theorem " "lemma Seabeele-prrove//mirrro
We keep only 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.
202T test set.
Lean We filter for files with the lean extension, using the keyword whitelist "theorem "lemma "example" " We remove all dependency files, and order avoid known benchmark contamination, we blacklist the Proofii fNet. and Mi niFFF 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 extension, using the keyword whitelist "#import", "interface", "implementation". "property", and blacklist C files via the keywords "#include" and the regex r' main) (. (5*
implemented a cutoff date for our Github API downloads, and used a cutoff date of April I, 2023.
For all languages, unless otherwise stated, we additionally filtered out files with 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-tra ratttaiinn baan-training-dee iiing-data (Morrison 2023 tool. We use Mathlib 4 commit c77 9bd5, which was created on August 20th 2023.
B.1.3 ISABELLE PROOFSTEPS
We construct dataset of Isabelle proofs, building upon the PISA dataset Diang al. (2021) Isabelle Proofsteps comprises proofs from the Archive of Formal Proofs and Isabelle Standard Library, scraped with PISA Jiang et al. (02T). 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 2510000 theorems.
B.1.4 STACK FILTERING
We source the following programming languages from the Stack (Kocetkov et al. 2022) dataset, and describe filtering process and quality issues chose mitigate beyond our default quality heuristics:
Agda: Only standard filters applied.
C: We include documents based on keyword whitelist, namely: "#include <fftwwh>". "#include <fftw3.h>". "#include <rfftw.h>", "#include <gsl", "#include <cblas.h>", "#include <blas.h>", "#include <lapacke.h>", "#include <nlopt.h>", "#include <petsc.h>".
C++ We include documents based on a keyword whitelist, namely: "Hinclude aadept_arrays.he "#include <adept.h>". "#include <alglib>, "#include <boost". "#include sarmadillo", "#include <blitz", "#include <Eigen", "#include <deal.1I". "#include <dlib", "#include <NTL", "#include <mtl".
Fortran Only standard filters applied.
GAP : Only standard filters applied.
Haskell We filtered the data to only contain files with the following im- ports: LunerricLinearrAggbrrr, Stumeric.SpecFunctii Numeric, Vector, Statistics, Data. Complex
18

---

Published as a conference paper at ICLR 2024
Idris: Only standard filters applied.
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 control relevance to scientific comput- ing, namely: "LinearAlgebra". "Difterentiallquatton"" "Symbolies". "Distributions", "DataFrames". " "DynamicalSystems" "Turing". "Gen", "JuMP", "sqrt". "abs", "ze- ros", "ones", "sin", "cos", "tan", "log", "exp", "integrate". "likelihood", "Matrix". T, "pi", "rand", "grad".
Julia
Jupyter
We found that many Jupyter notebook files were large due to containing long cell outputs, such as basc64 images, long tracebacks, or other extra JSON cell metadata. We use abconvert to convert notebooks to a markdown format, removing metadata.
Maple We filtered out files with 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 fixed list of libraries.
. R: We excluded all files beginning with 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 di- rectories named "latex/" because these were often auto auto-generated files, and excluded documents using gnuplot. We included only documents containing one of the keywords chapter(". " ""chapter*(". "" "),section[". "'/section*(" "/subsection(", "(subsecttoo"(" "subsubsectionn" " "subsubsection*("" " paragraph(" " "suupaaagrrphh" and ad- ditionally only included documents identified as English by a classifier from the langio package
For all languages we used within the Stack, unless otherwise stated, we additionally filtered out files with filesize greater than 1048575 bytes with numerical density (ratio of digit characters to non-digit characters) of 0.5.
We used v1.2 of the near-deduplicated Stack as 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 ArXiv, see Computer (2023).
B.3 WEB: OPENWERMATH
For the web portion of our training dataset, use OpenWebMath (Paster al. 2023
C EVALUATION HARNESS
We implement variety of math-related tasks and evaluation protocols into a public fork of the Language Model Evaluation Harness (Gao et al. (02T). The Harness provides model-agnostic framework for standardized, reproducible evaluation of language models.
We add the following tasks for the evaluations in this paper:
Lendrycks_mattee satis__mathpppp...p Perplexity evaluation MATH (Hendryeks et al. 2021a sub-tasks.
minif2f _er2f__sabbblll issabellee le: Proof autoformalization in Isabelle on the miniF2F benchmark based on Jiang et al. (2023), with Portal-to-Isabelle (Jiang et al. 2021 proof checker.
minerva__atee The MATH benchmark with the prompt and Sympy evaluation from Minerva (Lewkowycz et al. 2022).
mi merra--hendrycckeTest: MMLU-STEM tasks following Lewkowycz et al. 2022
19

---

Published as a conference paper at ICLR 2024
ocw_courses: The OCW Courses task from Lewkowyez et al. (2022
python_gsmäk, GSM8k with Python, based on Gao et al. (2022).
sympy_math: MATH with Sympy evaluation.
include a link to the implementations for these tasks, including full prompts, in our public codebase.
D EVALUATION: EXPERIMENT DETAILS
D.1 ISABELLE INFORMAL-TO-FORMAL THEOREM PROVING
We follow Jiang et al. 2023). allowing the model to issue a call to built-in Isabelle automation the output proof by generating edgehammer: This calls Sledgehammer (Paulson & Nipkow 2023) and the list of heuristics listed in Jiang et al. (023). Following Jiang et al. (2023), as a baseline we use Sledgehammer and the heuristics executed at the beginning of the proof (referred to Sledgehammer in the main text for brevity). We use a 30-second timeout for Sledgchammer and implement proof checking via Portal-to-Isabell (Jiang al. 2021). Refer the implementation in the Evaluation Hamess for further details.
D.2 LEAN THEOREM PROVING
Theorem proving via tactic prediction involves interacting with a proof assistant after each step of proof. Implementing these interactions within the evaluation harness is outside the scope of this work. Therefore, for the Lean theorem proving task we use separate evaluation setup based on an open-source implementation (Welleck 2023). We include our evaluation code in our public codebase.
Setup. We evaluate on miniF2F (Zheng et al. 2021), which consists of 488 formalized statements from math competitions and undergraduate coursework. Given formalized statement, the task is to generate a formal proof that is checked by Lean.
We best first search, commonly used for neural tactic prediction models le.g...Pllu & Sutskever (2020)). Best first search is parameterized by the number of attempts (N), generated tacties per iteration (S), and maximum iterations (T). We define the search budget number of generated tactics, N S T. We our search budget to N 1, S 32, and = 100, less than that the baseline model. Following Yang et al. (2023), we gener- ate tactics with beam search and use 10 minute timcout. We adapt the proof search imple- mentation from Welleck (202)), , which uses LeanDojo v.1.1.2 (Yang et al. 2023) for interac- tion. We Lean 4 mini F2F, using https:://ittult www. hamm/rah49211 2etr//ean--ae -olan-do-ppp jojo mew commit (00c77226c777 7e f 9de6c0fflde Note that the ReProver baseline from YYang al. 2023) reports performance with Lean 3.
the maximum
Prompt. We prompt the model with three (state, tactic) examples, shown in Figure
20

---

Published as a conference paper at ICLR 2024
"""Given the Lean 4 tactic state, suggest next tactic. Here are some examples:
Tactic state:
a : Type u_1 + Propt inst' DecidableEg at inst IsIrrefl CutExpand S InvImage (Finsupp. Lex ( II fun xx1 + x_1) x_1) ftoFinsupp
fun x x_
Next tactic:
rintro t (u, a, hr, he)
Tactic state:
6: Type u_lt
I Box
4 R
I J WithBot (Bex
fJ +
Next tactic:
simp only . intisymm iff, Le_antisymm withhotcco_subset___
Tactic state:
m n
h : Nat.cop cat.coprime m Nat Nat.ged m n =
Next tactic:
rw It h. w_gcd__e__cp_
Tactic state:
$8
Next tactic:
man
Figure 5: Prompt for the Lean theorem proving experiments.
21

---

Published as a conference paper at ICLR 2024
E DATASHEET
We provide a datasheet for Proof-Pile-2, following the framework Gebru et al. (2021)
MOTIVATION
For what purpose was the dataset cre- ated?
Proof-Pile-2 created for the training or finetuning domain-specific large lan- guage models for general mathematics tasks.
Who created the dataset and on behalf of which entity?
The dataset was created by the authors of this paper for the purposes of this research project.
Who funded the ereation of the dataset?
The creation of the dataset was funded by the coauthors' grants and employers, as fur- ther described inssecion
Any other comment?
COMPOSITION
What do the instances that comprise the dataset represent?
Instances are text-only documents.
How many instances are there in total?
We detail fine-grained token counts else- where in this paper.
Does the dataset contain all possible in- stances or is it sample (not necessarily random) of instances from a larger set?
Our dataset is filtered based on our assess- ments of quality for the language modeling task. More detail on methodology can be found in Appendixx
What data does each instance consist of?
Each instance a text-only document, alongside metadata about its originating split and filename or location.
Is there label or target associated with each instance?
No.
Is any information missing from individ- ual instances?
Yes, we filter undesired noise, such as base64-encoded images, from some doc- uments.
Are relationships between individual in- stances made explicit?
No.
Are there recommended data splits?
Yes, we release a canonical train, validation, and test split of the dataset, which we follow in this work.
Are there errors, sources of noise, or redundancies in the dataset?
We make our best efforts to remove errors or sources of noise, but our dataset will naturally contain documents with errors or noise, and may contain near-duplicate doc- uments.
Is the dataset self-contained, does it link to or otherwise rely on external re- sources?
The dataset self-contained, but can also be reconstructed based on external publicly available data sources and datasets follow- ing our instructions.
Does the dataset contain data that might be considered confidential?
All documents in Proof-Pile-2 are publicly available online.
22

---

Published as a conference paper at ICLR 2024
Does the dataset contain data that, if viewed directly, might be offensive, in- sulting, threatening, might otherwise cause anxiety?
We estimate toxic content to be less preva- lent in our dataset than other more general web-based datasets, due to its technical fo- cus. However, is likely to contain such content.
COLLECTION
How was the data associated with each instance acquired?
Data was largely sourced from existing pub- lic subsets, such the RedPajama dataset (Computer, 2023). Open WebMath dataset
(Paster 2023 , and via filtering the Stack (Kocetkov et al. 2022). Some data was collected using the Github API.
What mechanisms or procedures were used to collect the data?
See above.
If the dataset is a sample from a larger set, what was the sampling strategy?
We release the entirety of the dataset fol- lowing the application of our quality filters. We randomly held out validation and test splits from the dataset.
Who involved in the data collec- tion process and how were they compen- sated?
The authors of this paper participated in lo- cating, retrieving, and filtering the dataset.
Over what timeframe was the data col- lected?
This data was collected in 2023, with cut- off date of April 2023 for all subsets with the exception of our Lean proofstep data.
Were any ethical review processes con- ducted?
Yes, the authors conducted an informal eth- ical review internally.
PREPROCESSING
Was any prepoeessingcclanigglaelllngg of the data done?
Yes, the authors extensively filtered the dataset subsets in keeping with our expec- tations for high-quality language modeling data in our domain. See [Appendix for further detail on filtering steps taken.
Was the "raw" data saved in addition to data?
Raw data can be accessed via reuse of provided codebase.
the preprocesed/cceened//bbe
Is the software that was used to prepro- cess/clean/label the data available?
Yes. We release our codebase, which can be used to reproduce our dataset and its con- struction process, at https: ptnttps:/gge /tt:://gtiii huu com/ELeutherAA/ maath-aahh--h 1m
USES
Has the dataset been used for any tasks already?
Yes, this dataset has been used to train the LLEMMA language models as domain
adaptation and continued pretraining cor- pus.
Is there repository that links to any or all papers or systems that use the dataset?
No.
What (other) tasks could the dataset be used for?
The dataset specifically targeted high quality language modeling corpus for the mathematics domain, but may be useful for general-purpose language modeling or unforeseen other downstream uses.
23

---

Published as a conference paper at ICLR 2024
Is there anything about the composition of the dataset or the way was col- lected and prepovesse//leeeecllbbeeed that might impact future uses?
We filtered the dataset with the intent of creating a model useful for mathematical tasks with solely English text.
Are there tasks for which the dataset should not be used?
The dataset should not be used with the intent cause harm or for models intended for the purposes of harm.
DISTRIBUTION
Will the dataset be distributed to third parties outside of the entity on behalf of which the dataset was created?
We make the dataset publicly available for reproducibility, analysis, and other further downstream uses.
How will the dataset will be distributed?
We provide code to replicate the dataset, and release via the Huggingface Hub.
When will the dataset be distributed?
The dataset is available immediately.
Will the dataset be distributed under copyright other intellectual prop- erty (IP) license, and/or under applicable terms of use (ToU)?
We do not relicense the dataset's 's compo- nents, and do impose our own use re- strictions.
Have any third parties imposed IP-based or other restrictions the data associ- ated with the instances?
Not to our knowledge.
Do any export controls or other regula- tory restrictions apply to the dataset or to individual instances?
Not to our knowledge.
MAINTENANCE
Who will be supporiing/nuttig/maann taining the dataset?
The dataset will be hosted on the Hug- gingFace Hub and able to be recreated via code at https::/ /ttp://gitttuu.ut thub. com/ EleutherAf/math- 1m The dataset will not be updated post-relcase.
How can the owner/curatorr/manage of the dataset be contacted?
Via email at 2a2514 aaaa511@rrinceton.edd
there an erratum?
No.
Will the dataset be updated?
No.
If others want to extend/augmnen/buiid on/contribute to the dataset, is there
No.
mechanism for them to do so?
Table 10: Datasheet for Proof-Pile-2, following the framework introduced by Gebru et al. 2021
24

---

Published as a conference paper at ICLR 2024
F
ADDITIONAL RESULTS
F.1
PROOF AUTOFORMALIZAATOO
Table
shows additional results on Isabelle proof autoformalization, including the union of theorems closed by Sledgehammer and the given language model.
Method
Autoformalization pass @1
miniF2F-valid"
miniF2F-test
Sledgehammer
14.72%
20.49%
Code Llama 7b
16.31%
17.62%
LLEMMA-7b
20.60%
22.13%
Code Llama 7b Sledgehammer
20.17% 25.97%
25.00%
L.LEMM-7h U Sledgehammer
27.46%
Table 11: Isabelle autoformalization. *We exclude the 11 examples used in the few-shot prompts. Pass@1 I with greedy decoding.
G SUPERVISED FINETUNING
A full exploration of finetuning applications for LLEMMA, such instruction following (uuang
al. 2022 Wei et al. 2022), dialogue modeling (Thoppilan et al. 2022 Touvron et al. 2023 Collins al. 2023). and reward modeling (Cobbe et al., 2021 Lightman al. 2023) outside the scope
of this work. However, to establish that LLEMMA retains its advantage over other open models when finetuned, conduct preliminary experiments finetuning ALEMMA-77B MetaMathQA (Yu et al.) 2023), supervised dataset targeted at the MATH and GSM8k benchmarks. Results are shown in
Table 12
Initialization
Finetune Dataset
MATH
GSM8k
Llama 2 7B
WizardMath (Proprietary)
10.7%
54.9%
Llama 7B
MetaMathQA
19.4%
66.4%
LLEMMA 7B
MetaMathQA
25.2%
66.5 %
Llama 2 70B
WizardMath (Proprietary)
22.7%
81.6%
Llama 2 70B
MetaMathQA
26.6%
82.3%
Table 12: Finetuning various 7B base models on supervised mathematics datasets. All results with Llama 2 initialization copied from the literature (Luo et al.) 2023 Yu et al. 2023). The LLEMMA 7B finetune trained with identical hyperparameters to the models in Yu et a. (2023)
H QUALITATIVE EXAMPLES
shows example false positives when checking r-gram overlap with Open WebMath documents for various n. Figure shoows an example Open WebMath document that has 30- -raa overlap with MATH problem, and LLEMMA-7b's generated solution.
Dataset overlap. Figure 6
Task outputs.
Figure 8 shows a generated proof in the informal2formal theorem proving task.
25

---

Published as a conference paper at ICLR 2024
OpenWebMath document
2n affine transformations are simply linear combinationn of variables. The advantage of this is that the matrices multiplication ALso, with this representation. As result, scale matrix is \bmatinb s_x W 5.y lend(bmatrix))
better represented vaing by matrices, ainca they
associative
modern toolkits optimised
rotation matrix (bogan(bmatrri) Yeas Athota -lsin Asin \theta \cos Atheta (ama(iimt.i
translation matrix 1a stmply \begt [bmatriix \fracit_xHy)
MATH problem
(13) (0)
5 -12
A rotation centered at the origin takes
Which vector does the rotation take
to?
MATH solution
cos
sin Thus... cos 0
The rotation matrix must form sin 0
Hit
\cos \theta & Asin \theta VI
Asin \theta \oos
OpenWebMath document
sasic Probability
& number is selected at randon. from. through 130, inclusive. What is the probability that the aumber is a divisor of 50? Express your answez as a commen Eraction.
Apr 24, 2019
There are 100 integars batween 1-103, inclusiva. since 50 in 0$2+55259, it has (1+1111 (1+21-12) (31-655 factors. Thua, the answer $8/frac|6) (b000) (1
MATH problem
A number is selected at random from through 100, inclusive. What is the probability that the number is perfect square?
Hit
number selected at random from through 100, inclusive. What is the probability the number is
Math document Fig.
Jae values of the nost used medicinal plants in the Sall Province (Mozccoo).
It is alse important to note that for the abovementioned medicinsl plants, many other folk have been reported in dfffrrttt regiona Norcsco. Pirthermore,
L'teratuze--eet based preof revealed that these apecies have proven a wide variety of biological
phermacological activities (lable 4,
[11, 17,
20,
24, 26, 28, 30, 31, 34, 35, 36, 38, 39, 65, 66, 63, 68, 69, 70, 31, 72, 73, 74, 75, 76, 77, 18, 79, 80, 81, 82, 63, 34, 85, 85, 87, 88, 89, 92, 91, 32, 33, 94, 35, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112. 113.
114, 115, 116]), which may confirm the diffarent popular applications
Generated solution (LLEMMA 7b):
The first 100 positive integers 123345667..9
2.G.S555...........0.0....2..... 79,80,8 8.8.888882.3,888...66 R.B.SAS.SS..........9999999.....
We can see that..
Figure 6: Data overlap: Example false positives using 10-gram match between MATH solutions and Open- WebMath documents (top), 20-gram match between MATH problems and Open MahMWhh documents (middle). and 30-gram match between LLEMMA-7b's generated solutions and Mathaahhthh documents (bottom).
26

---

Published as a conference paper at ICLR 2024
Open Math document
triangle [ormed edges <-ong Line By the 9xs-exis, and the line $xmk3. If the azea of the zsiangle is less than 8209, sum all possible integral values aks.
Feb 28, 2018
Look at the graph, here... two triangles are possible https://www stsp:://www.denoss wateee.cooccaccuaatteee jogdd///
The Seight of the triangles at any point will be forned by
(2/31X 5
will Su.... want to sulve this
7.5)
7.5]
(1/2)
5 [ 7.5
(2/31x 5 x 7.5] = 40 (2/3)x22
(2/3)x-2 10x 2.5
Jaing little technology... the triengle Eormed above the x axis will be .246
And the min value for the triangle formed balow the x axis will be -15.246
with the given boundaries, the integer of all possible values of k giving triang les with an area units"2
(-15) + )-14) (-13) (15) (16)
-2) 1-11--111 001
-120
Feb 28, 2018
MATH Problem: A triangle is formed with edges along the line fo + 5, the i-axis, and the line x = k. If the arca of the triangle is less than 20, find the sum of all possible integral values of k. Answer: -120
Generated solution (LLEMMA 7b):
The triangle has vertices (k, 0), (0, 5). and (k, k + 5). The base of the triangle has length k, and the height triangle has length { k + 5. area the triangle is therefore
1 kl
2 5) =
1 5 3
= bh = 2
+
Since the of the triangle less than 20, have
2 < 1 1:2 10 <
This inequality is true if and only if A² + 5 - 10 is positive. Since 1.22 + 5/ 10 is a quadratic
with positive leading coefficient, it is positive if and only if its vertex is less than 0. The vertex of 2 + k 10 is 3. 125 Since 10 3 < 0, we have that f + 5 10 > 0 if and only if
l 5. Therefore, the only possible integral values of lo are l = 2, 4. The sum of these
values is 10 Final Answer: The final answer is 10.
Figure 7: Data overlap: Example Open WebMath document that has 30-gram overlap with the given MATH problem, and LLEMMA-76'S Ab'ss generated solution.
27

---

Published as a conference paper at ICLR 2024
Problem: 3a b -3,a a 3b 9. b 3c 19, then find abc. Show that it -56.
Informal Proof (Human-written): Summing all three equations yields that 5a 56 + 5c -3 19 = 25. Thus, a + + c = 5. Subtracting this from each of the given equations, we obtain that 2a 2, 4, 2c 14. Thus, -4, b 2, 7, and their product is abe -4 2 -5
Formal Statement and Proof:
theorem mathi_algebre algebraa_aa___ 338: fixes a b assumes "3 real
b -3" and "a + 9" and "a + 19"
shows b C -56" proof
(+ Summing all three equations yields that 5a + 5b + 5c -3 9 + 19 25.
Thus, + b + c == 5.
have "5
-- 19" using <ATP>
then have "5 (a + c) =25" <ATP>
then have "a + b + c = 5" <ATP>
(* Subtracting this from each of the given equations, we obtain that 2a
-8, 2b = 4, 2c 14. Thus, -4, == 2, =7, and their product is abe
-4 \times 2 \times
-56. *)
then have "2
-8" "2
4" c 14" using asams <ATP>
then have "a -4" "b = 2" "c 7" <ATP>
then show ?thesis <APP>
qed
Figure Informal-to-formall proving. The model is given the problem, informal proof, and formal statement, following Jiang et al. (2023). It generates formal proof (starting with proof -) containing Isabelle code, comments (( ((*...* .*))) that align the informal and formal proofs, and calls to an automated prover (shown <ATP>). The proof is from LLEMMA-7b with greedy decoding.
28


Reviews:
[{"review_id": "aAZ6crTFct", "reviewer": "Reviewer_HYfd", "summary": "This paper present a new model, namely LLEMMA, an open language model for mathematics. The model is used to solve math-related problems such as proving or calculators. The major contribution of the paper is opensourcing the model, as well as the training data and codes. The evaluation results show that the performance is encouraging.", "questions": "1. Have you experimented with different combination of training data?\n2. How did you perform instruction fine-tuning?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The model and code are opensourcing.\n2. It has proposed the Proof-Pile-2 data and will be released as well.\n3. It has shown a training method that works well by fine-tuning a llama2 based pretrained model.", "weaknesses": "1. It doesn't have much ablation study or analysis about the data configuration. For example, why we should use which part of data.\n2. It doesn't have much novelties, other than a model that experimentally looks ok.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "teLi1vqfuh", "reviewer": "Reviewer_JQiP", "summary": "In this submission, the authors released a new large-scale dataset for training mathematically-specified\nlarge language models. Additionally, based on the dataset, a new base model called LLemma is trained and released, which outperforms existing models like Code LLaMA and Minerva. Moreover, the dataset and the baseline are openly released, which helps to boost the research in AI4Math.", "questions": "Why did the authors train the 7B model for 200B tokens and the 34B (the larger) model for 50B (the fewer) tokens?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1. The paper is well-written and easy to follow. The details of data collection and training instructions are provided. Moreover, both data and model are released. \n\n2. The experimental part is solid. I especially like the ablation study of data mixture components given in Table 4, which helps to reveal the contribution of different data sources.", "weaknesses": "1. Technically, this submission is not so interesting, and I cannot learn anything new in the aspect of methodology. The claims and experimental results are natural — fine-tuning Code Llama on a larger mathematically specific dataset helps to improve its performance. Note that this is a very personal opinion:) It is OK if this work targets the topic of datasets and benchmarks.\n2. I hope that the authors can discuss more about their future plans in the section of Conclusion. In the field of AI4Math, the performance of the current LLM is still limited. What will the authors do in the next step? Will they continuously enlarge the dataset and/or model? Is this the final solution to AI4Math?\n3. The comparison between Code Llama and the proposed Llemma is not fair. It demonstrates the usefulness of the Proof-Pile-2 dataset. It would be nice if the authors could finetune Llama2 directly based on the Proof-Pile-2 dataset and show the model performance.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "1VP9171N7g", "reviewer": "Reviewer_Ch2c", "summary": "The paper proposed continual training with math/code data and achieved very competitive results on the related tasks. The evaluation is comprehensive and ablation studies are sound.", "questions": "- One thing would be interesting to know is that if pretrained from scratch, will it be better or not? \n- Do we still need fine-tuning in this case", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. This paper showcases that if we continue pretraining an LLM on a specific domain, we are able to get good performance. The authors established a good way to do domain adaptation.\n2. Data and training code are open-sourced, expect to have high reproducibility \n3. Ablation study is comprehensive.\n4. Writing is well-organized", "weaknesses": "- The authors are comparing their results with `Minerva`, however since the datasets and its mixture, model architecture, training methods are different, we don't know which part contributes to the good performance. \n- We don't know if there training from scratch or starting from other LLM (like llama2 base) could be as impactful as well", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)