让神经网络更快更安全，通过形式化验证早期退出结构
Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits
- 为带早期退出的网络设计专用鲁棒性验证方法
- 新算法在多个基准上实现更快验证和更高查询成功率
- 适合关注AI效率与安全平衡的研究者和开发者
确保AI系统的安全性和高效性是当前研究的核心目标。形式化验证可提供神经网络鲁棒性的保证，而早期退出则通过中间预测提升推理效率。然而，由于存在条件执行路径，验证带早期退出的网络带来新挑战。本文定义了专用于早期退出架构的鲁棒性属性，并展示如何使用现成求解器评估该属性。我们提出一种基线算法，结合早停策略与启发式优化，在保持严谨性与完备性的前提下提升性能。在多个基准上的实验验证了框架的有效性，并表明改进算法在推理加速的同时，也提升了可验证性——相比标准网络能在更短时间内解决更多查询。结合鲁棒性分析，我们揭示了准确率与效率之间的权衡关系，帮助用户做出合理选择。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。