Llemma

Analysis

Why This Paper Matters

Mathematics has long been a challenging frontier for large language models, requiring precise reasoning, symbolic manipulation, and often multi-step problem solving. While proprietary models like Minerva have shown impressive results, the lack of open alternatives hinders reproducibility and community-driven progress. Llemma addresses this gap by demonstrating that continued pretraining of an open base model (Code Llama) on a carefully curated math-focused dataset can yield competitive performance across diverse mathematical tasks—from chain-of-thought problem solving to formal theorem proving. This work is significant because it not only releases a capable model but also the underlying dataset, Proof-Pile-2, enabling others to build upon and extend these results.

How It Works

Llemma is built by continued pretraining of Code Llama on Proof-Pile-2, a 55-billion-token mixture of three primary sources: scientific papers (29B tokens from ArXiv via RedPajama), web data containing mathematics (15B tokens from OpenWebMath), and mathematical code (11B tokens from AlgebraicStack, including formal proof steps). A small fraction (5%) of general text from The Pile and GitHub is retained to prevent catastrophic forgetting. The training uses a standard autoregressive language modeling objective with bfloat16 mixed precision. The 7B model is trained for 200B tokens, while the 34B model for 50B tokens. Notably, before training Llemma 7B, the RoPE base period is contracted from θ=1,000,000 to θ=10,000 to allow for later long-context fine-tuning.

Evaluation spans three categories: chain-of-thought reasoning, tool use, and formal mathematics. For chain-of-thought, models generate step-by-step solutions in LaTeX or natural language, validated by exact string match or SymPy equivalence on datasets like MATH, GSM8k, OCWCourses, MMLU-STEM, and SAT. Tool use is tested by prompting the model to interleave natural language reasoning with Python code execution (MATH+Python and GSM8k+Python). Formal mathematics involves two tasks: informal-to-formal proving (generating Isabelle proofs from informal statements) and formal-to-formal proving (generating Lean tactic sequences), both evaluated on the miniF2F benchmark.

Results

Llemma consistently outperforms its Code Llama initialization across all chain-of-thought benchmarks. The 34B model achieves state-of-the-art results among open models and even surpasses the proprietary Minerva on the MATH dataset. Majority voting further boosts performance, as shown in the figure below.

In tool use tasks, Llemma improves over Code Llama on both MATH+Python and GSM8k+Python, demonstrating the benefit of math-specific pretraining for code-augmented reasoning.

For formal theorem proving, Llemma-7b closes 22.1% of theorems in the informal-to-formal Isabelle task, outperforming both its Code Llama initialization and the Sledgehammer automated prover. It also adds 26 new validation proofs and 17 new test proofs not found by Sledgehammer. In the formal-to-formal Lean task, Llemma-7b matches the performance of ReProver, a model specifically fine-tuned for tactic prediction, while being the first open model to demonstrate few-shot tactic prediction.

Significance

Llemma represents a major step toward democratizing mathematical AI. By releasing both the model and the Proof-Pile-2 dataset, the authors enable the research community to reproduce, extend, and build upon their work. The model's ability to perform tool use and formal theorem proving without finetuning highlights the effectiveness of continued pretraining on a well-structured corpus. This opens avenues for automated math tutoring, proof assistants, and scientific discovery. However, the work is limited to 7B and 34B scales and focuses on a specific set of benchmarks; future work may explore larger models, broader mathematical domains, and integration with interactive proof environments. Overall, Llemma sets a new standard for open math LLMs and provides a solid foundation for future research.