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.

翻译：本文通过建立与逻辑学的联系，研究了主流图学习形式化方法——图神经网络（GNNs）的表达能力与可判定性问题。我们采用一类近期发现的包含"普雷斯伯格量词"的可判定逻辑体系，展示了如何利用这些逻辑工具度量不同类别GNNs的表达能力，并在某些情况下实现了逻辑系统与GNNs表达能力的精确对应。同时，我们运用这些逻辑及其分析技术，为GNNs的验证问题构建了决策判定流程。研究进一步补充了关于这些逻辑体系静态分析问题的不可判定性结果，以及GNN验证问题的不可判定性证明。