Apr, 2020

自然语言前提选择：寻找数学文本的支持陈述

PDF
TL;DR本文提出了自然前提选择 (Natural Premise Selection) 这一新型自然语言处理 (NLP) 任务，以便找到能为生成某个语句非正式数学证明提供支持定义和支持命题的前提；此外，我们还提供了一个数据集 NL-PS，用于评估不同方法在此任务上的表现，并使用不同的基线模型来展示了该任务所涉及的基本解释挑战。
mathematical textnlpnatural premise selectiondatasetinterpretation challenges
发现论文，激发创造
  • 利用语料库分析和核方法进行数学前提选择

    本论文提出了基于机器学习的前提选择方法，通过构建依赖关系知识库并提出核方法的前提选择算法，在大型数学理论证明中实现了 50％的性能提升。

    Aug, 2011

  • 通过语句组合搜索进行自然语言推理

    本文提出了一种基于自然语言的演绎推理系统，通过将任务分解为逐步协调的步骤，并由搜索程序生成中间结论的树，可以成功地证明真实的语句并拒绝虚假的语句。

    Jan, 2022

  • 自然证明：自然语言数学定理证明

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

    Mar, 2021

  • 多前提自然语言推理

    该论文定义了一项新的文本蕴含任务，要求对多个前提句子进行推断，提出了一个新的数据集来最小化平凡的词汇推理，强调对日常事件的知识，并为文本蕴含提出了一个更具挑战性的环境；同时评估了多种强力神经网络基线，并分析多个前提任务与标准文本含义的区别。

    Oct, 2017

  • DeepMath - 前提选择的深度序列模型

    本研究使用神经序列模型探讨在自动定理证明的命题选择方面的有效性，提出了一个两级方法，能够在避免现有最先进模型的手工设计功能的同时在 Mizar 语料库上为 premise selection 任务提供良好结果。据我们所知，这是首次在大规模的定理证明中应用深度学习。

    Jun, 2016

  • 自然语言推理的灵活生成

    本研究提出了 ParaPattern，该方法利用自动化流程从维基百科生成训练数据，并使用 BART 模型在无直接人类监督下从多样的自然语言输入中生成演绎推理，结果表明，ParaPattern 模型在无领域训练数据的情况下，表现优于基线系统。

    Apr, 2021

  • 自然语言推断与不完整信息

    提出了一个处理模糊的假设的新系统，使用自然语言生成模型来从一个前提中推出另一个前提并以双向的方式搜索。 使用回路验证程序过滤质量不佳的生成来确保正确性。 该系统在修改后的 EntailmentBank 数据集和名为 “Everyday Norms：Why Not?“的新数据集上表现出可以恢复跨领域和非领域的前提的能力。

    Nov, 2022

  • 通过深度图嵌入进行定理证明的前提选择

    该研究使用基于深度学习的方法，提出了一个新的思路来选择与证明相应的数学陈述。应用了一种新的嵌入方法，将高阶逻辑公式表示为一个不变于变量重命名的图，并在保留语法和语义信息的同时，全面地将图形嵌入到一个向量中，从而在 HolStep 数据集上实现了优异的分类表现，将分类准确度从 83％ 提高到了 90.3％。

    Sep, 2017

  • 具有不完整信息的自然语言推断

    通过混合演绎（前向）和择优推断（后向）生成步骤进行阴性推断，以验证其他假设的缺失证据，避免致信任错误。

    Jul, 2023

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

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

    May, 2022