# 2023 Rozière et al.

Code Llama: Open Foundation Models for Code

LLEMMA：一个用于数学的开放语言模型 Zhangir Azerbayev$^{1,2}$ Hailey Schoelkopf$^{2}$ Keiran Paster$^{3,4}$ Marco Dos Santos$^{5}$ Stephen McAleer$^{6}$ Albert Q. Jiang$^{5}$ Jia Deng$^{1}$ Stella Bider...

精粹译文

LLEMMA：一个用于数学的开放语言模型

Zhangir Azerbayev1,2^{1,2} Hailey Schoelkopf2^{2} Keiran Paster3,4^{3,4} Marco Dos Santos5^{5} Stephen McAleer6^{6} Albert Q. Jiang5^{5} Jia Deng1^{1} Stella Biderman2^{2} Sean Welleck6,7^{6,7}

1^{1}普林斯顿大学 2^{2}EleutherAI 3^{3}多伦多大学 4^{4}向量研究所 5^{5}剑桥大学 6^{6}卡内基梅隆大学 7^{7}华盛顿大学

摘要

我们提出了 LLEMMA，一个用于数学的大型语言模型。我们在 Proof-Pile-2（一个包含科学论文、包含数学内容的网络数据以及数学代码的混合数据集）上对 Code Llama 进行了持续预训练，从而得到了 LLEMMA。在 MATH 基准测试中，LLEMMA 在同等参数规模下优于所有已知的开源基础模型，以及未发布的 Minerva 模型套件。此外，LLEMMA 无需任何进一步的微调即可进行工具使用和形式化定理证明。我们公开了所有产出，包括 70 亿和 340 亿参数的模型、Proof-Pile-2 数据集以及用于复现我们实验的代码。1^{1}

1 引言

在多样化的文本混合数据上训练的语言模型展现出了卓越的通用语言理解和生成能力（Brown 等人，2020；Chowdhery 等人，2022），并作为基础模型被适配到广泛的应用中（Raffel 等人，2023）。诸如开放式对话（Thoppilan 等人，2022；Touvron 等人，2023）或指令遵循（Ouyang 等人，2022；Wei 等人，2022）等应用需要自然文本全分布范围内的平衡性能，因此倾向于通用模型。然而，如果我们寻求在单一领域（如医学（Singhal 等人，2022；2023）、金融（Wu 等人，2023）或科学（Taylor 等人，2022））内最大化性能，那么特定领域的语言模型可以在给定的计算成本下提供卓越的能力，或者在给定的能力水平下降低计算成本。

在这项工作中，我们训练了一个用于数学的特定领域语言模型。我们这样做有几个动机。首先，解决数学问题需要针对大量专业先验知识进行模式匹配，这使其成为领域适配的理想场景。其次，数学推理本身就是一项核心的 AI 任务，其研究至少可以追溯到 Gelernter (1959) 和 Wang (1960)，并持续至今（Lu 等人，2023）。第三，具备强大数学推理能力的语言模型是许多研究课题的上游，例如奖励建模（Uesato 等人，2022；Lightman 等人，2023）、推理强化学习（Polu 等人，2022；Lample 等人，2022）以及算法推理（Zhou 等人，2022；Zhang 等人，2023）。

图 1：在 Proof-Pile-2 上进行持续预训练产生了 LLEMMA，这是一个具有改进数学能力的基础模型。

尽管过去曾训练过用于数学的特定领域模型，但它们要么是闭源的（Lewkowycz 等人，2022），限制了它们成为进一步研究平台的能力，要么远远落后于闭源的先进水平（Azerbayev 等人，2023）。

我们提出了一种通过在 Proof-Pile-2（一个多样化的数学相关文本和代码混合数据集）上进行持续预训练（Lewkowycz 等人，2022；Rozière 等人，2023）来将语言模型适配到数学领域的方案。将该方案应用于 Code Llama（Rozière 等人，2023）产生了 LLEMMA：具有显著改进数学能力的 70 亿和 340 亿参数基础语言模型。

具体而言，我们的贡献如下：

  1. 我们训练并发布了 LLEMMA 模型：专门用于数学的 7B 和 34B 参数语言模型。LLEMMA 模型是 MATH 基准测试（Lewkowycz 等人，2022）上公开发布的基础模型的新先进水平。
  2. 我们发布了 AlgebraicStack，这是一个包含 11B token 的专门与数学相关的代码数据集。
  3. 我们证明了 LLEMMA 能够使用计算工具来解决数学问题，即 Python 解释器和形式化定理证明器。
  4. 与之前的数学语言模型（如 Minerva（Lewkowycz 等人，2022））不同，LLEMMA 模型是开放获取的，并且我们开源了我们的训练数据和代码。这使得 LLEMMA 能够作为数学推理未来研究的平台。

我们的工作建立在 Minerva（Lewkowycz 等人，2022）的研究结果之上，但在几个方面有所不同：（1）LLEMMA 的训练和评估涵盖了更广泛的数据和任务，特别是代码数据（例如 AlgebraicStack）、工具使用和形式化数学；（2）我们的工作仅依赖于公开可用的工具和数据；（3）我们提供了与持续训练数据混合、记忆化和额外监督微调相关的新分析；（4）我们将所有产出公开。

2 方法

LLEMMA 模型是专门用于数学的 70 亿和 340 亿参数语言模型。我们的方法是在 Proof-Pile-2 上持续预训练 Code Llama（Rozière 等人，2023）。

模型适配 token 数开放
Minerva-8b164B✗
Minerva-62b109B✗
LLEMMA-7b (ours)200B✓
LLEMMA-34b (ours)50B✓
数据集token 数开放
Minerva Dataset38.5B✗
Proof-Pile-2 (ours)55B✓
Code (AlgebraicStack)11B✓
OpenWebMath (Paster et al., 2023))15B✓
ArXiv (Computer, 2023))29B✓

图 2：LLEMMA 与 Minerva 训练对比

2.1 数据：Proof-Pile-2

我们组建了 Proof-Pile-2，这是一个包含 55B token 的科学论文、包含数学的网络数据和数学代码的混合数据集。除了 Lean proofsteps 子集（参见附录 B）外，Proof-Pile-2 的知识截止日期为 2023 年 4 月。

代码。数值模拟、计算机代数系统和形式化定理证明器等计算工具对数学家来说越来越重要（Avigad，2018）。受此事实启发，我们创建了 AlgebraicStack，这是一个包含 11B token 的源自 17 种语言的源代码数据集，涵盖数值、符号和形式化数学。该数据集由来自 The Stack（Kocetkov 等人，2022）、公共 GitHub 存储库和形式化 proofstep 数据中的过滤代码组成。表 9 显示了 AlgebraicStack 中按语言划分的 token 数量。有关 AlgebraicStack 的更多详细信息，请参阅附录 B.1。

网络数据。我们使用 OpenWebMath（Paster 等人，2023），这是一个包含 15B token 的高质量网页数据集，这些网页经过了数学内容的过滤。OpenWebMath 基于数学相关关键词和基于分类器的数学分数过滤 CommonCrawl 网页，保留数学格式（例如 LaTeX\LaTeX、AsciiMath），并包含额外的质量过滤器（例如困惑度、领域、长度）和近去重。有关 OpenWebMath 的完整描述，请参阅 Paster 等人（2023）。

科学论文。我们使用 RedPajama 的 ArXiv 子集（Computer，2023），这是 LLaMA 训练数据集的开源复现。ArXiv 子集包含 29B token。

通用自然语言和代码数据。遵循 Lewkowycz 等人（2022），我们的训练混合数据包含少量通用领域数据，其作用是一种正则化形式。由于 LLaMA 2 的预训练数据集未公开，我们使用 The Pile（Gao 等人，2020；Biderman 等人，2022）作为替代训练数据集。我们将训练混合数据的 95% 设置为 Proof-Pile-2，2% 来自 The Pile（移除了 ArXiv，因为它已单独包含在 Proof-Pile-2 中），3% 为 RedPajama 的 GitHub 子集（Computer，2023）。

有关数据集组成和数据表的更多信息分别在附录 B 和附录 E 中。我们公开了 Proof-Pile-2，地址为 hf.co/datasets/EleutherAI/proof-pile-2。

2.2 模型与训练

每个模型均从 Code Llama（Rozière 等人，2023）初始化。Code Llama 模型是仅解码器的 Transformer 语言模型，从 Llama 2（Touvron 等人，2023）初始化，并在 500B token 的代码上进行了进一步训练。我们使用标准的自回归语言建模目标在 Proof-Pile-2 上继续训练 Code Llama 模型。我们对 7B 模型训练了 200B token，对 34B 模型训练了 50B token。

我们使用 GPT-NeoX 库（Andonian 等人，2023）在 256 个 A100 40GB GPU 上以 bfloat16 混合精度训练所有模型。我们对 LLEMMA-7B 使用了世界大小为 2 的张量并行（Shoeybi 等人，2019），对 LLEMMA-34B 使用了世界大小为 8 的张量并行，并在数据并行（Goyal 等人，2017）副本上使用了 ZeRO Stage 1 分片优化器状态（Rajbhandari 等人，2020）。我们使用 Flash Attention 2（Dao，2023）来提高吞吐量并进一步降低内存需求。

LLEMMA 7B 训练了 42,000 步，全局批大小为 400 万 token，上下文长度为 4096。这相当于大约 23,000 个 A100 小时。学习率在 500 步内预热至 1⋅10−41 \cdot 10^{-4}，然后在 48,000 步内余弦衰减至最大学习率的 1/30。训练步数与调度器长度之间存在差异的原因是我们计划训练 48,000 步，但在 42,000 步后遇到了 NaN 损失，这可能是由不稳定的优化或硬件故障引起的（Elsen 等人，2023）。

LLEMMA 34B 训练了 12,000 步，全局批大小为 400 万 token，上下文长度为 4096。这相当于大约 47,000 个 A100 小时。学习率在 500 步内预热至 5⋅10−55 \cdot 10^{-5}，然后衰减至峰值学习率的 1/30。

在训练 LLEMMA 7B 之前，我们将 Code Llama 7B 初始化中的 RoPE（Su 等人，2022）基周期从 θ=1,000,000\theta = 1,000,000 收缩至 θ=10,000\theta = 10,000。这是为了使 Peng 等人（2023）和 Rozière 等人（2023）中描述的长上下文微调过程可以在训练后的 LLEMMA 7B 上重复（我们留待未来工作实际执行）。由于计算限制，我们无法验证使用收缩的 RoPE 基周期训练 LLEMMA 34B 是否会带来性能损失，因此对于该模型，我们保留了 θ=1,000,000\theta = 1,000,000。

3 评估

我们的目标是评估 LLEMMA 作为数学文本基础模型的能力。为此，我们使用少样本评估（Brown 等人，2020）比较 LLEMMA 模型，并主要关注尚未针对该任务进行监督示例微调的先进模型。首先，我们评估模型使用思维链推理（Wei 等人，2023）和多数投票（Wang 等人，2023）解决数学问题的能力。我们的评估包括 MATH（Hendrycks 等人，2021b）和 GSM8k（Cobbe 等人，2021），这是评估语言模型定量推理的事实标准基准（Lewkowycz 等人，2022）。其次，我们探索少样本工具使用和形式化定理证明。第三，我们研究记忆化和数据混合的影响。附录 G 包含了一项关于 LLEMMA 监督微调的初步研究。

3.1 思维链数学问题解决

这些任务涉及生成用 LaTeX\LaTeX 或自然语言表达的问题的自包含文本解决方案，而不使用外部工具（Lewkowycz 等人，2022）。我们使用以下评估：

  • MATH（Hendrycks 等人，2021b），一个包含来自高中数学竞赛的 12.5k 个问题（5k 评估）的数据集。给定问题陈述，模型生成一个 LaTeX\LaTeX 解决方案和一个必须与参考答案匹配的答案。我们遵循与 Lewkowycz 等人（2022）类似的任务实现，使用他们的四个示例提示，并评估答案的精确字符串匹配或 SymPy 等价性。
  • GSM8k（Cobbe 等人，2021），一个初中水平数学应用题数据集。我们使用 Wei 等人（2023）的 8-shot 提示，因为 Lewkowycz 等人（2022）没有指定他们的评估提示或少样本示例数量。
  • OCWCourses（Lewkowycz 等人，2022），从麻省理工学院 OpenCourseWare 收集的本科水平 STEM 问题集合。我们使用（Lewkowycz 等人，2022）提供的四个示例提示。
  • MMLU-STEM（Hendrycks 等人，2021a），MMLU 基准测试中 57 个学科中的 18 个子集。我们遵循 Lewkowycz 等人（2022）并使用他们提供的四个示例思维链提示。
  • SAT，我们创建了一个数据集，由 2023 年 5 月美国大学理事会 SAT 考试中不包含图形的 32 道数学题组成，该考试在我们模型的知识截止日期之后。

图 3：LLEMMA 34B 对 MATH（Hendrycks 等人，2021a）问题的解决方案示例。该问题被标记为难度等级 5，是 MATH 中的最高等级。模型在 3.1 节描述的 4-shot 提示下进行条件化，解决方案通过贪婪解码产生。模型必须应用两个非平凡步骤来解决此问题：（1）注意到交换求和顺序简化了问题，以及（2）注意到所得和是裂项求和。

我们与 Minerva（Lewkowycz 等人，2022）进行了比较，后者在技术内容数据集上继续预训练了 PaLM 语言模型；Code Llama，LLEMMA 持续预训练的初始化；以及 Llama 2，Code Llama 在代码上持续预训练的初始化。对于开放获取模型，我们报告使用我们的评估套件计算的分数，该套件实现为语言模型评估工具（Language Model Evaluation Harness）（Gao 等人，2021）的一个分支。对于 Minerva 模型，我们报告来自 Lewkowycz 等人（2022）的基准分数。

结果。LLEMMA 在 Proof-Pile-2 上的持续预训练提高了在五个数学基准测试上的少样本性能。LLEMMA 34B 在 GSM8k 上比 Code Llama 提高了 20 个百分点，在 MATH 上提高了 13 个点，并且 LLEMMA 7B 优于专有的 Minerva 模型。我们的方法在撰写本文时也优于所有开放权重语言模型。我们得出结论，在 Proof-Pile-2 上进行持续预训练对于提高预训练模型执行数学问题解决的能力是有效的。

LLEMMA 在多样化的数学相关数据分布上进行预训练，并未针对特定任务进行调整。因此，我们预计 LLEMMA 可以通过特定任务微调和少样本提示适配到许多其他任务。

GSM8kOCWMMLU-STEMSATMATH
Llama 2 7B11.8%3.7%29.9%25.0%3.2%
Code Llama 7B10.5%4.4%25.1%9.4%4.5%
Minerva 8B16.2%7.7%35.6%-14.1%
LLEMMA 7B36.4%7.7%37.7%53.1%18.0%
Code Llama 34B29.6%7.0%40.5%40.6%12.2%
LLEMMA 34B51.5%11.8%49.0%71.9%25.0%
Minerva 62B52.4%12.0%53.9%-27.6%
Minerva 540B58.8%17.6%63.9%-33.6%

表 1：五个思维链推理任务的结果，样本通过贪婪解码生成。Minerva 结果引用自 Lewkowycz 等人（2022）。注意 CodeLlama 7B 在 MMLU 和 SAT 上的表现比随机猜测（25%）差，这主要是因为它未能以有效答案结束其思维链。

GSM8k maj@kOCW maj@kMMLU-STEM maj@kSAT maj@kMATH maj@k
Minerva 8B28.4%12.5%43.4%-25.4%
LLEMMA 7B54.0%14.3%49.9%78.1%33.5%
LLEMMA 34B69.3%18.4%59.7%81.3%43.1%
Minerva 62B68.5%23.5%63.5%-43.4%
Minerva 540B78.5%30.8%75.0%-50.3%

表 2：LLEMMA 和 Minerva 的多数投票结果。Minerva 结果引用自 Lewkowycz 等人（2022）。投票使用 MATH 的 k=256k=256，GSM8k 和 OCW 的 k=100k=100，以及 MMLU-STEM 和 SAT 的 k=16k=16 进行。我们使用 k=256k=256 和 k=100k=100 时温度 T=0.6T=0.6，对于 k=16k=16 时温度 T=0.3T=0.3 进行采样，并使用核采样，其中 p=0.95p=0.95（Holtzman 等人，2020）。由于计算限制，我们没有计算 Llama 2 和 Code Llama 的多数投票分数。

3.2 使用工具的数学问题解决

这些任务涉及在有权访问计算工具的情况下解决问题。我们评估以下内容：

  • MATH+Python，提示模型交替描述自然语言中的解决方案步骤，然后用代码执行该步骤。最终答案是一个执行为数值类型或 SymPy 对象的程序。我们的少样本提示包括使用内置数值运算、math 模块和 SymPy 的示例。
  • GSM8k+Python，通过编写执行为整数答案的 Python 程序来解决 GSM8k 应用题。我们使用 Gao 等人（2023）的提示。

结果。如表 3 所示，LLEMMA 在两项任务上都比 Code Llama 有所改进。它在有工具的情况下在 MATH 和 GSM8k 上的表现也高于其在没有工具的情况下在这些数据集上的表现。

GSM8k+Python pass@1MATH+Python pass@1
Code Llama 7B27.1%17.2%
LLEMMA 7B40.1%21.5%
Code Llama 34B52.7%23.5%
LLEMMA 34B62.6%27.1%

表 3：使用工具的数学问题解决。

3.3 形式化数学

交互式证明助手（如 Lean（de Moura 等人，2015）、Isabelle（Wenzel 等人，2008）和 Coq（Paulin-Mohring，1989a;b））用允许验证的编程语言表达数学。与主流语言相比，这些语言在预训练背景下数据稀缺。例如，BigCode 项目中用于预训练语言模型的 Stack 数据集拥有超过 700 GB 的 Python 代码，而 Lean 只有 322 MB。证明助手还需要模型利用原始源代码中不存在的信息，例如包含证明每一步信息的证明目标状态。

图 4：来自 LLEMMA-7b 的形式化证明示例。左：模型被给定一个问题、非正式证明和形式化陈述，遵循 Jiang 等人（2023）。它生成一个包含 Isabelle 代码和对自动化调用（显示为 <ATP>）的形式化证明（以 proof - 开头）。右：模型被给定一个证明状态（可视化为灰色注释），并生成后续步骤（例如 rw [..]）。

Proof-Pile-2 的 AlgebraicStack 包含超过 15 亿 token 的形式化数学数据，包括从 Lean 和 Isabelle 形式化中提取的证明状态。虽然对形式化数学的全面调查超出了本文的范围，但我们在两项任务上对 LLEMMA 进行了少样本评估：

  • 非正式到形式化证明（Jiang 等人，2023），给定形式化陈述、非正式 LaTeX\LaTeX 陈述和非正式 LaTeX\LaTeX 证明，生成形式化证明的任务。形式化证明由证明助手检查。我们使用 Isabelle 证明助手并在 miniF2F（Zheng 等人，2021）上进行评估，这是一个由奥林匹克竞赛和本科课程问题陈述组成的基准。对于提示，我们使用来自 Jiang 等人（2023）的 11 个（形式化陈述、非正式陈述、非正式证明、形式化证明）示例，为数论问题选择 7 个示例，为所有其他问题选择 6 个示例。我们通过贪婪解码生成单个证明。
  • 形式化到形式化证明（例如 Polu & Sutskever (2020)），通过生成一系列证明步骤（策略）来证明形式化陈述的任务。在每一步，输入是由证明助手给出的状态 xtx_t，语言模型的任务是生成一个证明步骤 yty_t（代码序列）。证明步骤由证明助手检查，产生一个新的状态 xt+1x_{t+1} 或错误消息。该过程继续，直到证明完成或达到超时。我们使用三个 (xt,yt)(x_t, y_t) 示例提示模型。我们使用 Lean 4 证明助手在 miniF2F（Zheng 等人，2021）上进行评估，并使用标准的最佳优先搜索。有关更多详细信息，请参阅附录 D。

结果。如表 4 所示，LLEMMA 在 Proof-Pile-2 上的持续预训练提高了在两项形式化定理证明任务上的少样本性能。

方法非正式到形式化 miniF2F-validminiF2F-test
Sledgehammer14.72%20.49%
Code Llama 7b16.31%17.62%
Code Llama 34b18.45%18.03%
LLEMMA-7b20.60%22.13%
LLEMMA-34b21.03%21.31%
方法形式化到形式化 搜索miniF2F-test
ReProver (微调)1×6426.50%
Code Llama 7b1×3220.49%
Code Llama 34b1×3222.13%
COPRA (GPT-4)-†23.36%
LLEMMA-7b1×3226.23%
LLEMMA-34b1×3225.82%

表 4：形式化定理证明任务。左：Isabelle 中的非正式到形式化证明，显示了使用贪婪解码证明的定理百分比。右：Lean 中的形式化到形式化证明，显示了在给定尝试次数 × 每次迭代的最佳优先搜索生成次数，以及 10 分钟超时的情况下证明的定理百分比。Sledgehammer（Paulson & Nipkow，2023）是内置的 Isabelle 自动化。ReProver（Yang 等人，2023）是一个监督和检索增强模型。COPRA（Thakur 等人，2023）是一种基于检索增强的 GPT-4 方法。† COPRA 不使用最佳优先搜索，而是从 GPT-4（OpenAI，2023）中采样最多 60 次。

在非正式到形式化证明方面，LLEMMA-7b 关闭了 22.1% 的定理，改进了其 Code Llama 初始化和 Sledgehammer 证明器。LLEMMA 证明的定理通常与 Sledgehammer 证明的定理互补：结合 Sledgehammer 和 LLEMMA 的证明导致了 26 个新的验证证明（增加了 11 个百分点）和 17 个新的测试证明（增加了 7 个点）；参见附录表 11。在我们的工作之前，唯一少样本证明自动形式化的演示使用了专有的 Codex 模型（Jiang 等人，2023）。

在 Lean 4 形式化到形式化证明方面，LLEMMA-7b 改进了其 Code Llama 初始化，并且表现类似于 ReProver（Yang 等人，2023），这是一个针对策略预测进行微调的检索增强语言模型。LLEMMA 使用 3 个示例提示适配到该任务，据我们所知，这是开放模型进行定理证明少样本策略预测的首次演示。

3.4 数据混合的影响

在训练语言模型时，根据混合权重对训练数据的高质量子集进行上采样是很常见的（Brown 等人，2020；Gao 等人，2020；Xie 等人，2023）。我们通过在几个手工挑选的混合权重上进行简短的训练运行来选择混合权重，然后选择在高质量留出文本集（我们使用 MATH 训练集）上最小化困惑度的权重。表 5 显示了使用 arXiv、Web 和代码的不同混合训练的模型的 MATH 训练集困惑度。基于这些结果，我们以 2 : 4 : 1 的比例训练了 LLEMMA。注意，我们的方法使用 MATH 训练集来确定训练超参数，尽管我们预计其效果与相关高质量文本的效果相似。

混合整体预代数代数数论计数与概率几何中间代数预微积分
2:4:11.4781.4951.5151.5521.4751.5191.4391.331
2:4:21.4821.5001.5191.5561.4771.5241.4431.334
4:2:11.4871.5051.5241.5611.4811.5341.4471.338
4:2:21.4891.5081.5271.5621.4831.5381.4471.339
4:4:11.4871.5061.5251.5611.4821.5291.4461.335
4:4:21.4851.5031.5231.5591.4801.5291.4441.334

表 5：使用不同数据混合训练的 Code Llama 7B 模型在减少步数后的 MATH 训练集困惑度。每个混合由其 arXiv:Web:Code 比例表示。

3.5 数据集重叠和记忆化

测试问题或解决方案是否出现在语料库中？我们检查测试序列（输入问题或输出解决方案）中的任何 30-gram 是否出现在任何 OpenWebMath 或 AlgebraicStack 文档中。如果是，我们称序列和文档之间发生了命中。表 6 显示了来自 MATH 的序列与来自 Proof-Pile-2 的文档之间的命中。使用我们的方法，大约 7% 的 MATH 测试问题陈述和 0.6% 的 MATH 测试解决方案有命中。注意，我们的方法给出了语义等价序列数量的下界（例如，它没有考虑替代措辞）。

我们手动检查了测试问题陈述和 OpenWebMath 文档之间均匀采样的 100 个命中。41 个案例没有解决方案，其中包括带有问题列表、讨论或提示的网站。49 个案例有与 MATH 真值解决方案不同的替代解决方案，但答案相同。这些包括以不同于真值的方式解决问题的解决方案、缺少细节的解决方案以及包含答案的讨论。9 个案例缺少或答案不正确，1 个案例与真值中的解决方案相同。总之，我们发现解决方案可以出现在源自网络文档的语料库中，特别是评估集中那些解决方案的替代方案。我们用 20-gram 命中重复了我们的分析，我们的发现是相似的，尽管有假阳性；参见附录图 6 中的示例。

Proof-Pile-2测试问题示例问题文档解决方案示例解决方案文档
OpenWebMathMATH3487173446
AlgebraicStackMATH3311
OpenWebMathGSM8k2300
AlgebraicStackGSM8k0000
相同解决方案1
不同解决方案，相同答案49
不同解决方案，不同答案9
无解决方案41
不同问题0

表 6：左：MATH 测试问题或解决方案与 Proof-Pile-2 文档之间的 30-gram 命中。示例和文档是有命中的唯一测试示例和 Proof-Pile-2 文档的数量。右：问题陈述与 Proof-Pile-2 文档之间 100 个命中的手动检查。

MATH 难度命中准确率非命中准确率# 命中
Level 172.7361.5011
Level 235.7140.1828
Level 330.3626.8856
Level 414.8916.6194
Level 56.086.39181

表 7：LLEMMA-34b 在命中（问题或解决方案与训练序列之间有 30-gram 重叠）和非命中上的准确率，按 MATH 难度等级划分。

语料库中的问题如何影响性能？接下来，我们评估 LLEMMA-34b 在有 30-gram 命中的测试示例和没有 30-gram 命中的测试示例上的表现。表 7 显示了按 MATH 难度等级划分的准确率。模型在困难问题上的准确率仍然很低（例如，Level 5 问题命中时为 6.08%，而没有命中的问题为 6.39%），并且我们观察到 30-gram 命中与各难度等级的准确率之间没有明确的关系。我们得出结论，测试示例与训练文档之间的非平凡匹配并不意味着模型生成了记忆化的正确答案。我们用 20-gram 和 7b 模型重复了该分析，我们的发现是类似的。图 7 显示了一个示例。

最后，我们检查了 LLEMMA 的 MATH 生成与 OpenWebMath 之间的 30-gram 命中。有 13 次命中，发生在模型生成常见数字序列（例如，斐波那契数列列表）时，外加一个多项式因式分解实例。附录图 6 显示了一个示例。我们发现所有这些观察结果都值得进一步研究。使用 LLEMMA 和 Proof-Pile-2 来更好地理解数据、记忆化和性能是一个有趣的未来方向。我们将分析代码包含在 LLEMMA 存储库中。

4 相关工作

大规模语言建模。大型语言模型的最新进展涉及两条相互关联的线索：模型和数据规模的不断扩大（Hoffmann 等人，2022；Kaplan 等人，2020；Chowdhery 等人，2022），以及向更通用模型（Radford 等人，2019；Brown 等人，2020）的演进，这些模型能够解决多样化的问题并快速适应新任务。第三条线索涉及实现对具备这些能力的语言模型的开放访问（Black 等人，2022；Biderman 等人，2023；Touvron 等人，2023；Rozière 等人，2023）。我们的工作提供了一种将这些语言模型专门化到数学领域的方案，为进一步的研究和应用提供了平台。

领域适配。语言模型应用通常需要一个通用领域的预训练步骤，随后是一个较短的微调步骤。微调步骤通常旨在灌输指令遵循能力（Sanh 等人，2022；Wei 等人，2022）或使模型的输出与人类偏好对齐（Ziegler 等人，2019；Ouyang 等人，2022；Bai 等人，2022）。其他工作探索通过持续训练（Rozière 等人，2023；Beltagy 等人，2019）、参数高效微调方法（Yong 等人，2023）、检索增强（Min 等人，2023；Asai 等人，2023）和其他技术将预训练模型适配到新领域。我们提供了一种涉及持续训练和针对性数据收集的适配方案。

数学语言模型。将大型语言模型应用于数学问题是机器学习的一个活跃子领域，包括在不同水平上对数学知识和推理进行基准测试（Hendrycks 等人，2021b；Zheng 等人，2021；Welleck 等人，2022；Azerbayev 等人，2023）。尽管实现强大的数学推理是一个重要的目标，但随着模型变得越来越强大，评估模型答案和过程的正确性变得困难（Bowman 等人，2022；Uesato 等人，2022；Lightman 等人，2023；Cobbe 等人，2021）。

许多近期工作专注于在任务相关（输入、输出）对上进行监督微调（例如 Yu 等人（2023）；Yue 等人（2023））。这样做提高了在一些常见数学语言建模基准上的性能，但使模型针对这些特定任务进行了训练。相比之下，Lewkowycz 等人（2022）和我们的工作寻求训练一个基础语言模型作为进一步发展的平台。

形式化数学语言模型。一项持续进行的工作探索在数学背景下将语言模型与交互式证明助手集成。这包括通过策略预测（Polu & Sutskever，2020；Han 等人，2022；Lample 等人，2022；Jiang 等人，2022）、自动形式化（Wu 等人，2022；Jiang 等人，2023）和集成工具（Welleck & Saha，2023）来合成证明。由于搜索的计算成本高昂，应用于该领域的语言模型传统上规模较小，但近期工作展示了使用更大模型的前景（First 等人，2023；Jiang 等人，2023）。我们的工作提供了一个少样本证明自动形式化和策略预测的演示，以及一个大型形式化数学数据集合，并提供了一个开放获取模型，用于进一步探索这些方向。

5 结论

我们介绍了 LLEMMA 和 Proof-Pile-2，这是一种用于数学语言建模的新型基础模型和语料库。我们的模型、数据集和代码均已公开。我们已经证明，LLEMMA 在数学问题解决基准测试上为开放权重模型实现了最先进的结果，展示了通过 Python 代码使用外部工具的能力，并演示了用于定理证明的少样本策略预测。我们希望 LLEMMA 和 Proof-Pile-2 能成为未来工作的有用基础，用于理解语言模型泛化和数据集组成、研究特定领域语言模型的局限性、将语言模型用作数学家的工具，以及提高语言模型的数学能力。

致谢

我们要感谢 Dragomir Radev、Arman Cohan、Jesse Michael Han 和 Deepmind Blueshift 团队提供的宝贵指导。感谢 Jonah Philion 为模型命名。感谢 Aviya Skowron 在我们模型的开发和发布过程中就伦理考量向我们提供建议。感谢 Jonathan Laurent 和 Leo Du 对我们开源代码的贡献。

我们还要感谢为本项目捐赠计算资源的多个方：Stability AI（训练 LLEMMA 模型）、CoreWeave（评估和微调）、安大略省以及赞助向量人工智能研究所的公司（www.vectorinstitute.ai/partners），以及杨百翰大学（微调）。KP 获得了 NSERC PGS-D 奖学金的支持。

参考文献

[此处省略参考文献列表，保持与原文档一致]

A 作者贡献

训练数据。Zhangir Azerbayev, Keiran Paster, Marco Dos Santos, Sean Welleck. 模型训练。Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster. 评估。Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Sean Welleck. 形式化数学评估。Sean Welleck. 记忆化分析。Sean Welleck, Keiran Paster. 资深作者与指导。Jia Deng, Stella Biderman, Sean Welleck.

B 数据：Proof-Pile-2

数据源Token 数权重
Proof-Pile-255B–
代码 (AlgebraicStack)11B1.00
网络 (OpenWebMath)15B4.00
论文 (ArXiv)29B2.00
通用代码 (RedPajama)59B0.22
通用语言 (Pile)300B0.15

表 8：Proof-Pile-2 数据源（顶部），训练期间包含的通用语言和代码数据（底部），以及训练期间各组件的混合权重。

B.1 数学代码：AlgebraicStack

AlgebraicStack 包含大约 11B token 的与数学相关的代码。我们在下面描述其来源、过滤和内容。表 9 显示了 AlgebraicStack 中每种语言的 token 数量。

语言AlgebraicStack token 数语言AlgebraicStack token 数
Agda35.2 MJulia531.0 M
C25.1 MJupyter199.1 M
C++954.1 MLean285.6 M
Coq281.9 MMaple2.0 M
Fortran724.9 MMatlab65.8 M
GAP3.6 MPython6,098.8 M
Haskell9.1 MR71.3 M
Idris10.9 MTex567.7 M
Isabelle1,089.7 M总计10,955.7 M

表 9：AlgebraicStack 中的 token 数，使用 Llama 分词器计算。

B.1.1 GITHUB 代码

以下编程语言在 Stack 中几乎不存在或主要由不正确的文件类型组成，因此我们直接通过 Github Python API 下载了这些语言的数据。

  • Coq：我们过滤具有 .v 扩展名的文件，并通过包含匹配关键词过滤器 "Theorem", "Proof", "Qed", "Inductive", "Definition", "Fixpoint" 的文件来包含 Coq，并通过关键词黑名单 "pragma", "endmodule", "posedge", "negedge", "wire" 排除 Verilog 文件。我们还排除了标注为自动生成的文件。
  • Isabelle：我们过滤具有 .thy 扩展名的文件，并包含匹配关键词白名单 "theorem ", "lemma " 的文件。我们仅保留 isabelle-prover/mirror-afp-devel 并丢弃所有其他旧版本的形式化证明档案（Archive of Formal Proofs）。我们进一步删除了在 PISA（Jiang 等人，2021）测试集中具有定理名称的定理陈述和证明。
  • Lean：我们过滤具有 .lean 扩展名的文件，使用关键词白名单 "theorem ", "lemma ", "example "。我们删除了所有依赖文件，为了避免已知的基准污染，我们将 ProofNet 和 MiniF2F 存储库列入黑名单。我们进一步删除了与 LeanDojo（Yang 等人，2023）验证集或测试集共享定理名称的定理或引理。
  • MATLAB：我们过滤具有 .m 扩展名的文件，使用关键词白名单 "#import", "interface", "implementation", "property"，并通过关键词 "#include" 和正则表达式 r' main\(.*{$' 排除 C 文件。

我们为 Github API 下载实施了截止日期，并使用了 2023 年 4 月 1 日作为截止日期。

对于所有语言，除非另有说明，我们还过滤掉了文件大小大于 1048575 字节或数值密度（数字字符与非数字字符的比率）为 0.5 的文件。我们还通过删除包含与其他文档重叠的 2048 字符块的文档来执行文档级精确去重。

B.1.2 LEAN PROOFSTEPS

我们使用 lean-training-data（Morrison，2023）工具从 Mathlib 4（mathlib Community，2020）中提取了一组（策略状态，下一个策略）对的数据集。我们使用了 Mathlib 4 提交 c779bd5，该提交创建于 2023 年 8 月 20 日。

B.1.3 ISABELLE PROOFSTEPS

我们构建了一个 Isabelle 证明数据集，建立在 PISA 数据集（Jiang 等人，2021）之上。Isabelle Proofsteps 包含来自形式化证明档案和 Isabelle 标准库的证明，由 PISA（Jiang 等人，2021）抓取。数据集中的每个条目都包含定理陈述、证明状态和证明步骤，由特定标签分隔。为了保持使用 PISA 测试集评估的完整性，我们通过删除名称与 PISA 测试集中的定理重叠的定理来对 Isabelle Proofsteps 进行去污染。虽然这种方法导致了严格的过滤——删除了超过 10,000 个定理，尽管 PISA 测试集中只有 3600 个——但我们认为为了减轻数据污染，这是可以接受的。过滤后，Isabelle Proofsteps 包含 251,000 个定理。

B.1.4 STACK 过滤

我们从 Stack（Kocetkov 等人，2022）数据集中获取以下编程语言，并描述了我们选择在默认质量启发式之外减轻的过滤过程和质量问题：

  • Agda：仅应用标准过滤器。
  • C：我们基于关键词白名单包含文档，即："#include <fftw.h>", "#include <fftw3.h>", "#include <rfftw.h>", "#include <gsl", "#include <cblas.h>", "#include <blas.h>", "#include <lapacke.h>", "#include <nlopt.h>", "#include <petsc.h>"。
  • C++：我们基于关键词白名单包含文档，即："#include <adept_arrays.h>", "#include <adept.h>", "#include <alglib", "#include <boost", "#include <armadillo", "#include <blitz", "#include <Eigen", "#include <deal.II", "#include <dlib", "#include <NTL", "#include <mtl"。
  • Fortran：仅应用标准过滤器。
  • GAP：仅应用标准过滤器。
  • Haskell：我们过滤数据，使其仅包含具有以下导入的文件：Numeric.LinearAlgebra, Numeric.SpecFunctions, Numeric.Vector, Statistics, Data.Complex。
  • Idris：仅应用标准过滤器。
  • Julia：我们过滤掉了标记错误的 JSON 行文件。我们删除了长度超过 10,000 个字符且既不是包含测试的文件，数值密度又低于 0.5 的文件，否则忽略数值密度。我们还仅接受特定关键词白名单内的文件，以尝试控制与科学计算的相关性，即："LinearAlgebra", "DifferentialEquations", "Symbolics", "Distributions", "DataFrames", "DynamicalSystems", "Turing", "Gen", "JuMP", "sqrt", "abs", "zeros", "ones", "sin", "cos", "tan", "log", "exp", "integrate", "likelihood", "Matrix", π\pi, "pi", "rand", "grad"。
  • Jupyter：我们发现许多 Jupyter 笔记本文件很大，因为它们包含长单元格输出，例如 base64 图像、长回溯或其他额外的 JSON 单元格元数据。我们使用 nbconvert 将笔记本转换为 markdown 格式，删除元数据。
  • Maple：我们过滤掉了大小超过 100,000 字节的文件，并发现一些文件是 XML。我们过滤掉了所有以 XML 声明开头的文件。
  • Python：我们通过排除以 "{" 字符开头的文档来过滤笔记本和 JSON 文件，并仅包含从固定库列表导入的文件。
  • R：我们排除了所有以 XML 声明开头的文件。我们还过滤掉了所有笔记本，并过滤掉了所有包含 MacOS "Resource Fork" 文件的文件。
  • Tex：我们使用了 10,000,000 字节的最大文件大小。我们排除了在名为 "latex/" 的目录中找到的 tex 文件，因为这些通常是自动生成的文件，并排除了使用 gnuplot 的文档。我们仅包含包含关键词 "\chapter{", "\chapter*{", "\section{", "\section*{", "\subsection{", "\subsection*{", "\subsubsection{", "\subsubsection*{", "\paragraph{", "\subparagraph{" 之一的文档，并额外仅包含被 langid 包中的分类器识别为英语的文档。

对于我们在 Stack 中使用的所有语言，除非另有说明，我们还过滤掉了文件大小大于 1048575 字节或数值密度为 0.5 的文件。

我们使用近去重的 Stack v1.2 作为处理基础。

B.2 论文：ARXIV

我们使用 2023 年 4 月由 Computer (2023) 访问的全部 ArXiv。有关应用于 ArXiv 的预处理的更多信息，请参阅 Computer (2023)。

B.3 网络：OPENWEBMATH

对于我们训练数据集的网络部分，我们使用 OpenWebMath (Paster 等人，2023)。

C 评估工具

我们将各种数学相关任务和评估协议实现到语言模型评估工具（Language Model Evaluation Harness）（Gao 等人，2021）的公共分支中。该工具为语言模型的标准化、可复现评估提供了一个模型无关的框架。

我们为本文的评估添加了以下任务：

  • hendrycks_math_ppl：MATH (Hendrycks 等人，2021a) 子任务的困惑度评估。
  • minif2f_isabelle：基于 Jiang 等人 (2023) 在 miniF2F 基准测试上的 Isabelle 证明自动形式化，带有 Portal-to-Isabelle (Jiang 等人，2021) 证明检查器。
  • minerva_math：带有来自 Minerva (Lewkowycz 等人，2022) 的提示和 Sympy 评估的 MATH 基准测试。
  • minerva-hendrycksTest：遵循 Lewkowycz 等人 (2022) 的 MMLU-STEM 任务。
  • ocw_courses：来自 Lewkowycz 等人 (2022) 的 OCW Courses 任务。
  • python_gsm8k：基于 Gao 等人 (2022) 的带有 Python 的 GSM8k。
  • sympy_math：带有 Sympy 评估的 MATH。

我们在我们的公共代码库中包含了这些任务的实现链接，包括完整的提示。

D 评估：实验细节

D.1 ISABELLE 非正式到形式化定理证明

我们遵循 Jiang 等人 (2023)，允许模型通过生成 sledgehammer 在输出证明中调用内置的 Isabelle 自动化。这会调用 Sledgehammer (Paulson & Nipkow, 2023) 和 Jiang 等人 (2023) 中列出的启发式列表。遵循 Jiang 等人 (2023)，作为基线，我们使用 Sledgehammer 和在证明开始时执行的启发式（为简洁起见，在正文中称为 Sledgehammer）。我们对 Sledgehammer 使用 30 秒超时，并通过 Portal-to-Isabelle (Jiang 等人，2021) 实现证明检查。有关更多详细信息，请参阅评估工具中的实现。

D.2 LEAN 定理证明

通过策略预测进行的定理证明涉及在证明的每一步之后与证明助手交互。在评估工具中实现这些交互超出了本文的范围。因此，对于 Lean 定理证明任务，我们使用基于开源实现（Welleck，2023）的单独评估设置。我们在我们的公共代码库中包含了我们的评估代码。

设置。我们在 miniF2F (Zheng 等人，2021) 上进行评估，该基准测试由来自数学竞赛和本科课程的 488 个形式化陈述组成。给定一个形式化陈述，任务是生成一个由 Lean 检查的形式化证明。

我们使用神经策略预测模型常用的最佳优先搜索（例如 Polu & Sutskever (2020)）。最佳优先搜索由尝试次数 (N)、每次迭代生成的策略 (S) 和最大迭代次数 (T) 参数化。我们将搜索预算定义为生成的策略的最大数量，N×S×TN \times S \times T。我们将搜索预算设置为 N=1,S=32,T=100N=1, S=32, T=100，小于基线模型。遵循 Yang 等人 (2023)，我们使用束搜索生成策略并使用 10 分钟超时。我们适配了 Welleck (2023) 的证明搜索实现，该实现使用 LeanDojo v.1.1.2 (Yang 等人，2023) 进行交互。我们使用 Lean 4 miniF2F，使用 https://github.com/rah4927/lean-dojo-mew 提交 d00c776260c77de7e70125ef0cd119de6c0ff1de。注意，(Yang 等人，2023) 的 ReProver 基线报告了 Lean 3 的性能。

提示。我们使用三个（状态，策略）示例提示模型，如图 5 所示。

图 5：Lean 定理证明实验的提示。

E 数据表

我们按照 Gebru 等人 (2021) 的框架为 Proof-Pile-2 提供数据表。

[此处省略数据表内容，保持与原文档一致]

F 附加结果

F.1 证明自动形式化

表 11 显示了关于 Isabelle 证明自动形式化的附加结果，包括 Sledgehammer 和给定语言模型所关闭的定理的并集。

方法自动形式化 pass@1 miniF2F-valid*miniF2F-test
Sledgehammer14.72%20.49%
Code Llama 7b16.31%17.62%
LLEMMA-7b20.60%22.13%
Code Llama 7b ∪ Sledgehammer20.17%25.00%
LLEMMA-7b ∪ Sledgehammer25.97%27.46%

表 11：Isabelle 自动形式化。*我们排除了少样本提示中使用的 11 个示例。Pass@1 使用贪婪解码。

G 监督微调

对 LLEMMA 的微调应用（例如指令遵循（Ouyang 等人，2022；Wei 等人，2022）、对话建模（Thoppilan 等人，2022；Touvron 等人，2023；Collins 等人，2023）和奖励建模（Cobbe 等人，2021；Lightman 等人，2023））的全面探索超出了本文的范围。然而，为了确定 LLEMMA 在微调时是否保持了相对于其他开放模型的优势，我们对 LLEMMA-7B 在 MetaMathQA（Yu 等人，2023）上进行了初步实验，这是一个针对 MATH 和 GSM8k 基准测试的监督数据集。结果如表 12 所示。

初始化微调数据集MATHGSM8k
Llama 2 7BWizardMath (专有)10.7%54.9%
Llama 2 7BMetaMathQA19.4%66.4%
LLEMMA 7BMetaMathQA25.2%66.5%
Llama 2 70BWizardMath (专有)22.7%81.6%
Llama 2 70BMetaMathQA26.6%82.3%

表 12：各种 7B 基础模型在监督数学数据集上的微调。所有使用 Llama 2 初始化的结果均复制自文献（Luo 等人，2023；Yu 等人，2023）。LLEMMA 7B 微调模型使用与 Yu 等人 (2023) 中的模型相同的超参数进行训练。

H 定性示例

数据集重叠。图 6 显示了检查与 OpenWebMath 文档的 nn-gram 重叠时各种 nn 的示例假阳性。图 7 显示了一个与 MATH 问题有 30-gram 重叠的 OpenWebMath 文档，以及 LLEMMA-7b 的生成解决方案。

任务输出。图 8 显示了非正式到形式化定理证明任务中的生成证明。

[此处省略图 6、7、8 的内容，保持与原文档一致]

硬核测试

正确率：0 / 5
1

LLEMMA 模型是通过在哪个数据集上对 Code Llama 进行持续预训练而得到的？

2

关于 LLEMMA 与 Minerva 模型的对比，下列说法正确的是？

3

AlgebraicStack 数据集的主要用途是什么？

4

在训练 LLEMMA 7B 模型时，作者对 Code Llama 的 RoPE 基周期做了什么调整？

5

根据论文，LLEMMA 在 MATH 基准测试中的表现如何？