发表机构
University of California, Riverside; University of Illinois Urbana-Champaign; University of Colorado Boulder; Amazon（加州大学河滨分校; 伊利诺伊大学厄巴纳-香槟分校; 科罗拉多大学博尔德分校; 亚马逊公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究系统探究神经网络证明共享的局限性，提出联合稳定神经元指标解释模板包含率差异，研发FastCert技术，在$L_0$-验证任务中较现有模板复用技术实现平均1.13倍加速。
AI 中文摘要
神经网络的鲁棒性验证因应用于诸多关键领域而愈发重要。在某些场景中，证明共享已被证明可通过跨查询复用中间层抽象状态（即模板）来加速不完备验证技术。然而，关于基于模板的加速在不同网络架构、属性、数据集及训练方法下的鲁棒性仍存在疑问。本研究对基于模板的加速的有效性及其局限性展开系统探究。研究表明，模板包含率在不同场景下差异极大；提出联合稳定神经元这一新指标以解释该差异，结果显示部分场景下基于模板的技术几乎无法提供加速。随后，提出FastCert这一新技术，其可自动在神经网络各层间分配模板以提升性能，若模板无法带来加速则完全弃用。在大量基于覆盖设计的$L_0$-验证任务中，FastCert相较于现有基于模板复用的技术实现了平均1.13倍的加速。
英文摘要
Robustness verification of neural networks is increasingly important, due to their use in many critical domains. In certain scenarios, proof sharing has been shown to accelerate incomplete verification techniques by reusing intermediate-layer abstract states, or templates, across queries. However, questions remain as to the robustness of template-based acceleration across varying network architectures, properties, datasets, and training methods. In this work, we perform a systematic study of the effectiveness of template-based acceleration and its limits. Our study shows that template subsumption rates can vary widely across scenarios. We present a novel metric of jointly stable neurons to explain this variation, showing that in some cases template-based techniques are very unlikely to provide any speedup. Then, we present FastCert, a novel technique for automatically distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup. Across a large set of covering-design based $L_0$-verification tasks, FastCert achieved an average speedup of 1.13x over an extant template-based reuse technique.
CommentsTo appear at the 33rd Static Analysis Symposium (SAS 2026)
