The Cost of Relaxation: Evaluating the Error in Convex Neural Network Verification
Not on the map. Why?
Abstract (arXiv)
Many neural network (NN) verification systems represent the network's input-output relation as a constraint program. Sound and complete, representations involve integer constraints, for simulating the activations. Recent works convexly relax the integer constraints, improving performance, at the cost of soundness. Convex relaxations consider outputs that are unreachable by the original network. We study the worst case divergence between the original network and its convex relaxations; both qualitatively and quantitatively. The relaxations' space forms a lattice, where the top element corresponds to a full relaxation, with every neuron linearized. The bottom element corresponds to the original network. We provide analytical upper and lower bounds for the ℓ_∞-distance between the fully relaxed and original outputs. This distance grows exponentially, w.r.t. the network's depth, and linearly w.r.t. the input's radius. The misclassification probability exhibits a step-like behavior, w.r.t. input radius. Our results are supported by experiments on MNIST, Fashion MNIST and random networks.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 21 of its 31 references that are in the map. First posted on arXiv 20 Apr 2026.
Builds on
21 of 31 references.
References · 21
- 2014Explaining and Harnessing Adversarial Examplescited by 7,364
- 2013Intriguing properties of neural networkscited by 5,155
- 2017Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithmscited by 4,349
- 2022Survey of Hallucination in Natural Language Generationcited by 2,075
- 2018Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examplescited by 1,268
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
- 2024DeepSeek LLM: Scaling Open-Source Language Models with Longtermismcited by 642
- 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 567
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 445
- 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 328
- 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 242
- 2020Understanding and Mitigating the Tradeoff Between Robustness and Accuracycited by 149
9 more
- 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 127
- 2019A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networkscited by 125
- 2017Dipole: Diagnosis Prediction in Healthcare via Attention-based Bidirectional Recurrent Neural Networkscited by 116
- 2024Marabou 2.0: A Versatile Formal Analyzer of Neural Networkscited by 81
- 2023First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)cited by 58
- 2022Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspectivecited by 42
- 2025Collaborative Retrieval for Large Language Model-based Conversational Recommender Systemscited by 16
- 2021Activation Functions in Artificial Neural Networks: A Systematic Overviewcited by 13
- 2024Autonomous Driving Small-Scale Cars: A Survey of Recent Developmentcited by 6
Built on by
Not cited yet.