LEVIS: Large Exact Verifiable Input Spaces for Neural Networks

Mohamad Fares El Hajj Chehade, Wenting Li, Brian Wesley Bell, Russell Bent, Saif R. Kazi, Hao Zhu
Proceedings of the 42nd International Conference on Machine Learning, PMLR 267:7634-7647, 2025.

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v267-chehade25b, title = {{LEVIS}: Large Exact Verifiable Input Spaces for Neural Networks}, author = {Chehade, Mohamad Fares El Hajj and Li, Wenting and Bell, Brian Wesley and Bent, Russell and Kazi, Saif R. and Zhu, Hao}, booktitle = {Proceedings of the 42nd International Conference on Machine Learning}, pages = {7634--7647}, year = {2025}, editor = {Singh, Aarti and Fazel, Maryam and Hsu, Daniel and Lacoste-Julien, Simon and Berkenkamp, Felix and Maharaj, Tegan and Wagstaff, Kiri and Zhu, Jerry}, volume = {267}, series = {Proceedings of Machine Learning Research}, month = {13--19 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v267/main/assets/chehade25b/chehade25b.pdf}, url = {https://proceedings.mlr.press/v267/chehade25b.html}, 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.} }
Endnote
%0 Conference Paper %T LEVIS: Large Exact Verifiable Input Spaces for Neural Networks %A Mohamad Fares El Hajj Chehade %A Wenting Li %A Brian Wesley Bell %A Russell Bent %A Saif R. Kazi %A Hao Zhu %B Proceedings of the 42nd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2025 %E Aarti Singh %E Maryam Fazel %E Daniel Hsu %E Simon Lacoste-Julien %E Felix Berkenkamp %E Tegan Maharaj %E Kiri Wagstaff %E Jerry Zhu %F pmlr-v267-chehade25b %I PMLR %P 7634--7647 %U https://proceedings.mlr.press/v267/chehade25b.html %V 267 %X 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.
APA
Chehade, M.F.E.H., Li, W., Bell, B.W., Bent, R., Kazi, S.R. & Zhu, H.. (2025). LEVIS: Large Exact Verifiable Input Spaces for Neural Networks. Proceedings of the 42nd International Conference on Machine Learning, in Proceedings of Machine Learning Research 267:7634-7647 Available from https://proceedings.mlr.press/v267/chehade25b.html.

Related Material