DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis

Abstract

We propose a novel, complete algorithm for the verification and analysis of feed-forward, ReLU-based neural networks. The algorithm, based on symbolic interval propagation, introduces a new method for determining split-nodes which evaluates the indirect effect that splitting has on the relaxations of successor nodes. We combine this with a new efficient linear-programming encoding of the splitting constraints to further improve the algorithm's performance. The resulting implementation, DEEPSPLIT, achieved speedups of around 1-2 orders of magnitude and 21-34% fewer timeouts when compared to the current SoA toolkits.