Uncovering the Limits of Proof Sharing for Neural Networks

揭示神经网络证明共享的局限性

Abstract: 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.

摘要： 由于神经网络在许多关键领域的广泛应用，其鲁棒性验证变得日益重要。在某些场景下，研究表明通过在不同查询间复用中间层抽象状态（即模板），证明共享（proof sharing）可以加速不完全验证技术。然而，基于模板的加速方法在面对不同的网络架构、属性、数据集和训练方法时，其鲁棒性仍存在疑问。

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.

在这项工作中，我们对基于模板的加速技术的有效性及其局限性进行了系统性研究。研究表明，模板包含率（template subsumption rates）在不同场景下差异巨大。我们提出了一种衡量“联合稳定神经元”（jointly stable neurons）的新指标来解释这种差异，并指出在某些情况下，基于模板的技术极不可能带来任何加速效果。

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.

随后，我们提出了 FastCert，这是一种自动在神经网络层间分配模板以提升性能的新技术；如果模板不太可能产生加速效果，该技术会完全放弃使用它们。在一系列基于覆盖设计（covering-design）的 $L_0$ 验证任务中，FastCert 相比现有的基于模板的复用技术，平均实现了 1.13 倍的加速。