Feb, 2024

统一合成定理与证明数据的 MUSTARD 方法

PDF
TL;DR该研究论文提出了 MUSTARD，一个数据生成框架，通过三个步骤合成高质量和多样化的定理和证明数据，用于理解大型语言模型在数学推理和定理证明方面的能力。利用 MUSTARD 生成的数据进行 Fine-tuning，可以在自动定理证明和数学问题求解中获得显著的性能提升。
large language modelsmathematical reasoningtheorem provingdata generation frameworkautomated theorem proving
发现论文，激发创造
  • DeepSeek-Prover: 通过大规模合成数据推进 LLMs 中的定理证明

    基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

    May, 2024

  • 通过数据增强和动态采样方法提升神经定理证明

    DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 ProofNet 两个标准数据集上实现了显著的性能提升。

    Dec, 2023

  • 使用合成数据探索大型语言模型的数学外推

    通过对高质量合成数据的微调，本文通过提出的算术难题问题展示出大型语言模型在多步推理任务上的出色表现，并通过开源的 3B 模型在三个不同的测试数据集上实验结果表明，这种模型不仅在域内数据集上能够达到 0.44 的零样本一次通过率 @1，而且还在域外数据集上展现出一定的泛化能力，对于扩展数字范围和算术难题问题的组合组件分别设计了两个域外数据集，在这两个更难的任务上，经过微调的模型展示出令人鼓舞的表现，零样本一次通过率 @1 分别为 0.33 和 0.35。

    Jun, 2024

  • 增强形式定理证明：一个用于训练 Coq 代码 AI 模型的综合数据集

    该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成 Coq 代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个 Coq 源代码文件，初步实验表明使用该数据集训练的模型在 Coq 代码生成方面具有显著的潜力。

    Mar, 2024

  • 数学牧人：一种无需标签的逐步验证器，用于数学推理中的 LLMs

    Math-Shepherd 是一种创新的过程导向数学验证器，使用自动生成的过程级监督数据进行训练，通过对 LLM 的输出逐步赋予奖励分数来解决复杂多步骤数学问题，指导一系列开源 LLMs 取得了非凡的性能，并在自洽性方法和其他验证模型方面表现优异，我们相信自动过程监督对 LLM 的未来演进具有重要潜力。

    Dec, 2023

  • 精益练习册：从自然语言数学问题转化而成的大规模精益问题集

    通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。

    Jun, 2024

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

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

    May, 2024

  • TheoremLlama: 通用 LLM 转换为 Lean4 专家

    使用 Lean 等计算机可验证形式语言来证明数学定理具有重大影响，本文提出了 TheoremLlama 框架，通过生成对齐的数据集和训练方法，使大型语言模型成为 Lean4 专家，实现了高于 GPT-4 基准的累积准确率。

    Jul, 2024

  • 借鉴失败：使用试错数据对直觉命题逻辑证明进行微调的 LLM

    通过从失败的搜索路径中学习，我们展示了训练模型的益处。我们与仅使用正确路径训练的模型进行比较，并发现前者以更少的搜索次数解决了更多未见过的定理。

    Apr, 2024

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

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

    Nov, 2023