Search

CN-121979626-A - Neural network verification method and system based on node importance and adaptive scheduling

CN121979626ACN 121979626 ACN121979626 ACN 121979626ACN-121979626-A

Abstract

The invention provides a neural network form verification method and system based on node importance and self-adaptive scheduling. The method comprises the steps of firstly, performing symbol interval propagation on a target neural network, identifying unstable nodes with uncertain input, then, dynamically calculating importance scores of each unstable node by integrating the layer depth position of the node in the network and the propagation upper bound of the unstable nodes on output disturbance, further, intelligently screening key nodes and dividing an input domain by adopting a quality and budget two-stage constraint decision mechanism according to the current hardware resource state and node importance, generating subdomains, and finally, dynamically scheduling verification tasks of all subdomains to a computing unit for parallel processing under real-time resource monitoring, and obtaining a final verification conclusion by a reduction result. The invention solves the problem of insufficient resource utilization in the existing verification method by driving resource allocation through importance, and remarkably improves the verification efficiency and precision.

Inventors

  • LI XUEJIAN
  • ZHU WENJIE

Assignees

  • 安徽大学

Dates

Publication Date
20260505
Application Date
20251210

Claims (9)

  1. 1. The neural network verification method based on node importance and adaptive scheduling is characterized by comprising the following steps of: S1, acquiring a neural network model parameter to be verified and a hardware resource characteristic parameter of target computing equipment; S2, performing symbol interval propagation on the neural network on a given input domain, and identifying all unstable nodes according to the relation between the input interval of each node and the linear region of the activation function of each node; S3, aiming at each unstable node, integrating the layer depth position in the network where the unstable node is positioned and the propagation influence of the unstable node on the final output disturbance, and calculating the comprehensive importance score of the node; S4, dynamically selecting a key node set to be divided according to the current available computing resource state and the importance score of each unstable node, dividing a current input domain according to the activation boundary of the selected node, and generating a plurality of subdomains; S5, scheduling each generated subdomain as an independent verification task to a computing unit for parallel verification, and combining verification results of all subdomains to obtain a verification conclusion of an original input domain; And S6, dynamically adjusting the partitioning strategy in the step S4 and the task scheduling in the step S5 by monitoring the state of the computing resource in real time so as to adapt to the hardware load and maximize the resource utilization rate.
  2. 2. The neural network verification method based on node importance and adaptive scheduling according to claim 1, wherein all nodes are classified as stable or unstable by judging whether the input interval of each node crosses the linear region of its activation function.
  3. 3. The node importance and adaptive scheduling-based neural network verification method of claim 1, wherein the node's integrated importance score is calculated by the following means (1) to (3): (1); (2); (3); In formulas (1) to (3): Representing nodes Is a comprehensive importance score of (2); the representation is based on the number of layers Is a position weight of (2); Representing nodes A and b are adjustment indices greater than 0 for controlling the relative weights of the two factors; Representing a summation operation, capturing the current layer To each subsequent layer For simulating slave layers To the output layer Error superposition of all possible paths; representing an attenuation factor for estimating an upper bound of the error amplification factor; Representing nodes I.e. the number of connections to the subsequent layer; Representing nodes A pre-activation value of (2); an upper bound matrix representing the jacobian of the k-th layer function over the nominal input domain; representation matrix Is a matrix measure of (2); For estimating the nonlinear cumulative amplification effect during the propagation of the disturbance from the first layer to the output layer L; Representing the 2-norm of the vector.
  4. 4. The neural network verification method based on node importance and adaptive scheduling according to claim 1, wherein in the step S4, a two-stage adaptive decision partitioning mechanism is adopted, and the method comprises: Quality constraint screening, namely arranging unstable nodes in the current sub-domain according to the descending order of the normalized importance scores of the unstable nodes, and selecting the accumulated importance proportion to reach a preset threshold value Is at least as much as the first The nodes form a theoretical key node set; Budget constraint adjustment, namely introducing the maximum subdomain number based on the theoretical key node set By evaluating the comprehensive evaluation index of each divided node, optimizing and adjusting node selection to ensure that the total number of sub-domains generated by division does not exceed ; The comprehensive evaluation index is calculated by the following formula (4): (4); In formula (4): Representing the comprehensive evaluation index; Representing the expected benefit; representing computational overhead; Representing nodes Is of importance of (2); Representing nodes Is a stable probability of (2); Representing nodes Is a degree of departure of (2); representing the layer at which the node is located To the output layer Is a depth of (c).
  5. 5. The neural network verification method based on node importance and adaptive scheduling according to claim 1, wherein in the step S6, the dynamic adjustment is specifically: real-time monitoring CPU/GPU utilization rate, memory occupation and cache hit rate indexes; when the idle computing resources are monitored, a more aggressive partitioning strategy is adopted to increase the parallelism; when the shortage of memory resources is monitored, a more conservative partitioning strategy is adopted to control the number of subdomains; And according to the computing estimated cost of the subdomain task and the importance of the source node thereof, the tasks are prioritized, and the tasks are dynamically scheduled to different computing units by combining the real-time load information so as to realize load balancing.
  6. 6. A neural network verification system based on node importance and adaptive scheduling, for implementing the neural network verification method based on node importance and adaptive scheduling according to any one of claims 1 to 5, characterized in that the system comprises: the resource sensing and initializing module is used for acquiring and storing the neural network model parameters and the hardware resource parameters; the symbol analysis and node identification module is used for executing symbol interval propagation and identifying unstable nodes; The importance evaluation module is used for calculating the comprehensive importance score of each unstable node; The self-adaptive division decision module is used for deciding key nodes to be divided according to the resource state and the node importance and executing input domain division; The parallel verification engine is used for scheduling and executing verification tasks of all subdomains; And the resource monitoring and dynamic scheduler is used for monitoring the state of hardware resources in real time and dynamically adjusting the strategy of the self-adaptive partition decision module and the task scheduling of the parallel verification engine according to the monitoring result.
  7. 7. The node importance and adaptive scheduling-based neural network verification system of claim 6, wherein the importance assessment module is configured to assess node importance by calculating a position weight and a propagation influence level of a node and combining them to normalize them, wherein the calculation of the propagation influence level utilizes a matrix measure-based disturbance propagation upper bound estimate.
  8. 8. The node importance and adaptive scheduling based neural network verification system of claim 6, wherein the adaptive partitioning decision module comprises: the key node screening unit is used for screening high-value nodes according to the accumulated importance threshold; And the budget constraint coordination unit is used for optimizing and adjusting the screened node set under the overall subdomain number budget by comprehensively evaluating expected benefits and calculation expenses of the nodes to form a final division decision.
  9. 9. The node importance and adaptive scheduling based neural network verification system of claim 6, wherein the resource monitoring and dynamic scheduler cooperates with the adaptive partitioning decision module and the parallel verification engine through an event driven mechanism to form a closed loop optimization, enabling the system to adapt to different hardware platforms from embedded devices to a server cluster.

Description

Neural network verification method and system based on node importance and adaptive scheduling Technical Field The invention relates to the technical field of formal verification of neural networks, in particular to a neural network verification method based on node importance and adaptive scheduling. Background Currently, neural networks have been widely used in key fields such as computer vision, natural language processing, and autopilot. However, neural networks often exhibit unpredictable vulnerability due to their complex nonlinear characteristics, and for example, applying small, human-imperceptible perturbations (challenge samples) to the input may result in catastrophic errors in the network output. This unreliability severely constrains the deployment of neural networks in security critical systems. Thus, formal verification techniques have evolved that aim to prove or certify that a network output meets certain security attributes (e.g., output range, class invariance) within a given input perturbation range by strict mathematical methods. The existing neural network form verification methods are mainly divided into two main categories, namely an accurate method and an extensible approximation method. The accurate method (such as solving based on mixed integer linear programming MILP) can give deterministic verification conclusion, but the calculation complexity grows exponentially with the network scale, and is difficult to apply to the actual scale network. To balance scalability and authentication capabilities, approximation methods based on symbol interval propagation (Symbolic Interval Propagation, SIP) and linear relaxation (Linear Relaxation, LR) such as sip+lr, deep poly, etc. are mainstream. Such methods can verify larger scale networks by symbolically computing interval boundaries that propagate input uncertainty and conservatively linearly relaxing nonlinear activation functions (e.g., reLU) to preserve manageability. However, the existing approximation method has the following two interrelated fundamental bottlenecks: The problem of accumulation and amplification of linear relaxation errors is that when linear relaxation is performed on the activation function, unavoidable over-approximation errors are introduced. In deep networks, such errors can be progressively amplified by inter-layer propagation, resulting in too loose boundaries of the final output interval, with the validation conclusion being conservative or even meaningless (i.e., low "validation accuracy"). Although methods like DeepPoly attempt to dynamically select a tighter relaxation regime, they fail to radically change the inherent drawback of error accumulation with network depth. The problem of insufficient utilization of hardware resources and strategy mismatch is a key bottleneck which restricts the improvement of verification precision. The prior method generally adopts a strategy of 'uniformly dividing' an input domain or all unstable nodes so as to exchange a more compact interval by increasing the calculated amount. However, this strategy has serious drawbacks: The difference of node influence is not considered, and the contribution degree of each node in the network to the final output error is huge. Even partitioning consumes a significant amount of precious computing resources (CPU/GPU cycles, memory bandwidth) on secondary nodes that have little impact on the validation results, while truly critical, dominant error amplification nodes do not receive sufficient computational attention. Is disjoint from hardware characteristics, and modern computing devices (such as multi-core CPU and massive parallel GPU) have strong parallel computing capability and hierarchical storage architecture. The task load generated by uniform division is often unbalanced, and the task load cannot be matched with the characteristics of parallel granularity, cache locality and the like of hardware, so that the multi-core is idle, the memory bandwidth cannot be saturated, and the advanced hardware potential cannot be effectively mined. For example, a large number of lightweight sub-domain tasks may not take full advantage of the MASSIVELY PARALLEL characteristics of the GPU, and complex tasks may in turn cause a single compute unit to be overloaded. Therefore, the core contradiction of the current neural network form verification method is that an adaptive and accurate cooperative mechanism is lacking between calculation division required for improving verification accuracy and how to efficiently and intelligently utilize limited hardware calculation resources. The existing method does not consider the difference of the influence of the nodes on the errors due to the partitioning strategy, so that huge waste of calculation resources is caused, and the improvement of verification accuracy meets the bottleneck formed by low utilization efficiency of the resources. Disclosure of Invention The invention aims to provide a neural network ve