LEVIS: Large Exact Verifiable Input Spaces for Neural Networks
<|reference_start|>LEVIS: Large Exact Verifiable Input Spaces for Neural Networks: 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.<|reference_end|>
@article{chehade2024levis:,
    title={LEVIS: Large Exact Verifiable Input Spaces for Neural Networks},
    author={Mohamad Fares El Hajj Chehade, Brian Wesley Bell, Russell Bent, Hao
  Zhu, Wenting Li},
    journal={arXiv preprint arXiv:2408.08824},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.08824},
    primaryClass={cs.LG}
}