Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits

• URL: http://arxiv.org/abs/2512.20755v1
• Date: Tue, 23 Dec 2025 20:36:54 GMT
• Title: Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
• Authors: Yizhak Yisrael Elboher, Avraham Raviv, Amihay Elboher, Zhouxing Shi, Omri Azencot, Hillel Kugler, Guy Katz,
• Abstract summary: We define a robustness property tailored to early exit architectures.<n>We show how off-the-shelf solvers can be used to assess it.<n>We show how these metrics can help users navigate the inherent trade-off between accuracy and efficiency.
• Score: 13.111404520708879
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Ensuring the safety and efficiency of AI systems is a central goal of modern research. Formal verification provides guarantees of neural network robustness, while early exits improve inference efficiency by enabling intermediate predictions. Yet verifying networks with early exits introduces new challenges due to their conditional execution paths. In this work, we define a robustness property tailored to early exit architectures and show how off-the-shelf solvers can be used to assess it. We present a baseline algorithm, enhanced with an early stopping strategy and heuristic optimizations that maintain soundness and completeness. Experiments on multiple benchmarks validate our framework's effectiveness and demonstrate the performance gains of the improved algorithm. Alongside the natural inference acceleration provided by early exits, we show that they also enhance verifiability, enabling more queries to be solved in less time compared to standard networks. Together with a robustness analysis, we show how these metrics can help users navigate the inherent trade-off between accuracy and efficiency.

Related papers

• WebLeaper: Empowering Efficiency and Efficacy in WebAgent via Enabling Info-Rich Seeking [60.35109192765302]
  Information seeking is a core capability that enables autonomous reasoning and decision-making.<n>We propose WebLeaper, a framework for constructing high-coverage IS tasks and generating efficient solution trajectories.<n>Our method consistently achieves improvements in both effectiveness and efficiency over strong baselines.
  arXiv  Detail & Related papers  (2025-10-28T17:51:42Z)
• Learning-Based Testing for Deep Learning: Enhancing Model Robustness with Adversarial Input Prioritization [0.0]
  This project aims to enhance fault detection and model robustness in Deep Neural Networks (DNNs)<n>Our method selects a subset of adversarial inputs with a high likelihood of exposing model faults without relying on architecture-specific characteristics or formal verification.<n>By efficiently organizing test permutations, it uncovers all potential faults significantly faster across various datasets, model architectures, and adversarial attack techniques.
  arXiv  Detail & Related papers  (2025-09-28T16:31:30Z)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees [3.208888890455612]
  We propose a novel framework to generate Verification-Friendly Neural Networks (VNNs) We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness.
  arXiv  Detail & Related papers  (2023-12-15T12:39:27Z)
• Free Lunch for Generating Effective Outlier Supervision [46.37464572099351]
  We propose an ultra-effective method to generate near-realistic outlier supervision. Our proposed textttBayesAug significantly reduces the false positive rate over 12.50% compared with the previous schemes.
  arXiv  Detail & Related papers  (2023-01-17T01:46:45Z)
• Large-Scale Sequential Learning for Recommender and Engineering Systems [91.3755431537592]
  In this thesis, we focus on the design of an automatic algorithms that provide personalized ranking by adapting to the current conditions. For the former, we propose novel algorithm called SAROS that take into account both kinds of feedback for learning over the sequence of interactions. The proposed idea of taking into account the neighbour lines shows statistically significant results in comparison with the initial approach for faults detection in power grid.
  arXiv  Detail & Related papers  (2022-05-13T21:09:41Z)
• Efficient Few-Shot Object Detection via Knowledge Inheritance [62.36414544915032]
  Few-shot object detection (FSOD) aims at learning a generic detector that can adapt to unseen tasks with scarce training samples. We present an efficient pretrain-transfer framework (PTF) baseline with no computational increment. We also propose an adaptive length re-scaling (ALR) strategy to alleviate the vector length inconsistency between the predicted novel weights and the pretrained base weights.
  arXiv  Detail & Related papers  (2022-03-23T06:24:31Z)
• Unsupervised Domain-adaptive Hash for Networks [81.49184987430333]
  Domain-adaptive hash learning has enjoyed considerable success in the computer vision community. We develop an unsupervised domain-adaptive hash learning method for networks, dubbed UDAH.
  arXiv  Detail & Related papers  (2021-08-20T12:09:38Z)
• Adaptive Inference through Early-Exit Networks: Design, Challenges and Directions [80.78077900288868]
  We decompose the design methodology of early-exit networks to its key components and survey the recent advances in each one of them. We position early-exiting against other efficient inference solutions and provide our insights on the current challenges and most promising future directions for research in the field.
  arXiv  Detail & Related papers  (2021-06-09T12:33:02Z)
• Bayesian Optimization with Machine Learning Algorithms Towards Anomaly Detection [66.05992706105224]
  In this paper, an effective anomaly detection framework is proposed utilizing Bayesian Optimization technique. The performance of the considered algorithms is evaluated using the ISCX 2012 dataset. Experimental results show the effectiveness of the proposed framework in term of accuracy rate, precision, low-false alarm rate, and recall.
  arXiv  Detail & Related papers  (2020-08-05T19:29:35Z)
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs [2.1320960069210484]
  Neural networks are commonly used in safety-critical real-world applications. Proving that either no such adversarial examples exist, or providing a concrete instance, is therefore crucial to ensure safe applications. We provide proofs for tight upper and lower bounds on max-pooling layers in convolutional networks.
  arXiv  Detail & Related papers  (2020-06-16T10:00:33Z)
• Learning Robust Feature Representations for Scene Text Detection [0.0]
  We present a network architecture derived from the loss to maximize conditional log-likelihood. By extending the layer of latent variables to multiple layers, the network is able to learn robust features on scale. In experiments, the proposed algorithm significantly outperforms state-of-the-art methods in terms of both recall and precision.
  arXiv  Detail & Related papers  (2020-05-26T01:06:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.