Counterexample-Guided Abstraction Refinement for Star-Based Neural Network Verification
摘要
We consider two reachability analysis methods for feedforward neural networks, which use star sets as datatype to store network states. While the first method is complete but computationally expensive, the second method offers better scalability by using over-approximations and thus sacrifying completeness. In this paper, we propose a counterexample-guided abstraction refinement (CEGAR) framework to combine the strengths of these two procedures, starting with the second method, and iteratively refining the over-approximation based on spurious counterexamples. Our algorithm is complete and it either certifies safety or it returns a counterexample as a proof of unsafety. We suggest multiple heuristics for the refinement and evaluate them experimentally, demonstrating that our CEGAR-based approach is more efficient than a previously proposed direct abstraction refinement method, and on some benchmarks, it significantly outperforms the exact method.