Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure

2024/04/23 by Tobias Ladner, Ladner, Tobias, Michael Eichelbeck +3 · 4 citations
Computer Science · #Embedded Systems Design Techniques #Formal Methods in Verification #Petri Nets in System Modeling

paper · pdf · doi:10.48550/arxiv.2404.15065

Abstract

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 perturbations inherently occur. However, these perturbations require us to formally verify neural networks before their deployment in safety-critical environments as neural networks are prone to adversarial attacks. While there exists research on the formal verification of neural networks, there is no work verifying the robustness of generic graph convolutional network architectures with uncertainty in the node features and in the graph structure over multiple message-passing steps. This work addresses this research gap by explicitly preserving the non-convex dependencies of all elements in the underlying computations through reachability analysis with (matrix) polynomial zonotopes. We demonstrate our approach on three popular benchmark datasets.

Cited by

• Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
• Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing
• Exact Verification of Graph Neural Networks with Incremental Constraint Solving
• Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

Related

• Certifiable Robustness to Graph Perturbations
• Fundamental Limits in Formal Verification of Message-Passing Neural Networks
• Certifying Robustness of Graph Convolutional Networks for Node Perturbation with Polyhedra Abstract Interpretation
• Certified Robustness of Graph Neural Networks against Adversarial Structural Perturbation
• Bounding the Expected Robustness of Graph Neural Networks Subject to Node Feature Attacks