提出新方法实现神经网络等价性验证，速度提升超300倍。
Revisiting Differential Verification: Equivalence Verification with Confidence
- 设计新型抽象域，提升等价性推理效率
- 验证结果覆盖大范围输入空间，非仅特定点
- 适用于模型剪枝后验证，适合高可靠场景
当部署前对已验证的神经网络进行剪枝并重新训练时，证明新网络与原始参考网络行为等价至关重要。本文重新审视差分验证机制，提出一种新型抽象域，使等价性推理更高效；同时从理论与实验角度分析哪些等价性质可通过差分推理高效求解。基于这些发现，结合置信度验证思想，提出一种新等价性属性，可利用差分验证实现对大范围输入空间的保证，而非仅针对预设输入点的小规模保证。我们在新工具VeryDiff中实现该方法，并在多个经典与新基准上进行评估，包括大型强子对撞机（CERN LHC）中的粒子喷注分类剪枝网络，结果显示相比最先进验证器alpha,beta-CROWN，中位加速比超过300倍。
原文摘要 · Abstract (English)
When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN's LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。