Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

TL;DR

This paper introduces RobLight, a lightweight and efficient method for verifying the robustness of graph neural networks against structural attacks, outperforming traditional solver-based approaches.

Contribution

It proposes replacing complex solvers with partial solvers for robustness verification, improving efficiency while maintaining effectiveness.

Findings

RobLight achieves faster verification times.

It maintains high accuracy in detecting adversarial attacks.

The approach is effective across various GNN models and datasets.

Abstract

Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, an important issue is the detection of attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the adversarial robustness problem - determining whether an attack exists - were originally developed for image classification. In the case of graph learning, the attack model usually considers changes to the graph structure in addition to or instead of the numerical features of the input, and the state of the art techniques proceed via reduction to constraint solving, working on top of powerful solvers, e.g. for mixed integer programming. We show that it is possible to improve on the state of the art in structural robustness by replacing the use of powerful solvers by calls to efficient partial solvers, which run in polynomial time but may be incomplete. We evaluate our tool RobLight on a diverse set of GNN variants and datasets.