Verifying Quantized Graph Neural Networks is PSPACE-complete

TL;DR

This paper studies the computational complexity of verifying quantized Graph Neural Networks, showing that the problem is PSPACE-complete, which highlights the inherent difficulty in formally verifying these models.

Contribution

It introduces the linear-constrained validity (LVP) problem for quantized GNNs, provides an efficient translation to logical language, and proves PSPACE-completeness.

Findings

LVP is in PSPACE for any reasonable activation functions

Verification of quantized GNNs is PSPACE-hard

Reasoning about quantized GNNs is computationally challenging

Abstract

In this paper, we investigate the verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifying GNNs properties, and provide an efficient translation from LVP instances into a logical language. We show that LVP is in PSPACE, for any reasonable activation functions. We provide a proof system. We also prove PSPACE-hardness, indicating that while reasoning about quantized GNNs is feasible, it remains generally computationally challenging.