可以证明数学定理的AI大模型：LLEMMA（开源）

数学是一门基于严格的逻辑和证明的学科，它要求对概念和结构有清晰和精确的定义和理解。AI则是一门基于数据和统计的学科，它要求对现象和规律有有效和近似的描述和预测。

这两者之间存在着一定的差异，那么AI真的无法应用数学吗？

很多人不相信，所以有这么一个团队推出了针对数学领域的AI大模型：LLEMMA

LLEMMA是什么？

LLEMMA是一个由EleutherAI团队开发的大型语言模型，专门用于数学领域。

它是在Code Llama的基础上继续预训练的，使用了Proof-Pile-2这个包含了科学论文、网页数据和数学代码的混合数据集。

LLEMMA在MATH基准测试中超越了所有已知的开放的基础模型，以及未发布的Minerva模型套件（在相同参数数量的情况下）。

而且，LLEMMA还能够使用计算器、计算机代数系统和形式定理证明器等工具来解决问题，而不需要任何进一步的微调。

下面是一个针对 MATH 基准问题的 Llemma 34B 解决方案：

LLEMMA项目的亮点是，它将所有的模型、数据和代码都开源了，让任何人都可以下载、使用和改进。LLEMMA有7亿和34亿参数的两个版本，分别占用约2.5GB和12GB的内存空间。

它们可以在个人电脑上运行，不需要联网或者使用云服务。这意味着你可以随时随地和LLEMMA进行数学对话，无论是出于学习、研究还是娱乐的目的。

开源代码地址：

https://github.com/EleutherAI/math-lm

https://blog.eleuther.ai/llemma/

论文地址:

https://arxiv.org/abs/2310.10631