效率与安全性的桥接: 带早期退出神经网络形式化验证
机器学习
2025-12-25 v1 人工智能
摘要
确保AI系统的安全性与效率是现代研究的核心目标.形式化验证提供神经网络鲁棒性保证, 而早期退出机制通过启用中间预测提升推理效率. 然而, 验证带早期退出的网络引入了新的挑战, 因其条件执行路径. 本文定义一种针对早期退出架构的鲁棒性属性, 并展示如何使用现成求解器进行评估. 我们提出基线算法, 并辅以早期终止策略与启发式优化, 保持严谨性与完备性. 实验在多个基准数据集上验证了框架效能, 并展示改进算法的性能提升. 除早期退出所提供的自然推理加速外, 我们发现其亦提升可验证性, 使更多查询能在更短时间内解决. 结合鲁棒性分析, 我们表明这些指标可帮助用户在准确性与效率之间导航固有的权衡.
引用
@article{arxiv.2512.20755,
title = {Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits},
author = {Yizhak Yisrael Elboher and Avraham Raviv and Amihay Elboher and Zhouxing Shi and Omri Azencot and Hillel Kugler and Guy Katz},
journal= {arXiv preprint arXiv:2512.20755},
year = {2025}
}