Algorithms for verifying deep neural networks.
By Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., & Kochenderfer, M. J.
Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., & Kochenderfer, M. J. (2021). Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization, 4(3–4), 244–404. http://dx.doi.org/10.1561/2400000035
This survey explores the rigorous field of formal verification for deep neural networks, focusing on techniques that mathematically prove whether a network’s output remains within a safe or desired set for a given range of inputs. The authors provide a comprehensive taxonomy of methodologies, categorizing them into five primary families: reachability, primal optimization, dual optimization, search and reachability, and search and optimization. By detailing how these algorithms handle nonlinear activation functions like ReLU through various over-approximation and relaxation strategies, the text highlights the fundamental trade-off between computational scalability and mathematical completeness. Furthermore, the source provides a unified implementation framework and comparative empirical analysis to evaluate the runtime efficiency and precision of these diverse verification tools across different network architectures. Ultimately, the work serves as an essential guide for ensuring the safety, stability, and robustness of autonomous systems that rely on complex neural functions.