Sep, 2017

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

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

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

    Jun, 2016

  • 将符号知识嵌入深度网络

    本文提出了一种基于图嵌入网络的符号知识应用方法，该方法将命题公式 (和赋值) 通过增强的 Graph Convolutional Network (GCN) 投射到流形上。通过识别节点异质性和结构约束等技术，我们能够生成语义上忠实的嵌入，提高推理检查和视觉关系预测模型的性能。有趣的是，我们观察到命题理论表示的可处理性与嵌入的易用性之间存在一种联系。

    Sep, 2019

  • 使用子图汇集技术提升图神经网络对逻辑公式的表达

    本研究通过开发一种新型的嵌入逻辑公式的结构感知神经网络架构，成功地解决了图形化方法在逻辑公式表示时的局限性，并在两个标准数据集上进行了实证研究，取得了最先进的性能，为深度学习与自动定理证明的融合提供了新的思路。

    Nov, 2019

  • 利用语料库分析和核方法进行数学前提选择

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

    Aug, 2011

  • 深度学习在定理证明中的调查

    该论文提供了一项深度学习在定理证明中的全面调研，包括现有方法的综述、数据集和策略的详细总结、评估指标和最先进技术的性能分析，以及未来研究的挑战和发展方向的批判性讨论。该调研旨在成为深度学习在定理证明中的基础参考，促进这个迅速发展领域的进一步研究。

    Apr, 2024

  • 高阶逻辑和定理证明的图表示

    本文首次使用图神经网络 (GNNs) 实现高阶证明搜索，并证明 GNNs 能够提高此领域的最新成果。我们考虑了高阶逻辑的几种图形表示，并将它们与 HOList 基准进行了评估。

    May, 2019

  • 在知识图谱上嵌入逻辑查询

    本研究提出了一种基于低维嵌入空间中的几何运算来有效处理知识图谱中逻辑查询的框架，能够在处理复杂查询时提高时间复杂度，这种方法应用于真实世界数据中能够提供有用的预测能力。

    Jun, 2018

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

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

    Apr, 2020

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

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

    Jan, 2022

  • 构建可逆的语义保留逻辑公式嵌入

    该研究工作探讨了如何使用基于图变分自编码器 (Graph Variational Autoencoder) 的深度架构来训练学习逻辑嵌入，以实现对逻辑嵌入的反向推理，即将嵌入空间中的逻辑公式反向映射回语法空间，进而提高机器学习中学习逻辑规则和性质的能力。

    May, 2023