基于可达性的具有节点和边特征的图神经网络形式化验证

图神经网络（GNN）已成为电力系统中开发快速且具拓扑感知能力的替代模型的重要方法，可支持潮流（PF）分析、最优潮流（OPF）估计和连锁故障分析（CFA）等任务。尽管其应用日益广泛，对基于 GNN 的模型进行形式化验证仍然具有挑战性，现有方法的适用范围也较为有限。我们通过引入 GraphStar 集合，将神经网络验证（NNV）框架扩展到图结构输入。GraphStar 集合是 Star 集合的推广，能够刻画节点特征和边特征上的不确定性。该扩展支持在线性消息传递操作中的集合传播，并能够对 GNN 架构中的 ReLU 非线性进行可靠近似，其中包括图卷积网络（GCN）层和带边特征的图同构网络（GINE）层。我们在三个电力系统任务——PF、OPF 和 CFA——上评估了 GNNV，测试案例包括 IEEE-24、IEEE-39 和 IEEE-118；此外还在两个标准图分类基准数据集 ENZYMES 和 PROTEINS 上进行了评估。结果表明，在采用基于 ReLU 的激活函数的图分类模型中，GNNV 比 CORA 提供了更严格的鲁棒性保证；同时，GNNV 首次为基于 GINE 的 PF 和 OPF 模型在节点与边联合扰动下提供了考虑边特征的鲁棒性保证。