Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

Chia-Hsuan Lu, Tony Tan, Michael Benedikt

TL;DR

This work tackles robust verification of graph neural networks under structural perturbations, a problem that is NP-hard and traditionally approached with heavy MIP solvers. The authors propose RobLight, a lightweight, partial-solver-based framework that uses a partial oracle (non-robustness tester and bound propagator) to perform a DFS-guided search over perturbed graphs with incomplete information. By exploiting GNN structure, including incremental computation, reordering, and budget-aware bound tightening, RobLight achieves substantial speedups over state-of-the-art solvers and scales to 4-layer GNNs on standard benchmarks. The results demonstrate accurate radius-of-robustness calculations and strong end-to-end performance on node and graph classification tasks, indicating practical viability for robust verification in graph learning settings.

Abstract

Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, and important issue is the detection of adversarial attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the adversarial robustness problem - determining whether such an attack exists - were originally developed for image classification, but there are variants for many other machine learning architectures. 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 in the area 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.

Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing

TL;DR

This work tackles robust verification of graph neural networks under structural perturbations, a problem that is NP-hard and traditionally approached with heavy MIP solvers. The authors propose RobLight, a lightweight, partial-solver-based framework that uses a partial oracle (non-robustness tester and bound propagator) to perform a DFS-guided search over perturbed graphs with incomplete information. By exploiting GNN structure, including incremental computation, reordering, and budget-aware bound tightening, RobLight achieves substantial speedups over state-of-the-art solvers and scales to 4-layer GNNs on standard benchmarks. The results demonstrate accurate radius-of-robustness calculations and strong end-to-end performance on node and graph classification tasks, indicating practical viability for robust verification in graph learning settings.

Abstract

Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, and important issue is the detection of adversarial attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the adversarial robustness problem - determining whether such an attack exists - were originally developed for image classification, but there are variants for many other machine learning architectures. 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 in the area 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.
Paper Structure (41 sections, 4 theorems, 37 equations, 3 figures, 16 tables, 2 algorithms)

This paper contains 41 sections, 4 theorems, 37 equations, 3 figures, 16 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Graph Neural Networks
  4. Adversarial Robustness of GNNs
  5. Lightweight robustness analysis graph neural networks
  6. Non-robustness tester
  7. Bound propagator
  8. Optimization
  9. Incremental Computation for the Partial Oracle
  10. Reordering Operations
  11. Bound Tightening of Aggregation Functions Using Budgets
  12. Graph Structure Heuristics for Edge Picking in the High-level algorithm
  13. Edge inference for local budgets
  14. Experiments
  15. Implementation of $\textup{RobLight}$ and Set up
  16. ...and 26 more sections

Key Result

lemma thmcounterlemma

For every incomplete graph $\mathcal{H} \in \mathfrak{H}_{V, X}$ and graph $\mathcal{G} \in \mathfrak{H}_{V, X}$, letting $\mathcal{G}'$ be the grounding of $\mathcal{H}$ to $\mathcal{G}$, it holds that ${\mathsf{dist}\left( \mathcal{G}', \mathcal{G} \right)} = {\mathsf{dist}\left( \mathcal{H}, \mat

Figures (3)

  • Figure 1: The number of instances solved by each tool plotted against runtime under different aggregations and budgets. The solid line denotes $\textup{RobLight}$, the dashed line denotes $\textup{GNNev}$, and the dotted line denotes $\textup{SCIP-MPNN}$. The blue, orange, green, and red lines correspond to budgets of $1$, $2$, $5$, and $10$, respectively. Note that the $x$ axis is in logarithmic scale.
  • Figure 2: The number of recursive calls plotted against the number of edges in the set of fragile edges. The blue dots represent the robust instances solved by $\textup{RobLight}$, the orange dots represent the non-robust instances solved by $\textup{RobLight}$, the green dots represent the robust instances solved by $\textup{RobLight}$ without any optimization strategies, and the red dots represent the non-robust instances solved by $\textup{RobLight}$ without any optimization strategies. Note that the $y$ axis is in logarithmic scale.
  • Figure 3: The number of instances solved by each tool plotted against runtime under different aggregations and budgets. The solid line denotes $\textup{RobLight}$ and the dotted line denotes $\textup{SCIP-MPNN}$. The blue, orange, green, red, purple, and brown lines correspond to pairs of global and local budget of $(1, 1)$, $(2, 1)$, $(2, 2)$, $(5, 1)$, $(5, 2)$, and $(5, 5)$, respectively. Note that the $x$ axis is in logarithmic scale.

Theorems & Definitions (27)

  • definition thmcounterdefinition: Featured graphs
  • definition thmcounterdefinition: Incomplete graphs
  • definition thmcounterdefinition: Refinement
  • definition thmcounterdefinition: Completion
  • definition thmcounterdefinition: Grounding
  • definition thmcounterdefinition: Relaxation
  • definition thmcounterdefinition: Distance
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • definition thmcounterdefinition: Graph neural network
  • ...and 17 more