DeepCDCL: An CDCL-based Neural Network Verification Framework
Zongxin Liu, Pengfei Yang, Lijun Zhang, Xiaowei Huang
TL;DR
This work tackles the scalability of verifying safety-critical neural networks by reframing neural network verification as a CDCL-based problem. It introduces DeepCDCL, a framework that combines a multi-threaded Solver with a dedicated Clause Manager, enabling asynchronous conflict-clause learning and management to prune infeasible paths efficiently. Key contributions include a practical implementation with three neural-network–specific conflict-clause generation methods, asynchronous elastic filtering, and a clause-pooling mechanism, demonstrated to yield substantial speedups over a strong baseline on ACAS Xu and MNIST tasks. The results indicate significant improvements in UNSAT cases and notable runtime reductions, suggesting that CDCL-based verification with asynchronous learning can enhance the practicality of verifying neural networks in safety-critical settings.
Abstract
Neural networks in safety-critical applications face increasing safety and security concerns due to their susceptibility to little disturbance. In this paper, we propose DeepCDCL, a novel neural network verification framework based on the Conflict-Driven Clause Learning (CDCL) algorithm. We introduce an asynchronous clause learning and management structure, reducing redundant time consumption compared to the direct application of the CDCL framework. Furthermore, we also provide a detailed evaluation of the performance of our approach on the ACAS Xu and MNIST datasets, showing that a significant speed-up is achieved in most cases.