LEVIS: Large Exact Verifiable Input Spaces for Neural Networks

TL;DR

LEVIS introduces a novel framework for precisely identifying large, verifiable input regions in neural networks, enhancing robustness verification through scalable optimization and geometric analysis.

Contribution

The paper presents a new verification framework combining MIP and CC optimization to efficiently identify large verifiable input spaces in neural networks.

Findings

Achieves up to 6x runtime reduction in verification tasks.

Demonstrates improved robustness verification in power flow and image classification.

Provides geometric insights into verifiable regions.

Abstract

The robustness of neural networks is crucial in safety-critical applications, where identifying a reliable input space is essential for effective model selection, robustness evaluation, and the development of reliable control strategies. Most existing robustness verification methods assess the worst-case output under the assumption that the input space is known. However, precisely identifying a verifiable input space \(\mathcal{C}\), where no adversarial examples exist, is challenging due to the possible high dimensionality, discontinuity, and non-convex nature of the input space. To address this challenge, we propose a novel framework, **LEVIS**, consisting of **LEVIS-{\alpha}** and **LEVIS-\b{eta}**. **LEVIS-{\alpha}** identifies a single, large verifiable ball that intersects at least two boundaries of a bounded region \(\mathcal{C}\), while **LEVIS-\b{eta}** systematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions include: (1) introducing a verification framework that uses mixed-integer programming (MIP) to compute nearest and directional adversarial points, (2) integrating complementarity-constrained (CC) optimization with a reduced MIP formulation for scalability, achieving up to a 6 times runtime reduction, (3) theoretically characterizing the properties of the verifiable balls obtained by **LEVIS-{\alpha}**, and (4) validating the approach across applications including electrical power flow regression and image classification, with demonstrated performance gains and geometric insights into the verifiable region.