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. 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. Under review as a conference paper at ICLR 2023 This local notion of adversarial robustness is also common in formal verification of classical neural networks (NN). However, in NN verification, the absence of misbehaviour of a more global kind is adressed using so called output reachability properties (ORP) (cf. Huang et al. (2020)). A common choice of ORP specifies a convex set of valid input vectors and a convex set of valid output vectors and is satisfied by some NN if there is a valid input that leads to a valid output. Thus, falsifying ORP, specifiying unwanted behaviour as valid outputs, guarantees the absence of respective misbehaviour regarding the set of valid inputs. To the best of our knowledge there currently is no research directly concerned with ORP of GNN. This work adresses both of the above mentioned gaps: we present fundamental results regarding the (im-)possibility of formal verification of GNN. We prove that -in direct contrast to formal verification of NN -there are non-trivial classes of ORP and ARP used for MPNN graph classification, that cannot be verified formally. Namely, as soon as the chosen kind of input specifications allows for graphs of unbounded size, non-trivial degree and sufficiently expressive labels, formal verification is no longer automatically possible in the following sense: there is no algorithm that, given an MPNN and specifications of valid inputs and outputs, answers correctly (yes/no) whether some valid input is mapped to some (in-)valud output. Additionally, we show that ORP and ARP of MPNN used for node classification are formally verifiable as soon as the degree of valid input graphs is bounded. In the ARP case, this extends the previously known bounds. The remaining part of this work is structured as follows: we give necessary definitions in Sect. 2 and a comprehensive overview of our results in Sect.3. In Sect. 4 and Sect. 5, we cover formal arguments, with purely technical parts outsourced to App. A and B. Finally, we discuss and evaluate our possibility and impossibility results in Sect.6. RELATED WORK This paper adresses fundamental questions regarding formal verification of adversarial robustness and output reachability of MPNN and GNN in general. Günnemann (2022) presents a survey on recent developments in research on adversarial attack, defense and robustness of GNN. We recapitulate some categorizations made in the survey and rank the corresponding works in our results. First, according to Günnemann ( 2022 ) most work considers GNN used for node-classification (for example, Zügner et al. (2018); Dai et al. (2018); Wang et al. (2020); Wu et al. (2019)) and among such most common are edge modifications of a fixed input graph (cf. Zügner et al. (2018); Zügner & Günnemann (2019); Ma et al. (2020)), but also node injections or deletions are considered (cf. Sun et al. (2020); Geisler et al. ( 2021 )). In all cases, the amount of such discrete modifications is bounded, which means that the set of input graphs under consideration is finite and, thus, the maximal degree is bounded. Any argument for the possibility of formal verification derivable from these works is subsumed by Theorem 2 here. Additionally, there is work considering label modifications (cf. Zügner et al. (2018); Wu et al. (2019); Takahashi (2019)), but only in discrete settings or where allowed modifications are bounded by box constraints. Again, this is covered by Theorem 2. There is also work on adversarial robustness of graph-classifier GNN (cf. Jin et al. (2020); Chen et al. (2020); Bojchevski et al. ( 2020 )). In all cases, the considered set of input graphs is given by a bounded amount of structural pertubations to some center graph. Therefore, this is no contradiction to the result of Corollary 1 as the size of considered graphs is always bounded. As stated above, to the best of our knowledge, there currently is no work