May, 2022

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

PDF
TL;DR通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。
theorem provingnatural languagegenerative modelsmathematical proofnaturalprover
发现论文，激发创造
  • 自然证明：自然语言数学定理证明

    NaturalProofs 是一个使用自然数学语言编写数学命题和证明的多域语料库，可用于评估系统在数学参考检索和生成任务中确定证明中出现的关键结果的能力，并提供了许多研究理解和创建自然数学语言的挑战性数学任务的新途径。

    Mar, 2021

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

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

    Sep, 2020

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

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

    May, 2022

  • LangPro: 自然语言定理证明器

    LangPro 是一种自然语言自动证明器，使用基于专门设计的自然逻辑的分析表格方法，能够推导出前提和假设之间的语义关系，并在 FraCaS 和 SICK 文本蕴含数据集上达到了可与最先进技术相媲美的高结果。

    Aug, 2017

  • ProoFVer: 用于事实验证的自然逻辑定理证明系统

    该论文提出 ProoFVer，使用 seq2seq 模型生成自然逻辑推理作为证明，以此决定索赔真实性，它拥有最高的标签准确性和第二优秀的 FEVER 排行榜得分，证明了它的鲁棒性。

    Aug, 2021

  • 利用自然语言处理进行数学归纳证明的自动评分

    数学证明教育的关键词包括准时反馈、自然语言处理、自动分级自由形式数学证明、用户研究。

    Jun, 2024

  • PRover: 可解释推理的证明生成系统

    我们提出了 PROVER，一种可解释的 transform-based 模型，能够同时回答基于规则的二元问题并生成相应的证明，经过实验表明，在 QA 任务中，PROVER 的证明生成精度为 87％，而在零 - shot 评估中，与 RuleTakers 相比，在 QA 任务中的表现得到保留或提高（最多提高 6％）；并在更深层次上（最多提高 15％）更好地泛化，仅使用 40％的训练数据即可获得近乎完美的 QA 准确性，但对于需要更深入推理的问题，证明生成变得具有挑战性，准确性下降到 65％，这表明未来仍有大量研究价值。

    Oct, 2020

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

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

    Feb, 2020

  • ProofWriter: 对自然语言生成蕴含、证明和阿布达布意见的系统

    这篇论文展示了一个名为 ProofWriter 的生成模型，能够可靠地生成一个理论的两个蕴含和支持它们的自然语言证明，具有高精度的缺少检测性能，能够大幅提高神经方法用于自然语言推理的可行性。

    Dec, 2020

  • LEGO 证明器：具有增长库的神经定理证明

    LEGO-Prover 使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。

    Oct, 2023