Relational DNN Verification With Cross Executional Bound Refinement

Debangshu Banerjee, Gagandeep Singh
Proceedings of the 41st International Conference on Machine Learning, PMLR 235:2779-2807, 2024.

Abstract

We focus on verifying relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations (UAP), certified worst-case hamming distance for binary string classifications, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. However, most of the existing works in DNN verification only handle properties defined over single executions and as a result, are imprecise for relational properties. Though few recent works for relational DNN verification, capture linear dependencies between the inputs of multiple executions, they do not leverage dependencies between the outputs of hidden layers producing imprecise results. We develop a scalable relational verifier RACoon that utilizes cross-execution dependencies at all layers of the DNN gaining substantial precision over SOTA baselines on a wide range of datasets, networks, and relational properties.

Cite this Paper

BibTeX
@InProceedings{pmlr-v235-banerjee24a, title = {Relational {DNN} Verification With Cross Executional Bound Refinement}, author = {Banerjee, Debangshu and Singh, Gagandeep}, booktitle = {Proceedings of the 41st International Conference on Machine Learning}, pages = {2779--2807}, year = {2024}, editor = {Salakhutdinov, Ruslan and Kolter, Zico and Heller, Katherine and Weller, Adrian and Oliver, Nuria and Scarlett, Jonathan and Berkenkamp, Felix}, volume = {235}, series = {Proceedings of Machine Learning Research}, month = {21--27 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v235/main/assets/banerjee24a/banerjee24a.pdf}, url = {https://proceedings.mlr.press/v235/banerjee24a.html}, abstract = {We focus on verifying relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations (UAP), certified worst-case hamming distance for binary string classifications, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. However, most of the existing works in DNN verification only handle properties defined over single executions and as a result, are imprecise for relational properties. Though few recent works for relational DNN verification, capture linear dependencies between the inputs of multiple executions, they do not leverage dependencies between the outputs of hidden layers producing imprecise results. We develop a scalable relational verifier RACoon that utilizes cross-execution dependencies at all layers of the DNN gaining substantial precision over SOTA baselines on a wide range of datasets, networks, and relational properties.} }
Endnote
%0 Conference Paper %T Relational DNN Verification With Cross Executional Bound Refinement %A Debangshu Banerjee %A Gagandeep Singh %B Proceedings of the 41st International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2024 %E Ruslan Salakhutdinov %E Zico Kolter %E Katherine Heller %E Adrian Weller %E Nuria Oliver %E Jonathan Scarlett %E Felix Berkenkamp %F pmlr-v235-banerjee24a %I PMLR %P 2779--2807 %U https://proceedings.mlr.press/v235/banerjee24a.html %V 235 %X We focus on verifying relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations (UAP), certified worst-case hamming distance for binary string classifications, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. However, most of the existing works in DNN verification only handle properties defined over single executions and as a result, are imprecise for relational properties. Though few recent works for relational DNN verification, capture linear dependencies between the inputs of multiple executions, they do not leverage dependencies between the outputs of hidden layers producing imprecise results. We develop a scalable relational verifier RACoon that utilizes cross-execution dependencies at all layers of the DNN gaining substantial precision over SOTA baselines on a wide range of datasets, networks, and relational properties.
APA
Banerjee, D. & Singh, G.. (2024). Relational DNN Verification With Cross Executional Bound Refinement. Proceedings of the 41st International Conference on Machine Learning, in Proceedings of Machine Learning Research 235:2779-2807 Available from https://proceedings.mlr.press/v235/banerjee24a.html.

Related Material