We Cannot Guarantee Safety: The Undecidability of Graph Neural Network Verification
Graph Neural Networks (GNN) are commonly used for two tasks: (whole) graph
classification and node classification. We formally introduce generically
formulated decision problems for both tasks, corresponding to the following
pattern: given a GNN, some specification of valid inputs, and some
specification of valid outputs, decide whether there is a valid input
satisfying the output specification. We then prove that graph classifier
verification is undecidable in general, implying that there cannot be an
algorithm surely guaranteeing the absence of misclassification of any kind.
Additionally, we show that verification in the node classification case becomes
decidable as soon as we restrict the degree of the considered graphs.
Furthermore, we discuss possible changes to these results depending on the
considered GNN model and specifications.