A Logic for Reasoning about Aggregate-Combine Graph Neural Networks

Pierre Nunn; Marco Sälzer; François Schwarzentruber; Nicolas Troquard

IJCAI 2024poster3 citations

A Logic for Reasoning about Aggregate-Combine Graph Neural Networks

Pierre Nunn, Marco Sälzer, François Schwarzentruber, Nicolas Troquard

Abstract

We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.

Knowledge Representation and Reasoning: KRR: Learning and reasoningMachine Learning: ML: Explainable/Interpretable machine learningMachine Learning: ML: Learning theory

BibTeX

@inproceedings{ijcai2024p391,
  title     = {A Logic for Reasoning about Aggregate-Combine Graph Neural Networks},
  author    = {Nunn, Pierre and Sälzer, Marco and Schwarzentruber, François and Troquard, Nicolas},
  booktitle = {Proceedings of the Thirty-Third International Joint Conference on
               Artificial Intelligence, {IJCAI-24}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Kate Larson},
  pages     = {3532--3540},
  year      = {2024},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2024/391},
  url       = {https://doi.org/10.24963/ijcai.2024/391},
}