VeriPrune: Equivalence verification of node pruned neural network

• Published in: Neurocomputing (Amsterdam) 2024-04, Vol.577, p.127347, Article 127347
• Main Authors: Wang, Weiru, Wang, Kai, Cheng, Zhiyang, Yang, Yilong
• Format: Article
• Language: English
• Subjects: Equivalence verification; Formal verification; Interval analysis; Neural network; Neural network compression
• ISSN: 0925-2312; 1872-8286
• DOI: 10.1016/j.neucom.2024.127347

Neural network compression is a widely used technique when deploying the neural network in energy-constrained and computation-constrained devices. To guarantee the compressed neural network is still usable without too much accuracy loss, the equivalence between the compressed networks and the original ones must be verified. However, the current verification approach can only verify the equivalence of the two neural networks in the same structure which is limited and unseen in real-world scenarios. In this paper, we proposed an equivalence verification method named VeriPrune, which can verify the equivalence of the deep neural networks without the structure limitation. In detail, we proposed an innovative virtual node completing method to solve the problem that node pruning causes structure change and invalidates the existing equivalence verification approaches. To demonstrate the feasibility and efficiency of the proposed approach, we conducted experiments on the public dataset with 49 DNNs and 1272 properties. The results show that the 83.9% properties, the 1067 of the total 1272 properties can be verified. The proposed VeriPrune can be further developed as a CASE tool for the industry settings. [Display omitted]