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 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-α and LEVIS-β. LEVIS-α identifies a single, large verifiable ball that intersects at least two boundaries of a bounded region C. In contrast, LEVIS-β systematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions are fourfold: (1) We introduce a verification framework, LEVIS, incorporating two optimization techniques for computing nearest and directional adversarial points based on mixedinteger programming (MIP). (2) To enhance scalability, we integrate complementarity-constrained (CC) optimization with a reduced MIP formulation, achieving up to a 6-fold reduction in runtime while approximating the verifiable region in a principled manner. (3) We provide a theoretical analysis characterizing the properties of the verifiable balls obtained through LEVIS-α. (4) We validate our approach across diverse applications, including electrical power flow regression and