Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats

在2019年的开创性工作中，Barceló和共同作者确定了与一阶逻辑可定义属性相对应的常数迭代深度图神经网络（GNNs）表达能力完全匹配的逻辑。在本文中，我们给出了两种情况下递归GNN的精确逻辑特征：（1）在浮点数设置中和（2）实数设置中。对于浮点数，与递归GNN相匹配的形式化方法是带有计数的基于规则的模态逻辑，而对于实数，我们使用适当的无穷模态逻辑，同样带有计数。这些结果在递归设置中给出了逻辑和GNN之间的精确匹配，而不需要在任何情况下相对于背景逻辑进行相对性，但使用了一些关于浮点算术的自然假设。应用我们的特征，我们还证明了，相对于在单调二阶逻辑（MSO）中可定义的图形属性，我们的无穷和基于规则的逻辑具有相同的表达能力。这意味着，相对于MSO可定义属性，具有实数和浮点数的递归GNN具有相同的表达能力，并表明，对于这样的属性，具有实数的递归GNN也由（有限的！）基于规则的模态逻辑进行了特征化。相比之下，在一般情况下，使用浮点数的表达能力比使用实数的表达能力要弱。除了逻辑导向的结果外，我们还通过分布式自动机对递归GNN进行了特征化，将其与分布式计算模型联系起来。

论文旨在精确地描述循环图神经网络（GNNs）的逻辑特性，以及它们与一阶逻辑定义的属性之间的关系。同时，论文探讨了浮点数和实数情况下适用于循环GNNs的逻辑特性。

论文提出了一种基于规则的模态逻辑和一种适用于实数的无穷模态逻辑，以精确匹配循环GNNs的表达能力。论文还表明，相对于在单调二阶逻辑（MSO）中定义的图形属性，这两种逻辑具有相同的表达能力。

论文的亮点包括：使用规则模态逻辑和无穷模态逻辑精确描述循环GNNs的逻辑特性；相对于MSO定义的图形属性，这两种逻辑具有相同的表达能力；通过分布式自动机描述循环GNNs；论文还提供了与分布式计算模型的联系。

最近在这个领域中的相关研究包括：Barceló等人的先前工作，以及使用GNNs进行图形分类和图形生成的研究。