Systematic Generation of Diverse Benchmarks for DNN Verification

摘要

A recent DNN verification survey [ ], classifies approaches as being based on reachability, optimization, and search algorithms – or their combination. Reachability methods begin with a symbolic encoding of an input set and compute, for each layer, a symbolic encoding of the output set. They vary in the symbolic encodings used, e.g., intervals, polyhedra, and in the degree of overapproximation they introduce [ , , , ]. Optimization methods formulate verification as an optimization problem whose solution implies the validity of  [ , , , , , ]. Search methods work in combination with reachability and optimization, by decomposing the input space to formulate verification sub-problems that are discharged by the above techniques [ , , , , , , – ].