arXiv:2404.15065v2 宣告类型: replace-cross 摘要：图神经网络由于其独特的能力，能够在图结构化数据上进行处理，正在机器学习领域变得越来越受欢迎。它们还被应用于自然环境，其中会不可避免地发生扰动。然而，这些扰动要求我们在将其部署在安全关键环境中之前，对神经网络进行形式验证，因为神经网络容易受到对抗性攻击的影响。虽然存在对神经网络进行形式验证的研究，但在存在节点特征和图结构不确定性的情况下，对通用图卷积网络架构在多步消息传递步骤中的鲁棒性进行验证的工作仍然不存在。本研究通过在可达性分析中显式地保留底层计算中所有元素的非凸依赖关系，以矩阵多项式区形为工具解决了这一研究缺口。我们在三个流行的基准数据集上展示了我们的方法。