Fundamental Limits in Formal Verification of Message-Passing Neural Networks
This work addresses the fundamental limits of formal verification for graph neural networks, which is crucial for ensuring safety in applications like social network analysis or molecular modeling, but it is incremental as it builds on existing verification theory for neural networks.
The paper tackles the problem of formally verifying safety properties like output reachability and adversarial robustness in Message-Passing Neural Networks (MPNNs), showing that verification is impossible for graph-classifier MPNNs with unbounded graph size and non-trivial degree, but possible for node-classifier MPNNs when graph degree is bounded.
Output reachability and adversarial robustness are among the most relevant safety properties of neural networks. We show that in the context of Message Passing Neural Networks (MPNN), a common Graph Neural Network (GNN) model, formal verification is impossible. In particular, we show that 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, we also show that 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. We discuss the implications of these results, for the purpose of obtaining a complete picture of the principle possibility to formally verify GNN, depending on the expressiveness of the involved GNN models and input-output specifications.