伴随着神经网络模型在各行业的广泛使用,其正确性和健壮性正在受到学术界和工业界越来越多的关注,特别是在安全攸关的领域中,如自动驾驶、恶意软件检测等,神经网络的每一次错误判断都将可能带来无法挽回的后果。神经网络是一种基于数理统计的优化模型,其目的在于使用近似函数高效地处理物理世界中难以描述的输入输出关系,这意味着神经网络对未知输入天然的不确定性;而形式化方法是一种建立在严谨数学逻辑上的适用于描述软硬件系统的建模和验证方法,其目的在于提升软硬件设计的可靠性,是典型的以确定性结果为导向的方法。将形式化方法应用于神经网络的建模和验证过程中,将有助于改善神经网络的不确定关系,同时提升神经网络输出结果的可信度。目前已有的研究方案主要以可满足性模块理论、抽象解释、区间计算等为基础,本文则立足于时序逻辑的性质验证,通过验证结果给出对神经网络关键性质的准确判断,并以此达到辅助改善神经网络模型系统的目的。本文提出了一种基于时序逻辑程序设计语言的神经网络正确性和健壮性的研究方案。该方案在统一模型检测UMC(Unified Model Checking)的框架下工作,其具体流程如下:首先,选用深度神经网络DNN(Deep Neural Network)模型和卷积神经网络CNN(Convolutional Neural Network)模型,准备合适的文本和图像数据集;其次,分析神经网络系统的模型正确性、样本正确性和模型健壮性,给出这三种共有性质的形式化定义,并在以DNN为核心的算术表达式系统和以CNN为核心的手写体图像识别系统中逐一细化,这些性质分别描述了模型系统的准确程度、输入数据的合理性和外来攻击的应对能力;然后,构建基于建模仿真验证语言MSVL(Modeling,Simulation and Verification Language)的神经网络模型系统M,并在 MC(MSVL Compiler)编译器中获得运行结果,与此同时,刻画基于命题投影时序逻辑PPTL(Propositional Projection Temporal Logic)的共有性质P,并在 UMC4M 验证器中获得验证结果;最后,面向拥有不同规模训练数据和不同层次网络结构的CNN模型系统,对比分析运行时间和验证时间的变化,结果表明,以性质为驱动的神经网络验证方案是可行且有效的。