Machine learning techniques often lack formal correctness guarantees. This is evidenced by the widespread adversarial examples that plague most deep-learning applications. This resulted in several research efforts that aim at verifying deep neural networks, with a particular focus on safety-critical applications. However, formal verification techniques still face major scalability and precision challenges when dealing with the complexity of such networks. 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 robustness in the resulting networks. Our proposed framework proves to result in networks that are comparable to the original ones in terms of prediction performance, while amenable to verification. This essentially enables us to establish robustness for more VNNs than their deep neural network counterparts, in a more time-efficient manner.

翻译：机器学习技术通常缺乏形式化正确性保证，这一问题在困扰大多数深度学习应用的广泛对抗样本现象中得到了充分体现。这促使多项研究工作致力于深度神经网络验证，尤其是面向安全关键型应用场景。然而，形式化验证技术在应对此类网络复杂性时仍面临可扩展性和精度的重大挑战。为应对可扩展性挑战而引入的过度近似处理，往往导致验证分析结果不明确。针对这一问题，我们提出了一种生成验证友好型神经网络（VNNs）的创新框架。该后训练优化框架能够在保持网络预测性能与鲁棒性之间取得平衡。实验证明，所提框架生成的网络在预测性能与原始网络相当的同时更易于验证。这使得我们能够比深度神经网络更高效地建立更多VNN的鲁棒性。