Machine learning techniques often lack formal correctness guarantees, evidenced by the widespread adversarial examples that plague most deep-learning applications. This lack of formal guarantees resulted in several research efforts that aim at verifying Deep Neural Networks (DNNs), with a particular focus on safety-critical applications. However, formal verification techniques still face major scalability and precision challenges. The over-approximation introduced during the formal verification process to tackle the scalability challenge often results in inconclusive analysis. To address this challenge, we propose a novel framework to generate Verification-Friendly Neural Networks (VNNs). We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness. Our proposed framework results in VNNs that are comparable to the original DNNs in terms of prediction performance, while amenable to formal verification techniques. This essentially enables us to establish robustness for more VNNs than their DNN counterparts, in a time-efficient manner.

翻译：机器学习技术通常缺乏形式化的正确性保证，这一点从困扰大多数深度学习应用的普遍对抗样本中可见一斑。这种形式化保证的缺失促使了多项旨在验证深度神经网络的研究工作，尤其是在安全关键型应用领域。然而，形式化验证技术仍面临重大的可扩展性和精确性挑战。为应对可扩展性挑战而在形式化验证过程中引入的过度近似，常常导致分析结果无法定论。为应对这一挑战，我们提出了一种新颖的框架来生成验证友好型神经网络。我们提出了一种训练后优化框架，以在保持预测性能和验证友好性之间取得平衡。我们提出的框架所产生的VNN，在预测性能方面可与原始DNN相媲美，同时更适用于形式化验证技术。这本质上使我们能够以时间高效的方式，为比其对应的DNN更多的VNN建立鲁棒性保证。