Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure

由于图神经网络具有处理图结构数据的独特能力，因此在机器学习领域中越来越受欢迎。它们也被应用于安全关键环境中，因为这些环境中本质上会发生扰动。然而，这些扰动要求我们在神经网络部署到安全关键环境之前进行正式验证，因为神经网络容易受到对抗性攻击。虽然已经存在关于神经网络的形式验证的研究，但没有研究验证具有节点特征和图结构不确定性的通用图卷积网络架构在多个消息传递步骤中的鲁棒性。本研究通过使用（矩阵）多项式绕体积分析明确保留底层计算中所有元素的非凸依赖关系来填补这一研究空白。我们在三个流行的基准数据集上演示了我们的方法。

论文旨在解决如何在存在节点特征和图结构不确定性的情况下验证通用图卷积网络架构的鲁棒性，以确保其在安全关键环境中的部署。

通过使用（矩阵）多项式zonotope进行可达性分析，显式保留底层计算中所有元素的非凸依赖关系，从而解决了通用图卷积网络架构的鲁棒性验证问题。

论文在三个流行的基准数据集上展示了其方法，实现了对通用图卷积网络架构的鲁棒性验证。值得注意的是，该方法使用了多项式zonotope进行可达性分析，这是一种新的技术，能够处理存在不确定性的数据结构。

最近的相关研究包括使用不同的形式化验证技术来验证神经网络的鲁棒性，如SMT求解器和符号执行。相关论文包括《Towards Deep Learning Models Resistant to Adversarial Attacks》和《DeepPoly：多项式折线性松弛的深度神经网络验证》。