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.
Code (0)
등록된 구현이 없습니다.
Tasks
Adversarial RobustnessClassificationGraph ClassificationGraph Neural NetworkNode ClassificationvalidMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Generalization and Representational Limits of Graph Neural Networks
We address two fundamental questions about graph neural networks (GNNs). First, we prove that several important graph properties cannot be computed by GNNs that rely entirely on local information. Such GNNs include the s…
Generalization BoundsOn the under-reaching phenomenon in message-passing neural PDE solvers: revisiting the CFL condition
This paper proposes sharp lower bounds for the number of message passing iterations required in graph neural networks (GNNs) when solving partial differential equations (PDE). This significantly reduces the need for exha…
How Does Message Passing Improve Collaborative Filtering?
Collaborative filtering (CF) has exhibited prominent results for recommender systems and been broadly utilized for real-world applications. A branch of research enhances CF methods by message passing used in graph neural…
Collaborative FilteringRecommendation SystemsTAGFormal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure
Graph neural networks are becoming increasingly popular in the field of machine learning due to their unique ability to process data structured in graphs. They have also been applied in safety-critical environments where…
Incompleteness of AI Safety Verification via Kolmogorov Complexity
Ensuring that artificial intelligence (AI) systems satisfy formal safety and policy constraints is a central challenge in safety-critical domains. While limitations of verification are often attributed to combinatorial c…