开源LLEMMA发布：超越未公开的顶尖模型，可直接应用于工具和定理证明

深度学习自然语言处理原创
作者：Winnie

今天向大家介绍一个新的开源大语言模型——LLEMMA，这是一个专为数学研究而设计的前沿语言模型。

LLEMMA解数学题的一个示例

LLEMMA的诞生源于在Proof-Pile-2数据集上对Code Llama模型的深度训练。这个数据集是一个科学论文、数学相关网页和数学代码的综合体。

过去虽然有数学专用的模型，但许多模型都有各种限制。例如，有的模型是封闭访问，这使得它们无法为更广泛的研究所用。有的则技术上稍显落后。

但LLEMMA的出现改变了这一局面。它不仅在MATH基准测试上创下了新高，甚至超越了某些还未对外公开的顶尖模型，如Minerva。更让人欣喜的是，LLEMMA无需额外的调整，即可直接应用于工具和定理证明。

让我们一起了解下这个模型背后的技术吧！

Paper: Llemma: An Open Language Model For Mathematics
Link: https://arxiv.org/pdf/2310.10631.pdf
Code: https://github.com/EleutherAI/math-lm

->辅导界的小米带你冲刺ACL2024

数据集

LLEMMA是专为数学设计的大型语言模型，具有70亿和340亿参数。这一模型的训练方法是在Proof-Pile-2.2.1数据集上继续对Code Llama模型进行预训练。以下是关于该数据集的简要说明：

Proof-Pile-2：这是一个包含550亿令牌的综合数据集，融合了科学论文、数学相关的网络内容和数学代码，其知识截止于2023年4月（不包括特定的Lean证明步骤子集）。
代码：为了适应数学家日益重视的计算工具，如数值模拟和计算代数系统，研究团队创建了名为AlgebraicStack的源代码数据集。这个数据集涉及17种编程语言，包括数值、符号和正式的数学内容，共计110亿令牌。
网络数据：研究团队利用了OpenWebMath数据集，这是一个精选的、与数学相关的高质量网络页面集合，总计150亿令牌。
科学论文：使用了名为RedPajama的ArXiv子集，其中包含290亿令牌。
通用自然语言和代码数据：作为训练数据的补充，研究团队还融合了一些通用领域的数据，并以Proof-Pile-2为主，还融合了Pile数据集和RedPajama的GitHub子集。

模型训练

模型初始化：所有模型都从Code Llama初始化，随后在Proof-Pile-2上接受更多的训练。

训练量：

LLEMMA 7B：2000亿令牌的训练。
LLEMMA 34B：500亿令牌的训练。

训练工具和硬件：使用GPT-NeoX库在256个A100 40GB GPU上进行训练。使用了各种先进技术如Tensor并行、ZeRO Stage 1分片优化器状态、Flash Attention 2等以提高效率和减少内存需求。

训练细节：

LLEMMA 7B：经过42,000步训练，每个全局批次有400万令牌，上下文长度为4096令牌，占用A100大约23,000小时。学习率开始从1 × 10^(-4)渐温，然后逐渐减少。虽然计划是48,000步训练，但在42,000步时由于NaN损失中断了。
LLEMMA 34B：经过12,000步训练，每个全局批次有400万令牌，上下文长度为4096令牌，约占用47,000个A100小时。学习率从5 × 10^(-5)开始逐渐增加，然后逐渐减少。
RoPE调整：在训练LLEMMA 7B前，RoPE的基本周期从θ = 1,000,000减少到θ = 10,000，目的是为了在LLEMMA 7B上进行长上下文微调。而LLEMMA 34B维持了θ = 1,000,000的原始设置。

实验设置与评估结果

作者通过少样本评估对LLEMMA模型进行比较，并专注于没有进行微调的最新模型。具体来说，他们使用了使用思维链推理和多数投票，在MATH和GSM8k等基准上进行了评估。

评估范围：

数学问题求解：测试模型在思维链推理和多数投票的数学问题上的表现。
少样本工具使用和正式定理证明：研究模型在这些方面的表现。
记忆和数据混合的影响：分析这些因素如何影响模型的表现。

使用CoT解决数学任务

评估数据集和任务：

MATH：一个来自高中数学竞赛的问题集，模型必须生成一个LATEX的解决方案，且其答案需要与参考答案匹配。
GSM8k：包含中学数学问题的数据集。
OCWCourses：从MIT的开放课程Ware提取的STEM问题。
MMLU-STEM：MMLU基准中的18个子集，涵盖57个主题。
SAT：包含2023年5月的SAT考试中不包含图形的数学问题的数据集。

作者与以下模型进行了比较：

Minerva：这个模型在技术内容的数据集上继续预训练了PaLM语言模型。
Code Llama：LLEMMA继续预训练的初始化模型。
Llama 2：Code Llama在代码上继续预训练的初始化模型。

对于开源的模型，作者使用他们的评估套件来报告分数，该套件是Language Model Evaluation Harness的一个分支。对于Minerva模型，作者报告了Lewkowycz等人在2022年文章中的基准分数。

LLEMMA在Proof-Pile-2上的继续预训练提高了五个数学基准测试的少样本性能。LLEMMA 34B在GSM8k上比Code Llama提高了20个百分点，在MATH上提高了13个百分点；LLEMMA 7B的表现超过了专有的Minerva模型。到目前为止，LLEMMA在所有开放权重语言模型上均表现最佳。因此，可以得出结论，Proof-Pile-2上的继续预训练对于提高预训练模型的数学问题解决能力是有效的。

此外，LLEMMA是在与数学相关的多样化数据上预训练的，而不是为特定任务进行调优。因此，预期LLEMMA可以通过任务特定的微调和少样本提示适应许多其他任务。

调用计算工具解决数学任务

这些任务涉及在有计算工具的情况下解决问题，主要评估了以下内容：

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

如下表所示，LLEMMA在两个任务上都优于Code Llama。它在MATH和GSM8k上使用工具的性能也高于它在没有工具的这些数据集上的性能。