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

TL;DR

This work tackles the challenge of formally verifying DNNs that include early exits, whose conditional inference paths complicate standard robustness guarantees. It formalizes a revised local robustness property $P_{ee}$ for networks with multiple exits and presents a baseline verification algorithm augmented with two optimizations that preserve soundness and completeness. The authors prove that $P_{ee}$ is fixed-parameter tractable under trace stability, and validate the approach experimentally across MNIST and CIFAR datasets using multiple architectures, showing that early exits can improve verifiability and reduce verification time while balancing accuracy. They also analyze how exit placement and threshold choices affect performance, robustness, and efficiency, and demonstrate that adding EEs to standard models can enhance verification practicality and reliability in real-world settings.

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.

Figures (15)

• Figure 1: SAFE/UNSAFE/UNKNOWN counts per epsilon, across different networks and datasets.
• Figure 2: Comparison of verification times between the original model with the underlying verifier (Vanilla Time) and the model with EEs, using \ref{['alg:combined-break-then-continue-optimizations']}.
• Figure 4: Impact of threshold selection on accuracy vs. runtime (left), accuracy vs. robustness (middle) and robustness vs. verification time (right) for CNN on CIFAR-10, with $\epsilon = 0.005$.
• Figure 5: Detailed impact of threshold selection on verification time for LeNet-5 on CIFAR-10.
• Figure 6: Robustness comparison between vanilla and models with EEs.

Theorems & Definitions (21)

• theorem thmcountertheorem
• definition thmcounterdefinition
• definition thmcounterdefinition: Do12
• theorem thmcountertheorem
• theorem thmcountertheorem
• theorem thmcountertheorem
• theorem thmcountertheorem
• proof
• Theorem
• proof