Bridges between graph neural networks (GNNs) and logical formalisms have been established by fixing architectural choices, such as the types of aggregation, combination, and activation functions. These choices define restricted classes of GNNs for which tight correspondences with logical formalisms can be obtained, by showing that logical formulae can be translated into equivalent GNNs and, conversely, that GNNs can be translated into equivalent formulae. In this paper we take a semantic perspective by establishing the logical expressiveness of classes of GNN classifiers that are preserved under structural properties: embeddings (extensions), injective homomorphisms, and homomorphisms. We show that, for each such property, there exists a fragment of graded modal logic characterising the class of GNNs. In particular, preservation under embeddings, injective homomorphisms, and homomorphisms corresponds to existential graded modal logic, its existential-positive fragment, and existential-positive modal logic, respectively. These results characterise the expressiveness of broad classes of GNNs independently of specific architectural choices, but we also show that each of these classes admits a GNN architecture of the same expressiveness. Technically, our approach uses a new well-quasi-order result for trees of bounded height, yielding finite representations of unravelling-invariant classes.
翻译:通过固定架构选择,如聚合、组合和激活函数的类型,图神经网络(GNNs)与逻辑形式体系之间的桥梁得以建立。这些选择定义了受限的GNN类别,通过证明逻辑公式可转化为等价的GNN,反之GNN也可转化为等价的公式,可建立这些类别与逻辑形式体系之间的紧密对应关系。本文采取语义视角,建立图神经网络分类器类别的逻辑表达能力——这些分类器在结构性质(嵌入、单射同态和同态)下保持。我们证明,对应每个此类性质,存在一个刻画该GNN类别的分级模态逻辑片段。特别地,嵌入、单射同态和同态下的保持分别对应于存在分级模态逻辑、其存在正片段和存在正模态逻辑。这些结果刻画了广泛GNN类别的表达能力,且独立于具体的架构选择;同时我们也证明每个此类别均存在具有相同表达能力的GNN架构。在技术层面,我们的方法利用有界高度树的新拟良序结果,得到展开不变类别的有限表示。