01
项目介绍
LLEMMA：一个专门解决数学问题的开源大语言模型，能力超过所有已知的开源模型 LLEMMA由多个大学和Eleuther AI公司共同研发，模型能够理解和生成数学表达式、解决数学问题，并与其他计算工具（如Python解释器和形式定理证明器）进行交互。
该模型基于Code Llama进行构建，在多个数学问题解决基准测试上，LLEMMA都表现出色，超过了所有已知的开放基础模型。LLEMMA模型是在Proof-Pile-2（一个包含550亿标记的数学和科学文档数据集）上进行预训练的，该数据集包括科学论文、与数学相关的网页数据和数学代码。
LLEMMA训练并发布了两个模型：Llemma 34B和Llemma 7B。LLEMMA 7B模型在200B个令牌上进行了训练，而LLEMMA 34B模型在50B个令牌上进行了训练。
LEMMA主要针对以下几类数学问题：
代数问题：如解方程、因式分解等。
微积分问题：如求导、积分等。
几何问题：如计算面积、体积等。
离散数学问题：如图论、组合数学等。
统计与概率问题：如概率分布、统计推断等。
02
项目实测
在数学基准测试（MATH benchmark）上，LLEMMA模型表现出色，超过了所有已知的开放基础模型。具体来说，它在MATH基准测试上的得分是0.87，而其他模型（如Minerva）的得分通常在0.7-0.8之间。
Llemma在链式思维数学（Chain-of-Thought Math）上的表现出色：Llemma在链式思维数学推理方面表现出色。这种推理方式要求模型能够跟踪和理解一个问题的多个步骤，并能够在每一步中应用前一步的结果。这是数学和逻辑推理中非常关键的一个方面。
在具体的数学问题解决中，Llemma能够：
识别问题的关键部分：Llemma模型能够准确地识别出问题中的关键变量和条件。
逐步解决问题：模型按照逻辑顺序，一步步地解决问题。
保持上下文：在解决多步骤问题时，模型能够保持对前面步骤的记忆，以便在后续步骤中使用。
生成证明：对于需要证明的数学定理或命题，模型能够生成逻辑严密的证明。
集成其他计算工具
Llemma模型还可以使用计算工具来解决问题，如计算器、计算机代数系统和形式定理证明器。它可以通过API或其他接口与这些计算工具进行交互。例如，当模型需要进行复杂的数学计算时，它可以调用Python解释器来执行这些计算。同样，当需要进行形式化证明时，它可以利用形式定理证明器来完成。这意味着模型不仅能够进行高级的数学推理，还能执行复杂的数学运算和证明。
03
应用场景
自动化证明：在数学或计算机科学领域，LLEMMA能够自动生成形式化证明，并通过形式定理证明器进行验证。
数据分析和统计计算：LLEMMA能够利用Python解释器进行高级数据分析，包括但不限于回归分析和时间序列分析。
符号计算：LLEMMA也能处理需要符号计算的问题，如解析解和积分，通过与计算工具的集成来实现。
详细介绍：https://blog.eleuther.ai/llemma/
