Computational tools for rigorously verifying the performance of large-scale machine learning (ML) models have progressed significantly in recent years. The most successful solvers employ highly specialized, GPU-accelerated branch and bound routines. Such tools are crucial for the successful deployment of machine learning applications in safety-critical systems, such as power systems. Despite their successes, however, barriers prevent out-of-the-box application of these routines to power system problems. This paper addresses this issue in two key ways. First, for the first time to our knowledge, we enable the simultaneous verification of multiple verification problems (e.g., checking for the violation of all line flow constraints simultaneously and not by solving individual verification problems). For that, we introduce an exact transformation that converts the "worst-case" violation across a set of potential violations to a series of ReLU-based layers that augment the original neural network. This allows verifiers to interpret them directly. Second, power system ML models often must be verified to satisfy power flow constraints. We propose a dualization procedure which encodes linear equality and inequality constraints directly into the verification problem; and in a manner which is mathematically consistent with the specialized verification tools. To demonstrate these innovations, we verify problems associated with data-driven security constrained DC-OPF solvers. We build and test our first set of innovations using the $\alpha,\beta$-CROWN solver, and we benchmark against Gurobi 10.0. Our contributions achieve a speedup that can exceed 100x and allow higher degrees of verification flexibility.

翻译：近年来，用于严格验证大规模机器学习模型性能的计算工具取得了显著进展。最成功的求解器采用高度专业化的GPU加速分支定界例程。这类工具对于在电力系统等安全关键系统中成功部署机器学习应用至关重要。然而，尽管取得了成功，现有障碍仍阻碍这些例程直接应用于电力系统问题。本文从两个关键方面解决这一问题。首先，据我们所知，我们首次实现了多验证问题的同步验证（例如，同时检查所有线路潮流约束的违反情况，而非逐个求解验证问题）。为此，我们引入了一种精确变换，将一组潜在违反约束中的"最坏情况"违反转化为一系列基于ReLU的层，这些层作为原始神经网络的扩展模块，使验证器能够直接对其进行解释。其次，电力系统机器学习模型通常需要验证其是否满足潮流约束。我们提出一种对偶化流程，能够将线性等式和不等式约束直接编码到验证问题中，且编码方式与专用验证工具在数学上保持一致。为演示这些创新，我们验证了与数据驱动安全约束直流最优潮流求解器相关的问题。我们使用α,β-CROWN求解器构建并测试了首批创新成果，并以Gurobi 10.0作为基准。我们的贡献实现了超过100倍的加速效果，并提供了更高的验证灵活性。