Source-linked AI summary
Llemma: An Open Language Model For Mathematics
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, Sean Welleck
TL;DR
Mathematics-focused language models have faced a tradeoff between domain specialization and open availability. Llemma addresses this by continuing Code Llama pretraining on the diverse Proof-Pile-2 corpus, producing models that achieve strong open-weights mathematical results and support tool use and theorem proving. The models, corpus, and code are openly released for future research.
Problem
Existing mathematics models were either closed access or lagged behind the closed-access state of the art, limiting their platform potential for further research.
Method
Llemma continues pretraining Code Llama on Proof-Pile-2, a mixture of scientific papers, mathematical web data, and mathematical code.
Results
Llemma achieves state-of-the-art results among open-weights models on mathematical problem-solving benchmarks and demonstrates Python tool use and few-shot tactic prediction for theorem proving.
Takeaways & Limitations
Llemma and Proof-Pile-2 provide an openly available base for studying mathematical reasoning, language-model generalization, dataset composition, and tool use.
Takeaways & Limitations
The analysis finds 13 30-gram overlaps with OpenWebMath in Llemma’s MATH generations, plus one polynomial-factoring instance, warranting further study of memorization.
Abstract
from arXiv · showhide
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 open base 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 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.
1 INTRODUCTION
Llemma adapts Code Llama into publicly available mathematics-focused base models by continued pretraining on diverse mathematical text and code. The work targets stronger mathematical reasoning while releasing models, data, and code for further research.
- Motivation: Domain-specific mathematics models can provide stronger in-domain capabilities than generalist models for a given computational cost.Mathematical problem solving draws on extensive specialized prior knowledge and supports research in reasoning, reward modeling, and algorithmic reasoning.
- Research gap: Prior mathematics models were either closed access or substantially behind the closed-access state of the art.
- Approach: Continued pretraining Code Llama on Proof-Pile-2 yields 7B and 34B Llemma base models with substantially improved mathematical capabilities.Proof-Pile-2 combines diverse mathematics-related text and code.
- Contributions: Llemma establishes a new state of the art among publicly released base models on MATH.
- Contributions: The project releases AlgebraicStack, an 11B-token dataset of code specifically related to mathematics.
- Contributions: Llemma can use Python and formal theorem provers to solve mathematical problems without additional finetuning.
- Contributions: Open models, training data, and code make Llemma a platform for future research in mathematical reasoning.
2 APPROACH
The approach forms Proof-Pile-2 from scientific papers, mathematical web data, and mathematical code, then continues autoregressive pretraining from Code Llama. Training produces 7B and 34B Llemma models under distinct compute and context configurations, with a documented RoPE limitation for the larger model.
- Model and training: Llemma models are 7B and 34B mathematics-specialized language models produced by continuing Code Llama pretraining on Proof-Pile-2.
- Data: Proof-Pile-2: Proof-Pile-2 is a 55B-token mixture of scientific papers, mathematical web data, and mathematical code.Except for the Lean proofsteps subset, its knowledge cutoff is April 2023.
- Data: Proof-Pile-2: AlgebraicStack contributes 11B tokens of source code from 17 languages spanning numerical, symbolic, and formal mathematics.
- Data: Proof-Pile-2: OpenWebMath supplies 15B tokens of web pages filtered for mathematical content, formatting, quality, and near-duplication.
- Data mixture: The training mixture uses Proof-Pile-2 for 95% of tokens, with 2% from the Pile and 3% from general code data.
- Model and training: The models use standard autoregressive language modeling, with 200B training tokens for 7B and 50B for 34B.
- Infrastructure: Training uses bfloat16 mixed precision across 256 A100 40GB GPUs with tensor parallelism and ZeRO Stage 1 sharding.
- Training compute: Llemma 7B and 34B use 4096-token contexts and roughly 23,000 and 47,000 A100-hours, respectively.
3 EVALUATION
The evaluation tests LLEMMA on mathematical reasoning, tool-assisted problem solving, and formal theorem proving using few-shot prompts and benchmark comparisons. Continued pretraining improves mathematical performance, tool use, and formal proving, while memorization does not clearly explain difficult-problem accuracy.
- Chain-of-thought mathematical problem solving: The evaluation covers five chain-of-thought benchmarks, including MATH, GSM8k, OCWCourses, MMLU-STEM, and SAT.Models generate self-contained solutions without external tools, using task-specific few-shot prompts.
- Chain-of-thought mathematical problem solving: A level-5 MATH example requires swapping the order of summation and recognizing that the resulting sum telescopes.The solution uses a 4-shot prompt and greedy decoding.
- Chain-of-thought mathematical problem solving: LLEMMA 34B improves over Code Llama by 20 percentage points on GSM8k and 13 points on MATH.LLEMMA 7B also outperforms the proprietary Minerva model, and the approach outperforms open-weight models available at the time.
- Mathematical problem solving with tool use: LLEMMA improves over Code Llama on MATH+Python and GSM8k+Python, with tool-assisted performance higher than performance without tools.The MATH+Python setup alternates natural-language solution steps with code execution, while GSM8k+Python generates a program producing an integer answer.
- Formal mathematics: Formal evaluation tests informal-to-formal proving in Isabelle and formal-to-formal tactic generation in Lean on miniF2F.Formal proofs are checked by proof assistants; formal-to-formal proving uses best-first search with a timeout.
- Formal mathematics: LLEMMA-7B closes 22.1% of informal-to-formal theorems, while combining its proofs with Sledgehammer adds 26 validation proofs and 17 test proofs.On Lean 4 formal-to-formal proving, LLEMMA-7B improves over Code Llama and performs similarly to ReProver.
- Memorization analysis: Test-problem memorization does not clearly explain performance: Level 5 accuracy is 6.08% with a 30-gram hit versus 6.39% without one.Manual inspection found 41 of 100 sampled hits had no solution and 49 had an alternative solution with the same answer.
4 RELATED WORK
Related work spans generalist language models, domain adaptation through continued training, mathematical reasoning, and formal theorem proving. It also highlights the tension between task-specific finetuning and base models intended as research platforms.
- Large language model research combines increasing model and data scale with a progression toward generalist models and broader open access.
- Domain adaptation: Domain adaptation commonly continues training pretrained models on novel domains, alongside general-domain pretraining and shorter finetuning for instruction following or preference alignment.
- Language models for mathematics: Mathematics research evaluates language-model knowledge and reasoning, but correctness of answers and processes becomes difficult to assess as models improve.
- Language models for mathematics: Supervised finetuning improves some mathematical benchmarks but specializes models for particular tasks, whereas base-model training targets platforms for further development.
- Language models for formal mathematics: Formal-mathematics work includes tactic prediction, autoformalization, and integrated tools, with search imposing substantial computational costs.
5 CONCLUSION
The paper introduces LLEMMA and Proof-Pile-2 as openly available resources for mathematical language modeling. It reports strong open-weights benchmark performance, external-tool use, and few-shot theorem-proving capabilities, while positioning the resources for future research.
- LLEMMA and Proof-Pile-2 are introduced as a base model and corpus for language modeling of mathematics.
- The models, dataset, and code are openly available for research and replication.
- LLEMMA achieves state-of-the-art results for open-weights models on mathematical problem-solving benchmarks.
- LLEMMA uses external tools through Python code and demonstrates few-shot tactic prediction for theorem proving.
- The released resources support future work on model generalization, dataset composition, domain-specific models, and mathematical reasoning tools.
B DATA: Proof-Pile-2
Proof-Pile-2 combines scientific papers, mathematical web data, and mathematical code, while its data construction applies source-specific filtering, cutoff dates, size and density limits, and deduplication.
- Proof-Pile-2 data sources and training-mixture weights are documented in a dedicated table.
- AlgebraicStack: AlgebraicStack contains roughly 11B tokens of mathematics-related code, with sources, filtering, and content described alongside language-level token counts.
- Source processing: The dataset supplements Stack coverage by downloading underrepresented or problematic programming languages through the GitHub Python API.
- Formal mathematics data: Formal-language data uses extensions and theorem-related keyword filters, with Isabelle data restricted to selected Archive of Formal Proofs content.
- Cutoffs and preprocessing: Across languages, preprocessing removes oversized or numerically dense files and performs document-level exact deduplication using overlapping 2048-character chunks.
- Formal mathematics data: Lean tactic-state and next-tactic pairs come from Mathlib 4 at commit c779bd5, created August 20, 2023.
- Source composition: The corpus includes ArXiv accessed in April 2023, OpenWebMath for web mathematics, and Stack-derived programming-language data.
C EVALUATION HARNESS
The evaluation harness provides a public, model-agnostic framework for reproducible mathematics evaluations. It includes benchmark tasks for perplexity, problem solving, tool use, formalization, and theorem proving, with Isabelle proofs checked through specified automation and timeouts.
- The public fork of the Language Model Evaluation Harness implements math-related tasks and standardized, reproducible evaluation protocols.
- Evaluation tasks: Evaluation tasks cover MATH perplexity, Isabelle autoformalization, Minerva-style mathematics and STEM benchmarks, OCW Courses, GSM8K with Python, and SymPy evaluation.
- The implementations, prompts, and evaluation tasks are included in the public codebase.
- Isabelle proving: Isabelle evaluation lets models generate sledgehammer to invoke built-in automation, uses a 30-second timeout, and checks proofs through Portal-to-Isabelle.
D.2 LEAN THEOREM PROVING
The Lean theorem-proving evaluation generates tactics from proof states and checks them through Lean, using a separate open-source evaluation setup with bounded best-first search.
- Setup: The evaluation uses a separate open-source setup because integrating proof-assistant interactions into the evaluation harness is outside the work’s scope.The evaluation code is included in the public codebase.
- Setup: The task generates formal proofs for formalized statements, which are checked by Lean.The evaluation uses miniF2F, containing 488 statements from math competitions and undergraduate coursework.
- Search: Best-first search is parameterized by attempts, tactics per iteration, and maximum iterations, with search budget defined as N × S × T.The setup uses N = 1, S = 32, and T = 100, with beam search and a 10-minute timeout.
- Prompt: The model is prompted with three state–tactic examples before generating the next tactic from a Lean tactic state.The prompt format is illustrated in Figure 5.
E DATASHEET
The Proof-Pile-2 datasheet documents the dataset as a collection of text-only documents and directs readers to the paper for detailed token counts.
- Datasheet: Proof-Pile-2 is documented with a datasheet following the framework of Gebru et al. (2021).The datasheet is presented as Table 10.
- Instances: The dataset instances are text-only documents.
- Dataset size: The datasheet states that fine-grained total token counts are detailed elsewhere in the paper.
- Labels and targets: The supplied datasheet passages pose questions about instance labels or targets without providing an associated answer.
F.1 PROOF AUTOFORMALIZATION
The Isabelle autoformalization results are reported in Table 11, which includes the union of theorems closed by Sledgehammer and the language model under greedy decoding.
- Results: Table 11 reports additional Isabelle autoformalization results, including the union of theorems closed by Sledgehammer and the language model.The table excludes the 11 examples used in the few-shot prompts and reports Pass@1 with greedy decoding.
G SUPERVISED FINETUNING
The paper limits its finetuning study to preliminary LLEMMA-7B experiments on MetaMathQA, while the supplied figures and examples document dataset overlap and theorem-proving outputs.
- Scope: A full exploration of finetuning applications is outside the scope of the work.The omitted applications include instruction following, dialogue modeling, and reward modeling.
- Finetuning: The preliminary finetuning experiment uses LLEMMA-7B and MetaMathQA, a supervised dataset targeting MATH and GSM8k.Results are reported in Table 12.
- Dataset overlap: Figure 6 shows example false positives from n-gram overlap checks involving MATH solutions, MATH problems, generated solutions, and OpenWebMath documents.The figure uses 10-, 20-, and 30-gram matches for different comparisons.
- Task outputs: Figure 8 shows a generated proof for informal-to-formal theorem proving.The figure includes Isabelle code, comments aligning informal and formal proofs, and automated-prover calls.
- Dataset overlap: Figure 7 presents an OpenWebMath document with 30-gram overlap with a MATH problem and LLEMMA-7B’s generated solution.