摘要:神经网络鲁棒性验证作为保障人工智能系统安全性与可靠性的关键技术, 能够为智能决策提供形式化保证. 现有研究普遍基于数据分布各向同性的简化假设, 进行均匀Lp范数球邻域上的验证算法开发. 但这一理论框架在面对现实世界复杂的数据特性时显得力不从心, 例如: 数据不同特征对模型预测结果的影响及其对扰动的敏感度表现出差异性; 某些特征受物理约束限制具有不可变性; 特征间还可能存在复杂的相关性结构. 这使得基于均匀扰动域的验证算法难以准确建模现实世界对人工智能系统的鲁棒性需求. 针对上述局限, 提出基于非均匀扰动域的鲁棒性验证框架. 通过结合具体应用领域的数据分布特性, 合理构建符合领域特征的扰动域几何结构, 并对领域自适应扰动进行建模. 在此基础上, 形式化地定义3种新型鲁棒性概念: 椭球鲁棒性、掩码局部鲁棒性以及马氏距离鲁棒性, 并提出了相应的鲁棒性验证问题的定义与构建方法. 此外, 设计NNV4RADAP算法, 通过构建等价的均匀Lp范数球鲁棒性验证问题来将现有的验证算法推广到面向领域自适应扰动的神经网络鲁棒性验证问题上. 实验结果显示, NNV4RADAP算法可以为神经网络提供更为精准且贴合数据分布特性的鲁棒性保证. 拓宽现有的深度神经网络的鲁棒性的形式定义, 并设计实现面向领域自适应扰动的神经网络鲁棒性的形式验证算法, 研究领域内基于数据分布的鲁棒性定义上的问题, 对于形式验证技术未来在可信人工智能技术中的落地和应用都有指导作用.