一句话：提出基于反例潜力的增量神经网络验证方法 Olive，优先重验更可能含反例的子问题以尽早发现反例。
增量神经网络验证通过复用相似网络 N 的验证模板来加速目标网络 N* 的验证。现有方法利用分支限界的问题拆分历史筛选待重验子问题，但只判断是否重验，忽略重验优先级，未优先处理更可能含反例的子问题，难以尽早终止。本文基于模板定义子问题间的反例潜力序，提出 Olive，按反例潜力有序探索 N* 的子问题；变体 Olive_g 为贪心策略，偏向更可能含反例的子问题，Olive_b 为平衡策略，在模板不精确时也探索低潜力子问题。在 MNIST 与 CIFAR-10 的 15 个网络、1445 个实例上评估，Olive 显著优于经典验证与现有增量方法，在含反例实例上优势明显，在认证实例上与 Ivan 相当。
Incremental verification is an emerging neural network verification approach that aims to accelerate the verification of a neural network N* by reusing the existing verification result (called a template ) of a similar neural network N . To date, the state‐of‐the‐art incremental verification approach leverages the problem splitting history produced by branch and bound ( BaB ) in verification of N , to select only a part of the sub‐problems for verification of N* , thus more efficient than verifying N* from scratch. While this approach identifies whether each sub‐problem should be re‐assessed, it neglects the information of how necessary each sub‐problem should be re‐assessed, in the sense that the sub‐problems that are more likely to contain counterexamples should be prioritized, in order to terminate the verification process as soon as a counterexample is detected. To bridge this gap, we first define a counterexample potentiality order over different sub‐problems based on the template, and then we propose Olive, an incremental verification approach that explores the sub‐problems of verifying N* orderly guided by counterexample potentiality. Specifically, Olive has two variants, including Olive g , a greedy strategy that always prefers to exploit the sub‐problems that are more likely to contain counterexamples, and Olive b , a balanced strategy that also explores the sub‐problems that are less likely, in case the template is not sufficiently precise. We experimentally evaluate the efficiency of Olive on 1445 verification problem instances derived from 15 neural networks spanning over two datasets MNIST and CIFAR‐10 . Our evaluation demonstrates significant performance advantages of Olive over state‐of‐the‐art classic verification and incremental approaches. In particular, Olive shows evident superiority on the problem instances that contain counterexamples, and performs as well as Ivan on the certified problem instances.
@article{paperbot3154,
title = {Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality},
author = {Guanqin Zhang and Zhenya Zhang and H.M.N. Dilum Bandara and Shiping Chen and Jianjun Zhao and Yulei Sui},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720417}
}