Fundamental Limits in Formal Verification of Message-Passing Neural Networks

Output reachability and adversarial robustness are among the most relevant safety properties of neural networks. In the context of Message Passing Neural Networks (MPNN), a common Graph Neural Network (GNN) model, formal verification is impossible. In particular, output reachability of graph-classifier MPNN, working over graphs of unbounded size, non-trivial degree and sufficiently expressive node labels, cannot be verified formally: there is no algorithm that answers correctly (with yes or no), given an MPNN, whether there exists some valid input to the MPNN such that the corresponding output satisfies a given specification. However, output reachability and adversarial robustness of node-classifier MPNN can be verified formally when a limit on the degree of input graphs is given a priori. The paper discusses the implications of these results for assessing the possibility of formally verifying GNN, depending on the expressiveness of the involved GNN models and input-output specifications.