EMNLPOct, 2023

TRIGO：用于生成语言模型的形式化数学证明简化的基准测试

PDF
TL;DR我们提出了 TRIGO，一个自动定理证明基准测试，要求模型能够逐步证明简化三角表达式，并评估生成型语言模型在公式推理、数字项操作、分组和因式分解方面的推理能力。我们从互联网收集三角表达式及其简化形式，并用 ``Lean'' 形式语言系统注释简化过程，然后自动从标注样本中生成额外的示例来扩充数据集。通过基于 Lean-Gym 的自动生成器创建不同难度和分布的数据集来全面分析模型的泛化能力。我们的广泛实验显示，TRIGO 对于包括在大量开源形式定理证明语言数据上预训练的 GPT-4 在内的先进生成型语言模型提出了新的挑战，并为研究生成型语言模型在形式和数学推理上的能力提供了新工具。
automated theorem provingtrigotrigonometric expressionsgenerative language modelsreasoning ability
发现论文，激发创造
  • ATG：基于生成式语言模型的自动定理生成基准测试

    自动生成定理是一个挑战，本文提出了一个基于自动化定理生成（ATG）的评估基准，以探究当前生成性语言模型（LMs）在生成新定理和可重复定理方面的能力，结果表明当前 LMs 仍有改进空间。

    May, 2024

  • 用于自动定理证明的生成语言建模

    本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。

    Sep, 2020

  • 不要相信：验证 - 用自动形式化证明 LLM 定量推理的基础

    通过自动生成验证的形式化 Isabelle 代码，我们的方法能够自动排除具有内在一致性问题或与形式化问题陈述不一致的解，并在多个数据集和模型大小上比以前最佳方法 — 普通多数投票 — 提高了 12% 以上的准确性。

    Mar, 2024

  • 自然证明器：基于语言模型的数学证明生成

    通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

    May, 2022

  • 学习证明三角恒等式

    本文提出了基于深度学习的自动证明系统 AutoTrig，用于解决三角函数恒等式的自动证明问题，通过逐步优化，AutoTrig 在最短步骤内完成证明且不输于现有方法。

    Jul, 2022

  • DeepSeek-Prover: 通过大规模合成数据推进 LLMs 中的定理证明

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

    May, 2024

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

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

    Jul, 2024

  • MathGenie: 利用问题逆向翻译生成合成数据以提升 LLMs 的数学推理能力

    MathGenie 是一种从小规模的问题解决数据集（称为种子数据）生成多样且可靠的数学问题的新方法，通过增加种子数据的真实解决方案，并训练一个回译模型将增加的解决方案翻译回新问题，从而产生与代码集成的问题解决方案，进而提供理性基础验证策略，该方法通过对新收集的数据训练从 7B 到 70B 范围的预训练模型，形成了 MathGenieLM 系列模型，这些模型在五个代表性数学推理数据集上始终优于以前的开放源语言模型，达到了最新的性能水平，尤其是 MathGenieLM-InternLM2 在 GSM8K 上达到了 87.7％的准确率，在 MATH 上达到了 55.7％的准确率，获得了开放源语言模型的最佳综合得分。

    Feb, 2024

  • EvoGPT-f: 用于基准测试形式数学语言的进化 GPT 框架

    这篇论文通过 EvoGPT-f 回答了关于五种形式数学语言（Lean 3、Lean 4、Coq、HOL 4、HOL Light）和四种标记化方法（字符、词级、字节对编码和 StarCoder 标记器）之间的差异化机器学习能力的定量分析，为进一步开展社区间系统定量和定性比较研究奠定了基础。

    Feb, 2024

  • Lean4 中自动形式化的评估基准

    大型语言模型 (LLMs) 具有彻底改变自动形式化的潜力。引入数学编程语言 Lean4 为评估 LLMs 的自动形式化能力提供了前所未有的机会。本文介绍了一种专为 Lean4 设计的新型评估基准，将其应用于测试包括 GPT-3.5、GPT-4 和 Gemini Pro 在内的最先进的 LLMs 的能力。我们全面的分析发现，尽管最近有所进展，这些 LLMs 在自动形式化方面仍存在局限性，尤其是在更复杂的数学领域。这些发现强调了需要进一步发展 LLMs，以充分发挥它们在科学研究和开发中的潜力。本研究不仅为当前的 LLM 能力设立了基准，还为自动形式化的未来增强奠定了基础。

    Jun, 2024