Oct, 2023

Llemma: 数学领域的开放语言模型

PDF
TL;DR我们提出了 Llemma 这个大型数学语言模型，通过将 Code Llama 进行预训练得到了 Llemma，并在 MATH 基准测试中表现优于所有已知的开源基础模型，同时还能进行工具使用和形式定理证明而无需进一步微调。
llemmalanguage modelmathematicspretrainingproof-pile
发现论文，激发创造
  • LLaMA：开放高效的基础语言模型

    介绍了 LLaMA，包含 7B 至 65B 个参数的基础语言模型，使用公开可用的数据集训练，其中 LLaMA-13B 在大多数基准测试中优于 GPT-3（175B），LLaMA-65B 等模型与最佳模型 Chinchilla-70B 和 PaLM-540B 相竞争。

    Feb, 2023

  • InternLM-Math: 面向可验证推理的开放数学大语言模型

    我们介绍并开源了我们的数学推理 LLMs InternLM-Math，它是从 InternLM2 继续预训练的，将序列到序列格式中的思维链推理、奖励建模、形式推理、数据增强和代码解释器统一起来，监督我们的模型成为一个多功能的数学推理者、验证者、证明者和扩充器。我们的预训练模型在各种非正式和正式基准测试中，包括 GSM8K、MATH、匈牙利数学考试、MathBench-ZH 和 MiniF2F，在即时学习、监督微调和代码辅助推理的环境设置下，取得了最先进的性能，MiniF2F 测试集上实现了 30.3 的成绩。我们进一步探索了如何使用 LEAN 解决数学问题，并研究了在多任务学习的环境设置下的性能，这表明了使用 LEAN 作为数学问题求解和证明的统一平台的可能性。我们的模型、代码和数据已在 https://github.com/InternLM/InternLM-Math 上发布。

    Feb, 2024

  • Mathify: 在数学问题求解任务上评估大型语言模型

    自然语言处理和大型语言模型在教育和指导方法领域取得了快速进展，特别在解决数学问题的应用方面，其中 MAmmoTH-13B 表现出了最高的能力水平，成为解决 NCERT 数学问题的可靠基准。

    Apr, 2024

  • VerityMath: 自校验实现的数学推理与单位一致性的推动

    通过定义单位并确保在数学运算过程中单位的一致性，我们提出了一种系统的方法来解决大规模语言模型在解决涉及跨多种类型或单位的数量的数学问题时面临的挑战。我们使用 Unit Consistency Programs（UCPs）为每个问题开发了一个带有单位规范和单位验证程序的数据集，并借助 UCPs 对 Code Llama（7B）模型进行了微调，从而产生了 VerityMath，并展示了我们的初步研究结果。

    Nov, 2023

  • 利用学习的符号抽象启动高水平数学推理

    该研究提出了一种名为学习数学抽象（LEMMA）算法，该算法可以通过引入抽象步骤来增强专家迭代，并利用层次化抽象的思想来帮助强化学习代理人解决数学问题，实验结果表明该算法可以有效提高已有代理人的解决问题能力和泛化能力。

    Nov, 2022

  • MuMath-Code：结合多角度数据增强的数学推理工具使用大型语言模型

    我们提出了一种结合外部工具和数据增强的方法，并采用两阶段的训练策略，以实现数学推理能力的增强。经过大量实验证明，我们的方法在数学推理任务上取得了新的最佳性能。

    May, 2024

  • 元数学：为大型语言模型建立自己的数学问题

    我们提出了一个名为 MetaMath 的精细调整的语言模型，专注于数学推理，实验证明 MetaMath 在数学推理方面表现优于开源语言模型。

    Sep, 2023

  • WizardMath：通过增强进化教学赋能大型语言模型的数学推理

    通过应用 RLEIF 方法于数学领域，我们提出了 WizardMath 以增强 Llama-2 的数学推理能力，实验证明我们的模型在 GSM8k 和 MATH 等数学推理评估上远超其他开源 LLMs，甚至胜过了 ChatGPT-3.5 等模型。

    Aug, 2023

  • 利用大型语言模型实现数学形式化辅助工具

    本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。

    Nov, 2022

  • TinyLlama：一种开源的小型语言模型

    TinyLlama 是一个小型预训练语言模型，通过利用开源社区的先进技术（如 FlashAttention）提高计算效率，在一系列下游任务中表现出色，超过了同规模的现有开源语言模型。

    Jan, 2024