得益于科学技术的不断进步以及物理算力的逐步提高,神经网络作为当下人工智能领域的重要一环,已经被越来越多地应用于金融、交通、医疗、消费等各行各业中。但是,目前用于评估神经网络质量的方法依然是基于训练集—测试集的传统软件测试方法,无法保证神经网络的安全性甚至是正确性。再加上对抗攻击技术近些年不断地发展,使得对抗样本可以在只产生微小扰动的情况下肆意更改神经网络的输出,这也给人工智能领域覆上了一层阴霾。因此,神经网络的安全性问题得到了形式化方法领域的关注。形式化验证是一种利用数学手段严格描述系统的性质和行为并确保系统质量的关键技术,该方法可以有效避免传统测试方法的缺点,从而严格地证明神经网络的安全性。但是,由于神经网络不同于传统软件的特殊结构,再加上激活函数向神经网络引入了大量的非线性和非凸特征,这些问题使得神经网络的形式化验证变得十分困难。因此,当前许多已有的神经网络形式化验证算法在面对复杂的大型神经网络时会显得力不从心。本文从基于优化与搜索的神经网络形式化验证算法入手,提出了一种基于分治与抽象策略的神经网络形式化验证算法,以及与之对应的神经网络形式化验证框架。抽象是形式化领域中的一种经典方法,它旨在抛弃原始系统的一些细节从而有效地缩减状态空间,并同时提供对原有性质的形式化保证。为了确保抽象的正确性,本文还使用了一种混合近似编码来提供对激活函数精确编码的最小上近似抽象处理。该算法按照分治的思想不断对优化问题的约束集进行混合抽象编码,同时迭代地执行抽象精细化操作以减小待搜索的状态空间,由于抽象技术可以在原始系统的基础上构造出一个能够对原有的安全属性进行抽象描述的简易系统,因此该算法在面对大型的复杂神经网络验证问题时,避免了直接在最复杂的状态空间中探索,转而搜索一个较简单的状态空间,从而大幅地提高了神经网络的验证效率。本文基于该策略提出的神经网络验证框架也整合了许多可用的先进方法,例如:符号区间传播、符号线性松弛、输入域分割等技术,并给出了完整的实现思路,以指导后续开发真正可用的神经网络验证工具。最后,使用基于该框架实现的神经网络验证工具DAA-Verifier在面向无人机机载防撞系统和公开的手写数字图像识别神经网络上进行了多维度实验,评估了该算法的运行时间、计算效率以及性能提升效果。除此之外,也与国际知名团队开发的神经网络形式化验证工具进行了对比。实验结果证明,基于分治与抽象策略的神经网络形式化验证算法在复杂神经网络的验证问题上有着良好的表现。