{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T05:42:30Z","timestamp":1775281350778,"version":"3.50.1"},"reference-count":77,"publisher":"Emerald","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,2,11]]},"abstract":"<jats:p>Deep neural networks are widely used for nonlinear function approximation, with applications ranging from computer vision to control. Although these networks involve the composition of simple arithmetic operations, it can be very challenging to verify whether a particular network satisfies certain input-output properties. This article surveys methods that have emerged recently for soundly verifying such properties. These methods borrow insights from reachability analysis, optimization, and search. We discuss fundamental differences and connections between existing algorithms. In addition, we provide pedagogical implementations of existing methods and compare them on a set of benchmark problems.<\/jats:p>","DOI":"10.1561\/2400000035","type":"journal-article","created":{"date-parts":[[2020,12,2]],"date-time":"2020-12-02T12:32:50Z","timestamp":1606912370000},"page":"244-404","source":"Crossref","is-referenced-by-count":164,"title":["Algorithms for Verifying Deep Neural Networks"],"prefix":"10.1561","volume":"4","author":[{"given":"Changliu","family":"Liu","sequence":"first","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Tomer","family":"Arnon","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Chris","family":"Lazarus","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Christopher","family":"Strong","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Mykel J.","family":"Kochenderfer","sequence":"additional","affiliation":[{"name":"Stanford University"}]}],"member":"140","published-online":{"date-parts":[[2021,2,11]]},"reference":[{"key":"2026033014423096200_ref001","volume-title":"Deep learning","author":"Goodfellow","year":"2016"},{"key":"2026033014423096200_ref002","doi-asserted-by":"crossref","article-title":"Deep residual learning for image recognition","author":"He","DOI":"10.1109\/CVPR.2016.90"},{"key":"2026033014423096200_ref003","doi-asserted-by":"crossref","article-title":"The stanford corenlp natural language processing toolkit","author":"Manning","DOI":"10.3115\/v1\/P14-5010"},{"issue":"7540","key":"2026033014423096200_ref004","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1038\/nature14236","article-title":"Human-level control through deep reinforcement learning","volume":"518","author":"Mnih","year":"2015","journal-title":"Nature"},{"key":"2026033014423096200_ref005","doi-asserted-by":"crossref","article-title":"The limitations of deep learning in adversarial settings","author":"Papernot","DOI":"10.1109\/EuroSP.2016.36"},{"key":"2026033014423096200_ref006","volume-title":"Reachable set computation and safety verification for neural networks with relu activations","author":"Xiang","year":"2017"},{"issue":"11","key":"2026033014423096200_ref007","doi-asserted-by":"crossref","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","article-title":"Output reachable set estimation and verification for multilayer neural networks","volume":"29","author":"Xiang","year":"2018","journal-title":"IEEE Transactions on Neural Networks and Learning Systems"},{"key":"2026033014423096200_ref008","doi-asserted-by":"crossref","article-title":"NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems","author":"Tran","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"2026033014423096200_ref009","volume-title":"Static Analysis","author":"Li","year":"2019"},{"key":"2026033014423096200_ref010","doi-asserted-by":"crossref","article-title":"Ai2: Safety and robustness certification of neural networks with abstract interpretation","author":"Gehr","DOI":"10.1109\/SP.2018.00058"},{"key":"2026033014423096200_ref011","article-title":"Beyond the single neuron convex barrier for neural network certification","volume-title":"Advances in Neural Information Processing Systems (NeurIPS)","author":"Singh","year":"2019"},{"key":"2026033014423096200_ref012","article-title":"Fast and effective robustness certification","volume-title":"Advances in Neural Information Processing Systems (NeurIPS)","author":"Singh","year":"2018"},{"key":"2026033014423096200_ref013","doi-asserted-by":"crossref","article-title":"An abstract domain for certifying neural networks","author":"Singh","DOI":"10.1145\/3290354"},{"key":"2026033014423096200_ref014","article-title":"Boosting robustness certification of neural networks","author":"Singh"},{"key":"2026033014423096200_ref015","volume-title":"An approach to reachability analysis for feed-forward relu neural networks","author":"Lomuscio","year":"2017"},{"key":"2026033014423096200_ref016","volume-title":"Evaluating robustness of neural networks with mixed integer programming","author":"Tjeng","year":"2017"},{"key":"2026033014423096200_ref017","article-title":"Measuring neural net robustness with constraints","volume-title":"Advances in Neural Information Processing Systems (NIPS)","author":"Bastani","year":"2016"},{"key":"2026033014423096200_ref018","article-title":"A dual approach to scalable verification of deep networks","author":"Dvijotham"},{"key":"2026033014423096200_ref019","article-title":"Provable defenses against adversarial examples via the convex outer adversarial polytope","author":"Wong"},{"key":"2026033014423096200_ref020","article-title":"Lagrangian decomposition for neural network verification","author":"Bunel"},{"key":"2026033014423096200_ref021","article-title":"Certified defenses against adversarial examples","author":"Raghunathan"},{"key":"2026033014423096200_ref022","volume-title":"Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming","author":"Fazlyab","year":"2019"},{"key":"2026033014423096200_ref023","article-title":"Formal security analysis of neural networks using symbolic intervals","volume-title":"USENIX Security Symposium","author":"Wang","year":"2018"},{"key":"2026033014423096200_ref024","article-title":"Efficient formal safety analysis of neural networks","volume-title":"Advances in Neural Information Processing Systems","author":"Wang","year":"2018"},{"key":"2026033014423096200_ref025","doi-asserted-by":"crossref","article-title":"Safety verification of deep neural networks","author":"Huang","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"2026033014423096200_ref026","article-title":"Towards fast computation of certified robustness for ReLU networks","author":"Weng"},{"key":"2026033014423096200_ref027","article-title":"Efficient neural network robustness certification with general activation functions","volume-title":"Advances in Neural Information Processing Systems (NeurIPS)","author":"Zhang","year":"2018"},{"key":"2026033014423096200_ref028","article-title":"Execution-guided overapproximation (ego) for improving scalability of neural network verification","author":"Bak"},{"key":"2026033014423096200_ref029","doi-asserted-by":"crossref","article-title":"Efficient neural network verification via adaptive refinement and adversarial search","author":"Henriksen","DOI":"10.3233\/FAIA200385"},{"key":"2026033014423096200_ref030","doi-asserted-by":"crossref","article-title":"Reluplex: An efficient SMT solver for verifying deep neural networks","author":"Katz","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"2026033014423096200_ref031","doi-asserted-by":"crossref","article-title":"The marabou framework for verification and analysis of deep neural networks","author":"Katz","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"2026033014423096200_ref032","doi-asserted-by":"crossref","article-title":"Formal verification of piece-wise linear feed-forward neural networks","author":"Ehlers","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"2026033014423096200_ref033","volume-title":"Output range analysis for deep neural networks","author":"Dutta","year":"2017"},{"key":"2026033014423096200_ref034","article-title":"Efficient verification of neural networks via dependency analysis","author":"Botoeva"},{"key":"2026033014423096200_ref035","volume-title":"Effective formal verification of neural networks using the geometry of linear regions","author":"Khedr","year":"2020"},{"key":"2026033014423096200_ref036","article-title":"A unified view of piecewise linear neural network verification","volume-title":"Advances in Neural Information Processing Systems","author":"Bunel","year":"2018"},{"issue":"2020","key":"2026033014423096200_ref037","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel","year":"2020","journal-title":"Journal of Machine Learning Research"},{"key":"2026033014423096200_ref038","article-title":"Neural network branching for neural network verification","author":"Lu"},{"key":"2026033014423096200_ref039","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"Barrett","year":"2018"},{"issue":"1","key":"2026033014423096200_ref040","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1137\/141000671","article-title":"Julia: A fresh approach to numerical computing","volume":"59","author":"Bezanson","year":"2017","journal-title":"SIAM Review"},{"key":"2026033014423096200_ref041","volume-title":"Automated verification of neural networks: Advances, challenges and perspectives","author":"Leofante","year":"2018"},{"key":"2026033014423096200_ref042","volume-title":"Verification for machine learning, autonomy, and neural networks survey","author":"Xiang","year":"2018"},{"key":"2026033014423096200_ref043","article-title":"A convex relaxation barrier to tight robustness verification of neural networks","volume-title":"Advances in Neural Information Processing Systems","author":"Salman","year":"2019"},{"key":"2026033014423096200_ref044","volume-title":"Testing deep neural networks","author":"Sun","year":"2018"},{"key":"2026033014423096200_ref045","volume-title":"A practical tutorial on modified condition\/decision coverage","author":"Hayhurst","year":"2001"},{"key":"2026033014423096200_ref046","doi-asserted-by":"crossref","article-title":"Deepxplore: Automated whitebox testing of deep learning systems","author":"Pei","DOI":"10.1145\/3132747.3132785"},{"key":"2026033014423096200_ref047","doi-asserted-by":"crossref","article-title":"Deeptest: Automated testing of deep-neural-network-driven autonomous cars","author":"Tian","DOI":"10.1145\/3180155.3180220"},{"issue":"1-2","key":"2026033014423096200_ref048","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0304-3800(02)00064-9","article-title":"Illuminating the \u201cblack box\u201d: A randomization approach for understanding variable contributions in artificial neural networks","volume":"154","author":"Olden","year":"2002","journal-title":"Ecological Modelling"},{"key":"2026033014423096200_ref049","volume-title":"Verification of bina-rized neural networks","author":"Cheng","year":"2017"},{"key":"2026033014423096200_ref050","doi-asserted-by":"crossref","article-title":"Verifying properties of binarized deep neural networks","author":"Narodytska","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"2026033014423096200_ref051","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-03592-1_16","article-title":"Verification of binarized neural networks via inter-neuron factoring","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"Cheng","year":"2018"},{"key":"2026033014423096200_ref052","doi-asserted-by":"crossref","article-title":"Reachable set estimation and safety verification for piecewise linear systems with neural network controllers","author":"Xiang","DOI":"10.23919\/ACC.2018.8431048"},{"key":"2026033014423096200_ref053","doi-asserted-by":"crossref","article-title":"Learning and verification of feedback control systems using feedforward neural networks","author":"Dutta","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"2026033014423096200_ref054","doi-asserted-by":"crossref","article-title":"Verification of rnn-based neural agent-environment systems","author":"Akintunde","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"2026033014423096200_ref055","article-title":"Differentiable abstract interpretation for provably robust neural networks","author":"Mirman"},{"key":"2026033014423096200_ref056","doi-asserted-by":"crossref","article-title":"An abstraction-based framework for neural network verification","author":"Elboher","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"2026033014423096200_ref057","article-title":"Abstraction based output range analysis for neural networks","volume-title":"Advances in Neural Information Processing Systems","author":"Prabhakar","year":"2019"},{"key":"2026033014423096200_ref058","doi-asserted-by":"crossref","article-title":"JuliaReach: A toolbox for set-based reachability","author":"Bogomolov","DOI":"10.1145\/3302504.3311804"},{"key":"2026033014423096200_ref059","article-title":"Reachability analysis for neural agent-environment systems","author":"Akintunde"},{"key":"2026033014423096200_ref060","doi-asserted-by":"crossref","DOI":"10.1109\/CDC42340.2020.9303750","volume-title":"Tightened convex relaxations for neural network robustness certification","author":"Anderson","year":"2020"},{"key":"2026033014423096200_ref061","doi-asserted-by":"crossref","article-title":"Recurjac: An efficient recursive algorithm for bounding jacobian matrix of neural networks and its applications","author":"Zhang","DOI":"10.1609\/aaai.v33i01.33015757"},{"key":"2026033014423096200_ref062","doi-asserted-by":"crossref","article-title":"Star-based reachability analysis of deep neural networks","author":"Tran","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"2026033014423096200_ref063","doi-asserted-by":"crossref","article-title":"Parallelizable reachability analysis algorithms for feed-forward neural networks","author":"Tran","DOI":"10.1109\/FormaliSE.2019.00012"},{"key":"2026033014423096200_ref064","volume-title":"Reachability analysis for feed-forward neural networks using face lattices","author":"Yang","year":"2020"},{"key":"2026033014423096200_ref065","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"Verification of deep convolutional neural networks using imagestars","author":"Tran","year":"2020"},{"key":"2026033014423096200_ref066","volume-title":"Specification-guided safety verification for feedforward neural networks","author":"Xiang","year":"2018"},{"issue":"2","key":"2026033014423096200_ref067","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1137\/15M1020575","article-title":"Jump: A modeling language for mathematical optimization","volume":"59","author":"Dunning","year":"2017","journal-title":"SIAM Review"},{"key":"2026033014423096200_ref068","first-page":"1","article-title":"Strong mixed-integer programming formulations for trained neural networks","volume-title":"Mathematical Programming","author":"Anderson","year":"2020"},{"key":"2026033014423096200_ref069","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-642-37518-7_4","article-title":"Dual neural network","volume-title":"Repetitive Motion Planning and Control of Redundant Robot Manipulators","author":"Zhang","year":"2013"},{"key":"2026033014423096200_ref070","volume-title":"Fast neural network verification via shadow prices","author":"Rubies-Royo","year":"2019"},{"key":"2026033014423096200_ref071","article-title":"A theoretical framework for back-propagation","author":"LeCun"},{"key":"2026033014423096200_ref072","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"Boyd","year":"1994"},{"key":"2026033014423096200_ref073","doi-asserted-by":"crossref","article-title":"Improved geometric path enumeration for verifying ReLU neural networks","author":"Bak","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"2026033014423096200_ref074","article-title":"Evaluating the robustness of neural networks: An extreme value theory approach","author":"Weng"},{"key":"2026033014423096200_ref075","volume-title":"MNIST handwritten digit database","author":"LeCun","year":"2010"},{"issue":"3","key":"2026033014423096200_ref076","doi-asserted-by":"crossref","first-page":"598","DOI":"10.2514\/1.G003724","article-title":"Deep neural network compression for aircraft collision avoidance systems","volume":"42","author":"Julian","year":"2019","journal-title":"AIAA Journal of Guidance, Control, and Dynamics"},{"key":"2026033014423096200_ref077","article-title":"Neural network verifications workshop, vnn-comp","author":"Liu"}],"container-title":["Foundations and Trends\u00ae in Optimization"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftopt\/article-pdf\/4\/3-4\/244\/10975935\/2400000035en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftopt\/article-pdf\/4\/3-4\/244\/10975935\/2400000035en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T18:42:45Z","timestamp":1774896165000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftopt\/article\/4\/3-4\/244\/1324794\/Algorithms-for-Verifying-Deep-Neural-Networks"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,11]]},"references-count":77,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2021,2,11]]}},"URL":"https:\/\/doi.org\/10.1561\/2400000035","relation":{},"ISSN":["2167-3888","2167-3918"],"issn-type":[{"value":"2167-3888","type":"print"},{"value":"2167-3918","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,11]]}}}