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

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:April 08,2025
  • Revised:July 18,2025
  • Adopted:
  • Online: March 25,2026
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063