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

May, 2019

Graph Representations for Higher-Order Logic and Theorem Proving

Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, Christian Szegedy

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

Abstract

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theor

graph neural networks proof search higher-order theorem provers deep learning holist benchmark

发现论文，激发创造

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

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

Nov, 2019

图挖掘的知识表示分析

研究高阶问题表述在知识表示方面的挑战性，并以图挖掘问题为例进行解决，提出了编码技术以及高阶语言扩展来实现高阶逻辑。此外，比较了三种不同的方法的性能，讨论了求解器的支持问题。

Aug, 2016

HOList: 面向高阶定理证明机器学习的环境

我们提供了一个基于 HOL Light 定理证明器的开源框架，可以用作强化学习环境；并提出了一个基于深度强化学习的自动定理证明器 DeepHOL，它在基准测试中取得了强大的初步结果。

Apr, 2019

HolStep：高阶逻辑定理证明的机器学习数据集

本文介绍了一种基于 Higher-Order Logic 证明的新数据集，旨在开发基于机器学习的定理证明策略并提出基于该数据集的各种机器学习任务，通过一些基于逻辑回归、卷积神经网络和循环神经网络的基准模型显示出将机器学习应用于 HOL 定理证明的前景。

Mar, 2017

图神经网络的逻辑

本文旨在阐述图神经网络的表达能力可以通过组合 Weisfeiler-Leman 算法和有限变量计数逻辑来精确描述，这种对应关系甚至导致了高阶图神经网络与高维 WL 算法的相应。

Apr, 2021

高效神经化 Higher-order Belief Propagation

本文提出了一种结合了图神经网络和概率图模型的方法，手段是利用一种高效的近似推理算法，将其嵌入到神经网络中实现端到端的学习，可以有效地捕捉节点和图之间的高阶关系，并在分子数据集上取得了明显优于基于 $k$ 阶图神经网络的最新效果。

Oct, 2020

Graph2Tac: 数学定理证明中的数学概念的分层表示学习

使用新的基于图的数据集进行 Coq 的机器学习，我们提出了 Graph2Tac（G2T）模型，通过考虑以往定义层次与当前目标之间的依赖关系，将新的数学概念整合到模型的知识库中。

Jan, 2024

图神经网络在知识图谱推理中的逻辑表现力

本文从逻辑表达式的角度对图神经网络进行了理论分析，实验结果验证了我们提出的实体标记方法的有效性，并揭示了基于标记技巧的最先进的方法为什么很有效。

Mar, 2023

图神经网络中的逻辑推理能力评估

本研究探讨使用关系学习算法如何进行逻辑推理，在设计了一套基于一阶逻辑的基准测试套件 GraphLog 后，我们使用图神经网络 (GNN) 来进行评估，并发现模型的泛化和适应能力强度受到训练中遇到的不同逻辑规则的多样性的影响。

Mar, 2020

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

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

Sep, 2017