基于增量约束求解的图神经网络精确验证

图神经网络（GNNs）越来越多地应用于高风险场景，如欺诈检测或医疗保健，但容易受到对抗攻击的影响。已有多种技术被提出以提供对抗鲁棒性保证，但对消息传递 GNNs 中常用聚合函数的支持仍然不足。在本文中，我们开发了一种针对 GNNs 的精确（可靠且完备）验证方法，用于在预算约束下计算针对涉及边添加或删除的属性和结构扰动的保证。我们的方法采用带边界收紧的约束求解，并迭代求解一系列松弛的约束满足问题，同时依赖求解器的增量求解能力来提高效率。我们实现了 GNNev，一种适用于消息传递神经网络的多功能精确验证器，它支持三种聚合函数——sum、max 和 mean——其中后两者在此首次被考虑。在真实世界欺诈数据集（Amazon 和 Yelp）和生化数据集（MUTAG 和 ENZYMES）上对 GNNev 的广泛实验评估表明了其可用性和有效性，并且在节点分类任务上表现出优于现有 sum 聚合 GNNs 精确验证工具的卓越性能，在图分类任务上亦具竞争力。