Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability of Graph Neural Networks via Logical Characterizations

Michael Benedikt, Chia-Hsuan Lu, Tony Tan

TL;DR

This work systematically maps the expressiveness and decidability landscape of graph neural networks through logical characterizations, leveraging decidable Presburger-type logics to relate GNNs to MP^2 and GP^2 formalisms. It establishes a finite spectrum for GNNs with eventually constant activations, enabling decidable satisfiability and universal-satisfiability results for several restricted GNN classes (notably local/global, outgoing-only, and piecewise-linear activations). It also proves tight complexity bounds, including PSPACE-completeness for satisfiability with local aggregation and TrReLU, and NP-completeness for fixed-layer variants, while showing undecidability for both satisfiability and universal satisfiability in several unbounded-activation settings. The paper further develops a representation framework using existential Presburger arithmetic with stars to handle modal-unbounded GNNs, and extends results to undirected graphs via guarded logics, highlighting a rich boundary between decidability and expressiveness. Overall, the work provides a rigorous, logic-based lens for verifying and reasoning about GNNs, with clear implications for designing verifiable graph-learning systems and guiding future theoretical explorations.

Abstract

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.

Decidability of Graph Neural Networks via Logical Characterizations

TL;DR

This work systematically maps the expressiveness and decidability landscape of graph neural networks through logical characterizations, leveraging decidable Presburger-type logics to relate GNNs to MP^2 and GP^2 formalisms. It establishes a finite spectrum for GNNs with eventually constant activations, enabling decidable satisfiability and universal-satisfiability results for several restricted GNN classes (notably local/global, outgoing-only, and piecewise-linear activations). It also proves tight complexity bounds, including PSPACE-completeness for satisfiability with local aggregation and TrReLU, and NP-completeness for fixed-layer variants, while showing undecidability for both satisfiability and universal satisfiability in several unbounded-activation settings. The paper further develops a representation framework using existential Presburger arithmetic with stars to handle modal-unbounded GNNs, and extends results to undirected graphs via guarded logics, highlighting a rich boundary between decidability and expressiveness. Overall, the work provides a rigorous, logic-based lens for verifying and reasoning about GNNs, with clear implications for designing verifiable graph-learning systems and guiding future theoretical explorations.

Abstract

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.
Paper Structure (26 sections, 65 theorems, 107 equations, 4 figures, 4 tables, 1 algorithm)

This paper contains 26 sections, 65 theorems, 107 equations, 4 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Acknowledgements
  3. Related work
  4. Preliminaries
  5. Summary of results
  6. Characterization and decidability of GNNs with eventually constant activation functions
  7. Decidability of satisfiability problems for GNNs with eventually constant functions, via logic
  8. Undecidability of $\mathsf{MP^2}$, and of GNNs with $\mathsf{TrReLU}$ and global readout
  9. $\mathsf{PSPACE}$-completeness of satisfiability for GNNs with local aggregation and $\mathsf{TrReLU}$ activations
  10. Exponential history-space property
  11. Exponential tree model property
  12. $\mathsf{PSPACE}$-completeness for the satisfiability problem of $\mathcal{L}\mathsf{TrReLU}\mathsf{{\text{-}}GNN}$s
  13. $\mathsf{NP}$-completeness for the satisfiability problem of fixed layer $\mathcal{L}\mathsf{TrReLU}\mathsf{{\text{-}}GNN}$s
  14. GNNs with unbounded activation functions
  15. Logics for unbounded activation function GNNs and separation of expressiveness
  16. ...and 11 more sections

Key Result

Theorem 3.13

The finite satisfiability problem of $\mathsf{GP^2}$ is decidable.

Figures (4)

  • Figure 1: Example of a $3$-unravelling tree of $\mathcal{G}_0$ on $v_1$.
  • Figure 2: $(n_1, n_2)$-bipolar graph.
  • Figure 3: An example of the encoding of the computation of the two-counter machines to directed graphs.
  • Figure 4: An example of the encoding of the computation of a two-counter machines in undirected graphs.

Theorems & Definitions (129)

  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Definition 3.5
  • Definition 3.6
  • Definition 3.7
  • Definition 3.10
  • Definition 3.11
  • Definition 3.12
  • ...and 119 more