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.