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

arXiv: https://arxiv.org/abs/2512.20755 · HTML: https://mlsanity.com/paper/2512.20755/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Early exit and edge inference, one of 12 directions in Efficient LLM inference and serving.
- Builds on 56 of its 88 references that are in the map.
- First posted on arXiv 23 Dec 2025.

## Placed in

- Efficient LLM inference and serving / [Early exit and edge inference](https://mlsanity.com/inference/early-exit-and-edge-inference/)

## Builds on (most cited first, 30 of 56)

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [The Lottery Ticket Hypothesis: Finding Sparse, Trainable Neural Networks](https://mlsanity.com/paper/1803.03635/) (2018)
- [Conformer: Convolution-augmented Transformer for Speech Recognition](https://mlsanity.com/paper/2005.08100/) (2020)
- [Neural Architecture Search with Reinforcement Learning](https://mlsanity.com/paper/1611.01578/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [BranchyNet: Fast Inference via Early Exiting from Deep Neural Networks](https://mlsanity.com/paper/1709.01686/) (2017)
- [LayerSkip: Enabling Early Exit Inference and Self-Speculative Decoding](https://mlsanity.com/paper/2404.16710/) (2024)
- [A Survey of Model Compression and Acceleration for Deep Neural Networks](https://mlsanity.com/paper/1710.09282/) (2017)
- [BERT Loses Patience: Fast and Robust Inference with Early Exit](https://mlsanity.com/paper/2006.04152/) (2020)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Dynamic Channel Pruning: Feature Boosting and Suppression](https://mlsanity.com/paper/1810.05331/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Adaptive Focus for Efficient Video Recognition](https://mlsanity.com/paper/2105.03245/) (2021)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Why should we add early exits to neural networks?](https://mlsanity.com/paper/2004.12814/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Conditional Deep Learning for Energy-Efficient and Enhanced Pattern Recognition](https://mlsanity.com/paper/1509.08971/) (2015)
- [Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability](https://mlsanity.com/paper/1809.03008/) (2018)

## Built on by (most cited first, 1 of 1)

- [Talking with Verifiers: Automatic Specification Generation for Neural Network Verification](https://mlsanity.com/paper/2603.02235/) (2026)

## Abstract (arXiv)

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.