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.

翻译：我们聚焦于深度神经网络（DNN）的关系属性验证，例如针对通用对抗扰动（UAP）的鲁棒性、二进制字符串分类的认证最坏情况汉明距离等。对这些属性的精确验证需要推理同一DNN的多次执行。然而，现有的大多数DNN验证工作仅处理单次执行定义的属性，因此对关系属性而言不够精确。尽管近期少数关系型DNN验证研究捕获了多次执行输入之间的线性依赖关系，但它们未能利用隐藏层输出间的依赖关系，导致结果不够精确。我们开发了可扩展的关系型验证器RACoon，该验证器在DNN所有层中利用跨执行依赖关系，在广泛的数据集、网络和关系属性上显著提升了相对于现有最优方法（SOTA）的精确度。