A Dual Approach to Scalable Verification of Deep Networks

Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, Pushmeet Kohli
Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence, PMLR R16:549-558, 2018.

Abstract

This paper addresses the problem of formally verifying desirable properties of neural net- works, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was lim- ited in its applicability by the size of the net- work, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activa- tion functions and specifications on neural net- work inputs and outputs. We formulate verifi- cation as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the opti- mization problem to obtain an upper bound on the worst case violation of the specification be- ing verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We de- velop specialized verification algorithms with provable tightness guarantees under special as- sumptions and demonstrate the practical sig- nificance of our general verification approach on a variety of verification tasks.

Cite this Paper

BibTeX
@InProceedings{pmlr-vR16-dvijotham18a, title = {A Dual Approach to Scalable Verification of Deep Networks}, author = {Dvijotham, Krishnamurthy and Stanforth, Robert and Gowal, Sven and Mann, Timothy and Kohli, Pushmeet}, booktitle = {Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence}, pages = {549--558}, year = {2018}, editor = {Globerson, Amir and Silva, Ricardo}, volume = {R16}, series = {Proceedings of Machine Learning Research}, month = {06--10 Aug}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/r16/main/assets/dvijotham18a/dvijotham18a.pdf}, url = {https://proceedings.mlr.press/r16/dvijotham18a.html}, abstract = {This paper addresses the problem of formally verifying desirable properties of neural net- works, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was lim- ited in its applicability by the size of the net- work, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activa- tion functions and specifications on neural net- work inputs and outputs. We formulate verifi- cation as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the opti- mization problem to obtain an upper bound on the worst case violation of the specification be- ing verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We de- velop specialized verification algorithms with provable tightness guarantees under special as- sumptions and demonstrate the practical sig- nificance of our general verification approach on a variety of verification tasks.}, note = {Reissued by PMLR on 04 October 2026.} }
Endnote
%0 Conference Paper %T A Dual Approach to Scalable Verification of Deep Networks %A Krishnamurthy Dvijotham %A Robert Stanforth %A Sven Gowal %A Timothy Mann %A Pushmeet Kohli %B Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence %C Proceedings of Machine Learning Research %D 2018 %E Amir Globerson %E Ricardo Silva %F pmlr-vR16-dvijotham18a %I PMLR %P 549--558 %U https://proceedings.mlr.press/r16/dvijotham18a.html %V R16 %X This paper addresses the problem of formally verifying desirable properties of neural net- works, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was lim- ited in its applicability by the size of the net- work, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activa- tion functions and specifications on neural net- work inputs and outputs. We formulate verifi- cation as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the opti- mization problem to obtain an upper bound on the worst case violation of the specification be- ing verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We de- velop specialized verification algorithms with provable tightness guarantees under special as- sumptions and demonstrate the practical sig- nificance of our general verification approach on a variety of verification tasks. %Z Reissued by PMLR on 04 October 2026.
APA
Dvijotham, K., Stanforth, R., Gowal, S., Mann, T. & Kohli, P.. (2018). A Dual Approach to Scalable Verification of Deep Networks. Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence, in Proceedings of Machine Learning Research R16:549-558 Available from https://proceedings.mlr.press/r16/dvijotham18a.html. Reissued by PMLR on 04 October 2026.

Related Material