Example Guided Synthesis of Linear Approximations for Neural Network Verification-猫眼课题宝

DOI：

10.1007/978-3-031-13185-1_8

发表时间：

2022

期刊：

影响因子：

通讯作者：

中科院分区：

其他

文献类型：

作者：

Brandon Paulsen;Chao Wang

非线性函数的线性近似有着广泛的应用，例如严格的全局优化，最近，涉及神经网络的验证问题。在后一种情况下，神经网络的激活函数必须手工制作线性近似。这种手工制作是乏味的，可能容易出错，并且需要专家来证明线性近似的可靠性。这种限制与快速发展的深度学习领域不一致-当前验证工具要么缺乏必要的线性近似，要么在具有最先进激活函数的神经网络上表现不佳。在这项工作中，我们考虑的问题，自动合成的声音线性逼近一个给定的神经网络激活函数。我们的方法以实例为指导：我们开发了一个程序来生成示例，然后我们利用机器学习技术来学习一个输出线性近似的（静态）函数。然而，由于我们使用的机器学习技术没有正式的保证，因此合成的函数可能会产生违规的线性近似。为了解决这个问题，我们使用严格的全局优化技术来限制最大违规，然后相应地调整合成的线性近似以确保合理性。我们评估我们的方法在几个神经网络验证任务。我们的评估表明，自动合成的线性近似大大提高了精度（即，就解决的验证问题的数量而言）与现有技术的神经网络验证工具中的手工制作的线性近似相比。包含我们的代码和实验脚本的工件可以在https://zenodo.org/record/6525186#.Yp51L9LMIzM上找到。

Linear approximations of nonlinear functions have a wide range of applications such as rigorous global optimization and, recently, verification problems involving neural networks. In the latter case, a linear approximation must be hand-crafted for the neural network’s activation functions. This hand-crafting is tedious, potentially error-prone, and requires an expert to prove the soundness of the linear approximation. Such a limitation is at odds with the rapidly advancing deep learning field – current verification tools either lack the necessary linear approximation, or perform poorly on neural networks with state-of-the-art activation functions. In this work, we consider the problem of automatically synthesizing sound linear approximations for a given neural network activation function. Our approach isexample-guided: we develop a procedure to generate examples, and then we leverage machine learning techniques to learn a (static) function that outputs linear approximations. However, since the machine learning techniques we employ do not come with formal guarantees, the resulting synthesized function may produce linear approximations with violations. To remedy this, we bound the maximum violation using rigorous global optimization techniques, and then adjust the synthesized linear approximation accordingly to ensure soundness. We evaluate our approach on several neural network verification tasks. Our evaluation shows that the automatically synthesized linear approximations greatly improve the accuracy (i.e., in terms of the number of verification problems solved) compared to hand-crafted linear approximations in state-of-the-art neural network verification tools. An artifact with our code and experimental scripts is available at: https://zenodo.org/record/6525186#.Yp51L9LMIzM.

Example Guided Synthesis of Linear Approximations for Neural Network Verification

文献摘要

相似文献