形式化验证是采用数学语言来论证一个硬件系统或软件系统是否在理论上能正常运作的方法。而对深度神经网络进行验证测试,能够帮助检测和改进神经网络的鲁棒性、安全性等综合性能,从而使神经网络在工业、交通、医学等领域的应用更为安全可靠和高效,这就需要利用基于形式化验证的方法,对现有的神经网络验证算法进行优化改进。Reluplex是现有的验证深度神经网络的算法之一,但它仍有许多缺陷和不足之处,例如仅限于能验证基于Relu激活函数的神经网络、有相当多的超时点无法验证、所耗时间和资源过多等等。本设计对Reluplex算法进行一系列改造和优化,以提高其运作效率并扩展其的验证功能。先是使之能验证Elu激活函数,随后再对整个算法加入多线程并行法、紧致化上下界和冲突分析以撤销拆分等优化措施,以节省整个算法的运行时间和至少攻克一部分超时点。这些优化既针对测试基于Relu激活函数的神经网络,也针对测试基于Elu激活函数的神经网络,从而分别进行对比分析,以验收优化效果。最后,获取了Relu激活函数、Elu激活函数分别在优化前和优化后下测试得到的总共四组实验数据。通过对比,可以看出在采用了优化措施后,不论是对Relu激活函数的验证还是对Elu激活函数的验证都确实提高了运算速度并解决了一些原算法下的超时测试点。还可以看出Elu激活函数下检验速度相对快于Relu激活函数,因为它比Relu节省神经网络的训练时间还能够增加相应的精确程度。这些能有助于以后研究深度神经网络的验证和优化。