We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.

翻译：我们展示了关于流行图学习形式——图神经网络（GNN）表达力与可判定性的研究成果，并借助其与逻辑之间的关联。通过利用一组近期发现的包含"Presburger量词"的可判定逻辑体系，我们展示了如何运用这些逻辑来度量各类GNN的表达能力，在某些情况下甚至得到了逻辑表达能力与GNN之间的精确对应关系。同时，我们运用这些逻辑及其分析技术，为GNN的验证问题构建了判定程序。此外，我们还给出了涉及该类逻辑的静态分析问题以及GNN验证问题的不可判定性结果作为补充。