Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features

Problem

Formal verification of Graph Neural Networks (GNNs) is a challenging task due to the complexity and variability of graph-structured data. Existing verification methods are often limited in their scope and applicability, particularly when it comes to handling uncertainty in node and edge features. This paper addresses these gaps by proposing a new approach that extends the capabilities of existing verification frameworks to better accommodate GNNs.

Method

The authors extend the Neural Network Verification (NNV) framework to handle graph-structured inputs. A key component of their approach is the introduction of GraphStar sets, which generalize Star sets to account for uncertainty in both node and edge features. The method involves the propagation of linear message-passing operations, which are essential for GNNs. Additionally, the authors provide a sound approximation of ReLU nonlinearities, which are commonly used in GNN architectures. The proposed framework is evaluated on two specific architectures: Graph Convolutional Networks (GCNs) and Graph Isomorphism Networks with Edge features (GINE).

Results

The proposed method demonstrates improved robustness guarantees compared to the CORA framework on graph classification models utilizing ReLU activations. Specifically, the robustness guarantees provided by the authors are tighter than those achieved by CORA. Furthermore, the authors report edge-aware robustness guarantees for GINE-based models under joint node and edge perturbations, although no specific quantitative results are provided for these guarantees.

Limitations

The authors do not report any limitations in their work. However, it is important to note that the lack of quantitative results for edge-aware robustness guarantees may limit the ability to fully assess the effectiveness of the proposed method in practical scenarios.

Why it matters

This work has significant implications for the formal verification of GNNs, particularly in applications where robustness to perturbations in both node and edge features is critical. By providing a more comprehensive verification framework, this research paves the way for more reliable deployment of GNNs in safety-critical applications, such as autonomous systems and financial modeling, where understanding the limits of model behavior is essential.