面向领域自适应扰动的神经网络鲁棒性形式验证
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP311

基金项目:

国家自然科学基金(62161146001)


Formal Verification for Neural Network Robustness Against Domain-adaptive Perturbations
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    As a key technology for ensuring the safety and reliability of artificial intelligence (AI) systems, neural network robustness verification can provide formal guarantees for intelligent decision-making. Existing research is generally based on simplified assumptions of isotropic data distributions to develop verification algorithms based on uniform Lp-norm ball neighborhoods. However, this theoretical framework proves inadequate in the face of the real-world complex data characteristics. For instance, different data features exhibit varying influences on model predictions and sensitivities to perturbations; some features are immutable due to physical constraints; complex correlation structures may exist among features. This makes it difficult for verification algorithms based on uniform perturbation domains to accurately model the robustness requirements of the real world for AI systems. To this end, this study proposes a robustness verification framework based on non-uniform perturbation domains. By combining the data distribution characteristics of specific application domains, the study constructs geometrically structured perturbation domains aligned with domain-specific features and model domain-adaptive perturbations. On this basis, it formally defines three novel robustness concepts, including ellipsoidal robustness, masked local robustness, and Mahalanobis distance robustness, and proposes the definition and construction methods for corresponding robustness verification problems. Furthermore, the NNV4RADAP algorithm is designed, which extends existing verification algorithms to neural network robustness verification problems for domain-adaptive perturbations by constructing equivalent uniform Lp-norm ball robustness verification problems. The experimental results demonstrate that the NNV4RADAP algorithm can provide more accurate and datadistribution-aligned robustness guarantees for neural networks. This study expands the existing formal definitions of deep neural network robustness and designs and implements a formal verification algorithm of neural network robustness for domain-adaptive perturbations. Additionally, it researches the problem in data distribution-based robustness definitions and provides guidance for the future implementation and application of formal verification techniques in trustworthy AI technologies.

    参考文献
    相似文献
    引证文献
引用本文

王麒扬,李璟旸,李国强.面向领域自适应扰动的神经网络鲁棒性形式验证.软件学报,,():1-24

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2025-04-08
  • 最后修改日期:2025-07-18
  • 录用日期:
  • 在线发布日期: 2026-03-25
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号