# GPU-Accelerated Verification of Machine Learning Models for Power Systems

arXiv: https://arxiv.org/abs/2306.10617 · HTML: https://mlsanity.com/paper/2306.10617/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 30 references that are in the map.
- First posted on arXiv 18 Jun 2023.

## Builds on (most cited first, 13 of 13)

- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [(Certified!!) Adversarial Robustness for Free!](https://mlsanity.com/paper/2206.10550/) (2022)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Physics-Informed Neural Networks for AC Optimal Power Flow](https://mlsanity.com/paper/2110.02672/) (2021)
- [Learning Optimal Power Flow: Worst-Case Guarantees for Neural Networks](https://mlsanity.com/paper/2006.11029/) (2020)
- [Verification of Neural Network Behaviour: Formal Guarantees for Power System Applications](https://mlsanity.com/paper/1910.01624/) (2019)
- [Global Performance Guarantees for Neural Network Models of AC Power Flow](https://mlsanity.com/paper/2211.07125/) (2022)

## Built on by (most cited first, 4 of 4)

- [Dual Conic Proxies for AC Optimal Power Flow](https://mlsanity.com/paper/2310.02969/) (2023)
- [Scalable Exact Verification of Optimization Proxies for Large-Scale Optimal Power Flow](https://mlsanity.com/paper/2405.06109/) (2024)
- [Achieving the Tightest Relaxation of Sigmoids for Formal Verification](https://mlsanity.com/paper/2408.10491/) (2024)
- [Finite-Sample Probabilistic Safety Certification for AI-Based Grid-Edge Coordination](https://mlsanity.com/paper/2609.28182/) (2026)

## Abstract (arXiv)

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 α,β-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.