Research map / Large language models / Agents, code and math
Llemma: An Open Language Model for Mathematics
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Continues pretraining Code Llama on the 55B-token Proof-Pile-2 math corpus to produce open 7B and 34B Llemma models that lead open base models on MATH and show few-shot tool use and formal theorem proving.
Problem
Open language models lag behind closed math-specialized models (e.g., Minerva) on mathematical reasoning, and no open, reproducible math-specialized base model with released data existed.
Approach
Adapt a code-pretrained base model to mathematics via continued pretraining on a curated math mixture (Proof-Pile-2 with arXiv, OpenWebMath, and the AlgebraicStack code dataset), releasing all artifacts openly.
Key results
- Llemma-34B reaches 25.0% on MATH with 4-shot greedy decoding versus 12.2% for Code Llama 34B, and 51.5% on GSM8k versus 29.6%.
- Llemma-7B achieves 18.0% on MATH, above Minerva 8B at 14.1%, and 36.4% on GSM8k versus 16.2% for Minerva 8B.
- On Lean formal-to-formal miniF2F-test, Llemma-7B proves 26.23% of theorems, close to ReProver's 26.50%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · GSM8k | accuracy: 29.6% -> 51.5% | Helped |
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · OCW | accuracy: 7.0% -> 11.8% | Helped |
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · MMLU-STEM | accuracy: 40.5% -> 49.0% | Helped |
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · SAT | accuracy: 40.6% -> 71.9% | Helped |
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · MATH | accuracy: 12.2% -> 25.0% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 7B and 34B · GSM8k+Python and MATH+Python | pass@1: 27.1% -> 40.1%; 17.2% -> 21.5%; 52.7% -> 62.6%; 23.5% -> 27.1% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 7B · miniF2F-valid (Isabelle informal-to-formal) | proven theorems: 16.31% -> 20.60% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 7B · miniF2F-test (Isabelle informal-to-formal) | proven theorems: 17.62% -> 22.13% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 34B · miniF2F-valid (Isabelle informal-to-formal) | proven theorems: 18.45% -> 21.03% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 34B · miniF2F-test (Isabelle informal-to-formal) | proven theorems: 18.03% -> 21.31% | Helped |
| Continue pretraining Code Llama on Proof-Pile-2 | Code Llama 7B · miniF2F-test (Lean formal-to-formal) | proven theorems: 20.49% -> 26.23% | Helped |
| Continue pretraining Code Llama 34B on Proof-Pile-2 | Code Llama 34B · miniF2F-test (Lean formal-to-formal) | proven theorems: 22.13% -> 25.82% | Helped |
Surprising findings
- Llemma-7B's MATH and GSM8k perplexity-based mixture selection and evaluation showed 30-gram test overlap with the corpus, yet hit accuracy was no higher than non-hit accuracy at higher difficulty levels.
- Code Llama 7B scores below random guessing on MMLU-STEM and SAT, largely because it fails to end its chain of thought with a valid answer.
Limitations
- Llemma-34B was trained with unchanged RoPE base, and the authors could not verify that contracting RoPE for 34B would not hurt performance.
- Test problems and solutions appear in the pretraining corpus (about 7% of MATH problem statements have 30-gram hits), so contamination is a concern.
- Formal theorem proving evaluation is limited to miniF2F and a single search budget; the work does not fully investigate formal mathematics.
Experimental setup
Datasets: Proof-Pile-2 AlgebraicStack OpenWebMath RedPajama ArXiv The Pile MATH GSM8k MetaMathQA miniF2F
Benchmarks: MATH GSM8k OCWCourses MMLU-STEM SAT miniF2F
Metrics: accuracy maj@k pass@1 perplexity
Baselines: Minerva Code Llama Llama 2 Sledgehammer ReProver COPRA
Builds on: Code Llama Minerva OpenWebMath RedPajama GPT-NeoX
Closest papers by meaning
- RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.90)
- MathArena: Evaluating LLMs on Uncontaminated Math Competitions (NeurIPS 2025 · similarity 0.90)
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.89)
- MathConstruct: Challenging LLM Reasoning with Constructive Proofs (ICML 2025 · similarity 0.89)
- One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · similarity 0.89)
- MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs (ICLR 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.