May, 2022

神经定理证明的超树式证明搜索

PDF
TL;DR我们提出了一种基于 Transformer 的自动定理证明器的在线训练过程，并使用 AlphaZero 的新型搜索算法 HTPS。我们通过在线训练从以前的证明搜索中学习，使其可以概括到远离训练分布的域。通过研究逐渐复杂的三个环境的性能，我们报告了我们管道主要组件的详细消除。我们证明，在仅使用 HTPS 的情况下，一个在注释证明上训练的模型可以证明 65.4% 的 Metamath 定理的保留集，显著优于 GPT-f 的 56.5% 的先前技术水平。这些未经证明的定理的在线训练将准确性提高到 82.6％。在类似的计算预算下，我们将对 Lean-based miniF2F-curriculum 数据集的技术水平从 31％提高到 42％的证明准确性。
发现论文，激发创造
  • 用于自动定理证明的生成语言建模

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

    Sep, 2020

  • 面向大规模神经定理证明

    提出了一种新型的神经定理证明器，通过仅考虑最高证明分数相关的证明路径，可以在以前无法应用的知识库上进行推理和学习。

    Jul, 2018

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

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

    Dec, 2023

  • 深度网络引导的证明搜索

    利用深度学习技术来辅助自动的定理证明，通过对 Mizar 库的证明进行数据训练和选择处理，改进 ATP 的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。

    Jan, 2017

  • Magnushammer: 基于 Transformer 的前提选择方法

    本文介绍了一个基于神经变换器的自动定理证明方法 Magnushammer，使用 PISA 基准测试，证明率达到 59.5％，超过了目前最成熟和最流行的基于符号的求解器 Sledgehammer 的 38.3％，并通过与基于语言模型的神经形式证明器相结合，将先前的最先进证明率从 57.0％提高到 71.0％。

    Mar, 2023

  • Holophrasm：用于高阶逻辑的神经自动定理证明器

    使用深度学习自动证明定理的系统 Holophrasm，利用 Metamath 语言的形式化逻辑和神经网络增强的贪心算法，以及序列到序列模型进行行动枚举，可以证明 Metamath's set.mm 模块中 14% 的测试定理。

    Aug, 2016

  • 学习生成定理以证明定理

    为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了 Metamath 自动定理证明的发展。

    Feb, 2020

  • 数学游戏

    Holophrasm 是使用 MCTS 和神经网络进行策略和评估的神经定理证明器，本文旨在通过其他游戏树搜索算法提高 Holophrasm 定理证明器的性能。

    Sep, 2023

  • 端到端可导证明中学习推理策略

    本文提出了一种名为 Conditional Theorem Provers（CTPs）的方法，它是 Neural Theorem Provers（NTPs）的扩展，可以通过基于梯度的优化学习出最优规则选择策略以实现可解释性和可扩展性，并且在大规模任务中表现优异。CTPs 在 CLUTRR 数据集上取得了表现最优结果，并在标准基准测试中展现了比其他神经符号模型更好的链接预测结果。

    Jul, 2020

  • 使用验证器引导搜索生成自然语言证明

    本文介绍了一种新的逐步方法 NLProofS，通过在给定假设的条件下学习生成相关步骤，从而在 NLP 中解决证明生成的问题，并在 EntailmentBank 上取得了最先进的性能。

    May, 2022