Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915692941410304 |
|---|---|
| author | Elboher, Yizhak Yisrael Raviv, Avraham Elboher, Amihay Shi, Zhouxing Azencot, Omri Kugler, Hillel Katz, Guy |
| author_facet | Elboher, Yizhak Yisrael Raviv, Avraham Elboher, Amihay Shi, Zhouxing Azencot, Omri Kugler, Hillel Katz, Guy |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_20755 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits Elboher, Yizhak Yisrael Raviv, Avraham Elboher, Amihay Shi, Zhouxing Azencot, Omri Kugler, Hillel Katz, Guy Machine Learning Artificial Intelligence 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. |
| title | Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2512.20755 |