LEVIS: Large Exact Verifiable Input Spaces for Neural Networks

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.