这是一款名为 Llemma 的开源语言模型，该模型是为数学设计的。
Llemma 模型是在自定义数据集上进行训练的，数据集由从网络上各种来源抓取的数学论文和文本组成。
在数学语料库上持续预训练后，开放语言模型提高了形式定理证明任务的小样本性能。
特点：
- Llemma能正确解决高中或奥林匹克级别数学问题。
- 与 COPRA 和 Proverbot9001 等其他模型相比，它在 Lean 和 Coq 等系统中解决数学证明的能力。
- 虽然 Llemma 在一个数据集上比 COPRA 提高了 3%，但 Proverbot9001 等其他模型估计在其他数据集上解决了大约 10-15% 的证明问题。
- Llemma 被认为对正式证明生成之外的任务具有潜在用途，例如提供提示、在正式和非正式证明之间进行转换或总结参考文献
详细点击标题
我们提出了 Llemma，一种大型数学语言模型。我们继续在 Proof-Pile-2 上对 Code Llama 进行预训练，Proof-Pile-2 是科学论文、包含数学的网络数据和数学代码的混合物，产生 Llemma。
在 MATH 基准上，Llemma 的性能优于所有已知的开放基础模型，以及在等参数基础上未发布的 Minerva 模型套件。
此外，Llemma 能够进行工具使用和形式定理证明，无需任何进一步的微调。我们公开发布所有工件，包括 70 亿和 340 亿个参数模型、Proof-Pile-2 以及复制我们实验的代码。
Llemma 能够进行工具使用和形式定理证明，无需任何进一步的微调。我们公开发布所有工件，包括 70 亿和 340 亿个参数模型、Proof-Pile-2 以及复制我们实验的代码。