近年来,深度神经网络（DNN）的鲁棒性比以往任何时候都受到更多的关注。这是因为在AI应用程序领域,DNN在安全攸关的程序（例如自动驾驶和身份验证控制）中被广泛采用。这些应用场景需要神经网络满足一定的鲁棒性,对细微扰动具有一定的抗干扰能力。为了解决这个问题,就需要严格地验证神经网络是否满足鲁棒性。而形式化方法已被证明有效地为DNN的鲁棒性提供可证明的认证。但是,由于验证问题固有的计算复杂性,它们或是遇到了可伸缩性不足的问题,或是遇到了精度方面的问题。在本文中,我们提出了一种新颖的以攻击为指导的方法,可以有效地验证神经网络的鲁棒性,并实现了验证工具Agrify。我们方法的新颖之处在于,我们使用现有的攻击方法来生成相对粗略的对抗样本,通过使用粗略对抗样本中的信息,达到简化最终验证问题的目的。特别的是,我们专注于具有Re LU激活函数的神经网络,这种网络已广泛应用于解决分类问题。我们结合了梯度攻击的高效性和形式化方法的精确性,在神经网络鲁棒性验证问题上找到了一个新的平衡————在不损失计算精度的情况下更加高效的验证神经网络。我们利用梯度攻击生成相对粗糙的对抗样本,利用其中的有效信息通过符号区间分析技术计算神经元的边界值,最后利用更紧的边界值构造一个更为简洁的MILP模型,通过求解该模型以达到验证神经网络鲁棒性的目的。为进行评估本文方法的有效性,我们将其与目前最先进的三个验证工具（MIPVer-ify,Neurify,Venus）做了对比,实验结果表明,我们的方法比基于约束解决方案的验证工具的性能最高高出69倍,同时可以计算出最小对抗扰动的对抗样本。对于那些经过对抗训练的网络,这种改进尤其重要。