论文标题
有效的二进制神经网络的精确验证
Efficient Exact Verification of Binarized Neural Networks
论文作者
论文摘要
与神经网络的可靠性有关，研究人员开发了验证技术以证明其稳健性。大多数验证仪与实价网络一起使用。不幸的是，确切的（完整和声音）验证者面临可扩展性的挑战，并且由于浮点误差而无法提供正确的保证。我们认为，二元化神经网络（BNN）提供了可比的鲁棒性，并允许精确且有效地验证。我们提出了一个新系统EEV，以有效且精确的BNN验证。 EEV由两个部分组成：（i）一个新颖的SAT求解器，该求解器通过在BNN编码中固定处理固定的基数约束来加快BNN验证； （ii）通过诱导平衡的层次稀疏性和低基数界限并自适应取消梯度来训练求解求解器友好的BNN的策略。我们通过在MNIST和CIFAR10数据集对非平凡卷积BNN的L-INF结合的对抗性鲁棒性的第一个精确验证结果来证明EEV的有效性。与在相同任务上对相同体系结构的实价网络的精确验证相比，EEV验证了BNNS的数百到数千倍，同时在大多数情况下提供了可比较的可验证准确性。
Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases.
