The robustness of neural networks is paramount in safety-critical applications. While most current robustness verification methods assess the worst-case output under the assumption that the input space is known, identifying a verifiable input space $\mathcal{C}$, where no adversarial examples exist, is crucial for effective model selection, robustness evaluation, and the development of reliable control strategies. To address this challenge, we introduce a novel framework, $\texttt{LEVIS}$, comprising $\texttt{LEVIS}$-$\alpha$ and $\texttt{LEVIS}$-$\beta$. $\texttt{LEVIS}$-$\alpha$ locates the largest possible verifiable ball within the central region of $\mathcal{C}$ that intersects at least two boundaries. In contrast, $\texttt{LEVIS}$-$\beta$ integrates multiple verifiable balls to encapsulate the entirety of the verifiable space comprehensively. Our contributions are threefold: (1) We propose $\texttt{LEVIS}$ equipped with three pioneering techniques that identify the maximum verifiable ball and the nearest adversarial point along collinear or orthogonal directions. (2) We offer a theoretical analysis elucidating the properties of the verifiable balls acquired through $\texttt{LEVIS}$-$\alpha$ and $\texttt{LEVIS}$-$\beta$. (3) We validate our methodology across diverse applications, including electrical power flow regression and image classification, showcasing performance enhancements and visualizations of the searching characteristics.

翻译：在安全关键应用中，神经网络的鲁棒性至关重要。尽管当前大多数鲁棒性验证方法基于输入空间已知的假设评估最坏情况输出，但识别一个不存在对抗样本的可验证输入空间 $\mathcal{C}$，对于有效的模型选择、鲁棒性评估以及可靠控制策略的开发至关重要。为应对这一挑战，我们引入了一个新颖框架 $\texttt{LEVIS}$，它包含 $\texttt{LEVIS}$-$\alpha$ 和 $\texttt{LEVIS}$-$\beta$。$\texttt{LEVIS}$-$\alpha$ 在 $\mathcal{C}$ 的中心区域定位与至少两个边界相交的最大可能可验证球。相比之下，$\texttt{LEVIS}$-$\beta$ 整合多个可验证球以全面覆盖整个可验证空间。我们的贡献有三方面：（1）我们提出了 $\texttt{LEVIS}$，它配备了三种开创性技术，能够识别最大可验证球以及沿共线或正交方向的最邻近对抗点。（2）我们提供了理论分析，阐明了通过 $\texttt{LEVIS}$-$\alpha$ 和 $\texttt{LEVIS}$-$\beta$ 获得的可验证球的性质。（3）我们在多种应用中验证了我们的方法，包括电力潮流回归和图像分类，展示了性能提升以及搜索特性的可视化结果。