Graph neural networks (GNNs) are increasingly often employed in high-stakes applications, such as fraud detection or healthcare, but are susceptible to adversarial attacks. A number of techniques have been proposed to provide adversarial robustness guarantees, but support for commonly used aggregation functions in message-passing GNNs is lacking. In this paper, we develop an exact (sound and complete) verification method for GNNs to compute guarantees against attribute and structural perturbations that involve edge addition or deletion, subject to budget constraints. Our method employs constraint solving with bound tightening, and iteratively solves a sequence of relaxed constraint satisfaction problems while relying on incremental solving capabilities of solvers to improve efficiency. We implement GNNev, a versatile exact verifier for message-passing neural networks, which supports three aggregation functions -- sum, max and mean -- with the latter two considered here for the first time. Extensive experimental evaluation of GNNev on real-world fraud datasets (Amazon and Yelp) and biochemical datasets (MUTAG and ENZYMES) demonstrates its usability and effectiveness, as well as superior performance on node classification and competitiveness on graph classification compared to existing exact verification tools on sum-aggregated GNNs.

翻译：图神经网络近年来在高风险场景（如欺诈检测、医疗健康）中得到广泛应用，但容易遭受对抗攻击。当前已有多种技术被提出用于提供对抗鲁棒性保证，然而这些技术缺乏对消息传递型图神经网络中常用聚合函数的支持。本文提出一种针对图神经网络的精确（完备且可判定）验证方法，用于计算在预算约束下针对属性扰动和结构扰动（涵盖边增删）的保证。该方法采用带边界收紧的约束求解技术，通过迭代求解一系列松弛约束满足问题，并借助求解器的增量求解能力提升效率。我们实现了GNNev——一个支持三种聚合函数（求和、最大值、均值）的通用精确验证工具，其中后两种聚合函数首次被纳入验证范畴。基于真实欺诈数据集（Amazon、Yelp）与生物化学数据集（MUTAG、ENZYMES）的大量实验表明，该工具具备实用性和有效性，且在节点分类任务上性能优越，在图分类任务上与现有针对求和聚合图神经网络的精确验证工具具有竞争力。