A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

TL;DR

This paper introduces a modal logic framework for reasoning about graph neural networks (GNNs), demonstrating transformations between formulas and GNNs, and analyzing the computational complexity of related problems.

Contribution

It develops a logic that captures GNN properties, enabling logical reasoning and efficient transformations between formulas and GNNs, advancing the understanding of GNN expressiveness.

Findings

Formulas can be transformed into GNNs and vice versa efficiently.

The satisfiability problem for the logic is PSPACE-complete.

Logical methods can be applied to GNN reasoning tasks.

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.