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**, comprising **LEVIS-$\alpha$** and **LEVIS-$\beta$**. **LEVIS-$\alpha$** identifies a single, large verifiable ball that intersects at least two boundaries of a bounded region $ \mathcal{C} $, while **LEVIS-$\beta$** systematically captures the entirety of the verifiable space by integrating multiple verifiable balls. Our contributions are fourfold: we introduce a verification framework, **LEVIS**, incorporating two optimization techniques for computing nearest and directional adversarial points based on mixed-integer programming (MIP); to enhance scalability, we integrate complementary constrained (CC) optimization with a reduced MIP formulation, achieving up to a 17-fold reduction in runtime by approximating the verifiable region in a principled way; we provide a theoretical analysis characterizing the properties of the verifiable balls obtained through **LEVIS-$\alpha$**; and we validate our approach across diverse applications, including electrical power flow regression and image classification, demonstrating performance improvements and visualizing the geometric properties of the verifiable region.

Lay Summary:

Neural networks are powerful tools used in applications like image recognition and energy systems, but they can make mistakes when their inputs are slightly changed. This is risky in safety-critical areas such as power grid control or self-driving cars. Our work introduces LEVIS, a method that finds input regions where a neural network is guaranteed to behave correctly, even in the presence of small changes.Rather than guessing safe regions or checking every possible input, LEVIS builds exact "safe zones" around certain points, like drawing protective bubbles. These zones are carefully calculated so that any input inside will not trigger errors or surprises in the network's decisions. We introduce two strategies: one that finds a single large bubble and one that builds many smaller ones to cover more space. LEVIS is both fast and reliable thanks to a smart combination of optimization tools.We tested LEVIS on real problems from power systems and image classification. It found safer regions more accurately and faster than previous methods. Our approach can help make AI systems more trustworthy and easier to analyze in the real world.