Satoshi Munakata

Caterina Urban

Haruki Yokoyama

Koji Yamamoto

Kazuki Munakata

Verifying Attention Robustness of Deep Neural Networks against Semantic Perturbations

Keywords: feed-forward ReLU neural networks, robustness certification, semantic perturbations, saliency-map consistency, traversing

It is known that deep neural networks (DNNs) classify an input image by paying particular attention to certain specific pixels; a graphical representation of the magnitude of attention to each pixel is called a saliency-map. Saliency-maps are used to check the validity of the classification decision basis, e.g., it is not a valid basis for classification if a DNN pays more attention to the background rather than the subject of an image. Semantic perturbations can significantly change the saliency-map. In this work, we propose the first verification method for attention robustness, i.e., the local robustness of the changes in the saliency-map against combinations of semantic perturbations. Specifically, our method determines the range of the perturbation parameters (e.g., the brightness change) that maintains the difference between the actual saliency-map change and the expected saliency-map change below a given threshold value. Our method is based on activation region traversals, focusing on the outermost robust boundary for scalability on larger DNNs. Experimental results demonstrate that our method can show the extent to which DNNs can classify with the same basis regardless of semantic perturbations and report on performance and performance factors of activation region traversals.

Introduction

Classification Robustness. Deep neural networks (DNN) are dominant solutions in image classification [START_REF] Krizhevsky | Imagenet classification with deep convolutional neural networks[END_REF]. However, quality assurance is essential when DNNs are used in safety-critical systems, for example, cyber-physical systems such as self-driving cars and medical diagnosis [START_REF] Ashmore | Assuring the machine learning lifecycle: Desiderata, methods, and challenges[END_REF]. From an assurance point of view, the robustness of the classification against input perturbations is one of the key properties, and thus, it has been studied extensively [11]. [4,[START_REF] Gao | Fuzz testing based data augmentation to improve robustness of deep neural networks[END_REF] reported that despite input images can be perturbed in the real world by various mechanisms, such as brightness change and translation; even small semantic perturbations can change the classification labels for DNNs. Therefore, it is essential to verify classification robustness against semantic perturbations. Several methods have already been proposed to compute the range of perturbation parameters (e.g., the amount of brightness change and translation) that do not change classification labels [START_REF] Balunovic | Certifying geometric robustness of neural networks[END_REF][START_REF] Mohapatra | Towards verifying robustness of neural networks against a family of semantic perturbations[END_REF]. Classification Validity. It is known that DNNs classify an input image by paying particular attention to certain specific pixels in the image; a graphical representation of the magnitude of attention to each pixel, like a heatmap, is called saliency-map [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF][START_REF] Sundararajan | Axiomatic attribution for deep networks[END_REF]. A saliency-map can be obtained from the gradients of DNN outputs with respect to an input image, and it is used to check the validity of the classification decision basis. For instance, if a DNN classifies the subject type by paying attention to a background rather than the subject to be classified in an input image (as in the case of "Husky vs. Wolf [19]"), it is not a valid basis for classification. We believe that such low validity classification should not be accepted in safety-critical situations, even if the classification labels are correct. Semantic perturbations can significantly change the saliency-maps [17,[START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF][START_REF] Han | Explanation consistency training: Facilitating consistency-based semi-supervised learning with interpretability[END_REF]. However, existing robustness verification methods only target changes in the classification labels and not the saliency-maps. Our Approach: Verifying Attention Robustness. In this work, we propose the first verification method for attention robustness, i.e., the local robustness of the changes in the saliency-map against combinations of semantic perturbations. Specifically, our method determines the range of the perturbation parameters (e.g., the brightness change) that maintains the difference between (a) the actual saliency-map change and (b) the expected saliency-map change below a given threshold value. Regarding the latter (b), brightness change keeps the saliency-map unchanged, whereas translation moves one along with the image. Although the concept of such difference is the same as saliency-map consistency used in semi-supervised learning [START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF][START_REF] Han | Explanation consistency training: Facilitating consistency-based semi-supervised learning with interpretability[END_REF], for the sake of verification, it is necessary to calculate the minimum and maximum values of the difference within each perturbation parameter sub-space. Therefore, we focus on the fact that DNN output is linear with respect to DNN input within an activation region [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF]. That is, the actual saliency-map calculated from the gradient is constant within each region; thus, we can compute the range of the difference by sampling a single point within each region if the saliency-map is expected to keep, while by convex optimization if the saliency map is expected to move. Our method is based on traversing activation regions on a DNN with layers for classification and semantic perturbations; it is also possible to traverse (i.e., verify) all activation regions in a small DNN or traverse only activation regions near the outermost robust boundary in a larger DNN. Experimental results demonstrate that our method can show the extent to which DNNs can classify with the same basis regardless of semantic perturbations and report on performance and performance factors of activation region traversals. Contributions. Our main contributions are:

-We formulate the problem of attention robustness verification; we then propose a method for verifying attention robustness for the first time. Using our method, it is also possible to traverse and verify all activation regions or only ones near the outermost decision boundary. -We implement our method in a python tool and evaluate it on DNNs trained with popular datasets; we then show the specific performance and factors of verifying attention robustness. In the context of traversal verification methods, we use the largest DNNs for performance evaluation.

Overview

Situation. Suppose a situation where we have to evaluate the weaknesses of a DNN for image classification against combinations of semantic perturbations caused by differences in shooting conditions, such as lighting and subject position. For example, as shown in Figure 1, the original label of the handwritten text image is "0"; however, the DNN often misclassifies it as the other labels, with changes in brightness, patch, and translations. Therefore, we want to know in advance the ranges of semantic perturbation parameters that are likely to cause such misclassification as a weakness of the DNN for each typical image. However, classification robustness is not sufficient for capturing such weaknesses in the following cases. Case 1. Even if the brightness changes so much that the image is not visible to humans, the classification label of the perturbed image may happen to match the original label. Then vast ranges of the perturbation parameters are evaluated as robust for classification; however, such overestimated ranges are naturally invalid and unsafe. For instance, Figure 2 shows the changes in MNIST image "8" and the actual saliency-map when the brightness is gradually changed; although the classification seems robust because the labels of each image are the same, the collapsed saliency-maps indicate that the DNN does not pay proper attention to text "8" in each image. Therefore, our approach uses the metric attention inconsistency, which quantifies the degree of collapse of a saliency-map, to further evaluate the range of the perturbation parameter as satisfying the property attention robustness; i.e., the DNN is paying proper attention as well as the original image. Attention inconsistency is a kind of distance (cf. Figure 4) between an actual saliency-map (second row) and an expected one (third row); e.g., the saliency-map of DNN-1 for translation perturbation (column (T)) is expected to follow image translation; however, if it is not, then attention inconsistency is high. In addition, Figure 2 shows an example of determining that attention robustness is satisfied if each attention inconsistency value (third row) is less than or equal to threshold value δ. Case 2. The classification label often changes by combining semantic perturbations, such as brightness change and patch, even for the perturbation parameter ranges that each perturbation alone could be robust. It is important to understand what combinations are weak for the DNN; however, it is difficult to verify all combinations as there are many semantic perturbations assumed in an operational environment. In our observations, a perturbation that significantly collapses the saliency-map is more likely to cause misclassification when combined with another perturbation because another perturbation can change the intensity of pixels to which the DNN should not pay attention. Therefore, to understand the weakness of combining perturbations, our approach visualizes the outermost boundary at which the sufficiency of robustness switches on the perturbation parameter space. For instance, Figure 3 shows connected regions that contain the outermost boundary for classification robustness (left side) or attention robustness (right side). The classification boundary indicates that the DNN can misclassify the image with a thin patch and middle brightness. In contrast, the attention boundary further indicates that the brightness change can collapse the saliency-map more than patching, so we can see that any combinations with the brightness change pose a greater risk. Even when the same perturbations are given, the values of attention inconsistency for different DNNs are usually different (cf. Figure 4); thus, it is better to evaluate what semantic perturbation poses a greater risk for each DNN.

Problem Formulation

Our method targets feed-forward ReLU-activated neural networks (ReLU-FNNs)

for image classification. A ReLU-FNN image classifier is a function f : X → Y mapping an N f -dimensional (pixels × color-depth) image x ∈ X ⊆ R N f to a classification label argmax j∈Y f j (x) in the K f -class label space Y = {1, . . . , K f },
where f j : X → R is the confidence function for the j-th class.

The ReLU activation function occurs in between the linear maps performed by the ReLU-FNN layers and applies the function max(0, x l,n ) to each neuron x l,n in a layer l ∈ L f (where L f is the number of layers of ReLU-FNN f ). When x l,n > 0, we say that x l,n is active; otherwise, we say that x l,n is inactive. We write ap f (x) for the activation pattern of an image x given as input to a ReLU-FNN f , i.e., the sequence of neuron activation statuses in f when x is taken as input. We write AP f for the entire set of activation patterns of a ReLU-FNN f .

Given an activation pattern p ∈ AP f , we write ar f (p) for the corresponding activation region, i.e., the subset of the input space containing all images that share the same activation pattern: x ∈ ar f (p) ⇔ ap f (x) = p. Note that, neuron activation statuses in an activation pattern p yield half-space constraints in the input space [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF][START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF]. Thus, an activation region ar f (p) can equivalently be represented as a convex polytope described by the conjunction of the half-space constraints resulting from the activation pattern p. Classification Robustness. A semantic perturbation is a function g : Θ×X → X applying a perturbation with

N g parameters θ ∈ Θ ⊆ R N g to an image x ∈ X to yield a perturbed image g(θ, x) def = g N g (θ N g , •) • • • • • g 1 (θ 1 , x) = g N g (θ N g , . . . g 1 (θ 1 , x), . . . ) ∈ X,
where g i : R × X → X performs the i-th atomic semantic perturbation with parameter θ i (with g i (0, x) = x for any image x ∈ X). For instance, a brightness decrease perturbation g b is a(n atomic) semantic perturbation function with a single brightness adjustment parameter β ≥ 0:

g b (β, x) def = ReLU (x -1β).
Definition 1 (Classification Robustness). A perturbation region η ⊂ Θ satisfies classification robustness -written CR(x; η) -if and only if the classification label f (g(θ, x)) is the same as f (x) when the perturbation parameter θ is within η: CR(x; η) def = ∀θ ∈ η. f (x) = f (g(θ, x)).

Vice versa, we define misclassification robustness when f (g(θ, x)) is always different from f (x) when θ is within η: M R(x; η) def = ∀θ ∈ η. f (x) = f (g(θ, x)).

The classification robustness verification problem P rob CR def = (f, g, x0, Θ) consists in enumerating, for a given input image x0, the perturbation parameter regions η CR , η M R ⊂ Θ respectively satisfying CR(x0; η CR ) and M R(x0; η M R ).

Attention Robustness. We generalize the definition of saliency-map from [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF] to that of an attention-map, which is a function map j : X → X from an image x ∈ X to the heatmap image m j ∈ X plotting the magnitude of the contribution to the j-th class confidence f j (x) for each pixel of x. Specifically,

map j (x) def = f ilter ∂fj (x) ∂x1 , . . . , ∂fj (x)
∂x N f , where f ilter(•) is an arbitrary image processing function (such as normalization and smoothing) and, following [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF]28], the magnitude of the contribution of each pixel x 1 , . . . , x N f is given by the gradient with respect to the j-th class confidence. When f ilter(x) def = |x|, our definition of map j matches that of saliency-map in [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF]. Note that, within an activation region ar f (p), f j is linear [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF] and thus the gradient

∂fj (x)
∂xi is a constant value. We expect attention-maps to change consistently with respect to a semantic image perturbation. For instance, for a brightness change perturbation, we expect the attention-map to remain the same. Instead, for a translation perturbation, we expect the attention-map to be subject to the same translation. In the following, we write g(•) for the attention-map perturbation corresponding to a given semantic perturbation g(•). We define attention inconsistency as the difference between the actual and expected attention-map after a semantic perturbation:

ai(x; θ) def = j∈Y dist map j g(θ, x) , g θ, map j (x)
where dist : X × X → R is an arbitrary distance function such as Lp-norm (||x -x || p ). Note that, when dist(•) is L2-norm, our definition of attention inconsistency coincides with the definition of saliency-map consistency given by [START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF].

Definition 2 (Attention Robustness).

A perturbation region η ⊂ Θ satisfies attention robustness -written AR(x; η, δ) -if and only if the attention inconsistency is always less than or equal to δ when the perturbation parameter θ is within η: AR(x; η, δ) def = ∀θ ∈ η. ai(x; θ) ≤ δ.

When the attention inconsistency is always greater than δ, we have inconsistency robustness: IR(x; η, δ) def = ∀θ ∈ η. ai(x; θ) > δ.

The attention robustness verification problem P rob AR def = (f, g, x0, Θ, δ) consists in enumerating, for a given input image x0, the perturbation parameter regions η AR , η IR ⊂ Θ respectively satisfying AR(x0; η AR , δ) and IR(x0; η IR , δ). Outermost Boundary Verification. In practice, to represent the trend of the weakness of a ReLU-FNN image classifier to a semantic perturbation, we argue that it is not necessary to enumerate all perturbation parameter regions within a perturbation parameter space Θ. Instead, we search the outermost CR/AR boundary, that is, the perturbation parameter regions η that lay on the CR/AR boundary farthest away from the original image.

An illustration of the outermost CR boundary is given in Figure 5. More formally, we define the outermost CR boundary as follows:

Definition 3 (Outermost CR Boundary). The outermost CR boundary of a classification robustness verification problem, ob CR (P rob CR ), is a set of perturbation parameter regions HS ⊂ P(Θ) such that:

1. for all perturbation regions η ∈ HS, there exists a path connected-space from the original image x0 (i.e., 0 ∈ Θ) to η that consists of regions satisfying CR (written Reachable(η; x0)); 2. all perturbation regions η ∈ HS lay on the classification boundary, i.e., ∃θ,

θ ∈ η. f (g(θ, x0)) = f (x0) ∧ f (g(θ , x0)) = f (x0); 3.
there exists a region η ∈ HS that contains the farthest reachable perturbation parameter point θ from the original image, i.e., θ = max θ∈Θ ||θ|| 2 such that Reachable({θ}; x0).

The definition of the outermost AR boundary is analogous. Note that not all perturbation regions inside the outermost CR/AR boundary satisfy the CR/AR property (cf. the enclaves in Figure 5). The outermost CR boundary verification problem and outermost AR boundary verification problem P rob CR ob = (f, g, x0, Θ) and P rob AR ob = (f, g, x0, Θ, δ) consist in enumerating, for a given input image x0, the perturbation parameter regions η CR ob and η AR ob ) that belong to the outermost CR and AR boundary ob CR (P rob CR ) and ob AR (P rob AR ).

Geometric Boundary Search (GBS )

In the following, we describe our Geometric Boundary Search (GBS ) method for solving P rob CR ob , and P rob AR ob shown in Algorithm 1 and 2. In Appendix I.8, we also describe our Breadth-First Search (BFS ) method for solving P rob CR , and P rob AR .

Encoding Semantic Perturbations

After some variables initialization (cf. Line 1 in Algorithm 1), the semantic perturbation g is encoded into a ReLU-FNN g x0 : Θ → X (cf. Line 2).

In this paper, we focus on combinations of atomic perturbations such as brightness change (B), patch placement (P), and translation (T). Nonetheless, our method is applicable to any semantic perturbation as long as it can be represented or approximated with sufficient accuracy.

For the encoding, we follow [START_REF] Mohapatra | Towards verifying robustness of neural networks against a family of semantic perturbations[END_REF] and represent (combinations of) semantic perturbations as a piecewise linear function by using affine transformations and ReLUs. For instance, a brightness decrease perturbation g b (β, x0) def = ReLU (x0-1β) (cf. Section 3) can be encoded as a ReLU-FNN as follows:

g b (β, x0) encode -→     1 0 . . . 0 0 1 . . . 0 . . . 0 0 . . . 1     ReLU         -1 1 0 . . . 0 -1 0 1 . . . 0 . . . -1 0 0 . . . 1         β x0 1 . . . x0 N f         + 0
which we can combine with the given ReLU-FNN f to obtain the compound ReLU-FNN f • g x0 b to verify. The full encoding for all considered (brightness, patch, translation) perturbations is shown in Appendix I.5.

Traversing Activation Regions.

GBS then performs a traversal of activation regions of the compound ReLU-FNN f •g x0 near the outermost CR/AR boundary for P rob CR ob /P rob AR ob . Specifically, it initializes a queue Q with the activation pattern ap f •g x0 ( 0) of the original input image x0 with no semantic perturbation, i.e., θ = 0 (cf. Line 3 in Algorithm 1, we explain the other queue initialization parameters shortly). Given a queue element q ∈ Q, the functions p(q), isF ollowing(q), and lineDistance(q) respectively return the 1st, 2nd, and 3rd element of q.

Then, for each activation pattern p in Q (cf. Line 6), GBS reconstructs the corresponding perturbation parameter region η (subroutine constructActivation-Region, Line 7) as the convex polytope resulting from p (cf. Section 3 and η in Figure 6-(1a)).

Next, for each neuron x l,n in f • g x0 (cf. Line 11), it checks whether its activation status cannot flip within the perturbation parameter space Θ, i.e., the resulting half-space has no feasible points within Θ (subroutine isStable, Line 12, cf. half-space h 1,5 in Figure 6-(1a)). Otherwise, a new activation pattern p is constructed by flipping the activation status of x l,n (subroutine flipped, Line 13) and added to a local queue Q (cf. Line 9, and 23, 25) if p has not been observed already (cf. Line 14) and it is feasible (subroutine calcInterior-PointOnFace, Lines 15-16. cf. point θ F and half-space h 1,2 in Figure 6-(1a)).

The perturbation parameter region η is then simplified to η (subroutine simplified, Line 2 in Algorithm 2; e.g., reducing the half-spaces used to represent η to just h 1,2 and h 1,3 in Figure 6-(1a)). η is used to efficiently calculate the range of attention inconsistency within η (subroutine calcRange, Line 3 in Algorithm 2, cf. Section 4.4), and then attention/inconsistency robustness can be verified based on the range (Line 5 and 8 in Algorithm 2). Furthermore, classification/misclassification robustness can be verified in the same way if subroutine calcRange returns the range of confidence f f (x0) (g x0 (θ)) -f j (g x0 (θ)) within η (cf. Section 4.4) and δ = 0 ∧ w δ = 0. At last, the local queue Q is pushed onto Q (cf. Line 29 in Algorithm 1).

To avoid getting stuck around enclaves inside the outermost CR/AR boundary (cf. Figure 5) during the traversal of activation regions, GBS switches status when needed between "searching for a decision boundary" and "following a found decision boundary". The initial status is set to "searching for a decision boundary", i.e., ¬isF ollowing when initializing the queue Q (cf. Line 3). The switch to isF ollowing happens when region η is on the boundary (i.e., lo ≤ δ ≤ up) or near the boundary (i.e., δ -w δ ≤ lo ≤ δ + w δ , cf. Line 15 in Algorithm 2 and Figure 6-(3a,1b,3b)); where w δ is a hyperparameter to determine whether close to the boundary or not. w δ should be greater than 0 to verify attention/inconsistency robustness because attention inconsistency changes discretely for ReLU-FNNs (ch. Section 4.3). GBS can revert back to searching for a decision boundary if when following a found boundary it finds a reachable perturbation parameter region that is farther from 0 (cf. Lines 19-20 in Algorithm 1 and Figure 6-(2b)).

Calculating Attention Inconsistency

Gradients within an Activation Region. Let p ∈ AP f •g x0 be an activation pattern of the compound ReLU-FNN f • g x0 . The gradient

∂fj (g x0 (θ)) ∂θs is constant within ar f •g x0 (p) (cf. Section 3). We write g x0 i (θ) for the i-th pixel x i of a perturbed image in {g x0 (θ) | θ ∈ ar f •g x0 (p)} ⊂ X. The gradient ∂g x0 i ∂θ = ∂xi
∂θ is also a constant value. By the chain rule, we have

∂fj (x) ∂xi = ∂fj (g x0 (θ))/∂θs ∂xi/θs . Thus ∂fj (x)
∂xi is also constant. This fact is formalized by the following lemma:

Lemma 1. ∂fj (x) ∂xi = C (x ∈ {g x0 (θ) | θ ∈ ar f •g x0 (p)})
(cf. a small example in Appendix I.7). Therefore, the gradient

∂fj (x)
∂xi can be computed as the weights of the j-th class output for ReLU-FNN f about activation pattern ap f ( ẋ); where, ẋ = g x0 ( θ) and θ is an arbitrary sample within ar q ← popM axLineDistance(Q); p ← p(q); OBS ← OBS ∪ {p} 7:

Q ⊂ AP f •g x0 × B × R ← {(ap f •g x0 ( 0), ⊥, 0)} //
η ← constructActivationRegion(f • g x0 , p) 8: F S ⊂ Z × Z ← {} // (l, n) means the n-th neuron in l-th layer is a face of η 9: Q ⊂ AP f •g x0 × B × R ← {} //
F S ← F S ∪ {(l, n)} // (l,n) is a face of η. 18: θ L ← calcInteriorP ointOnLine(η, l, n) 19: if isF ollowing(q) ∧ θ L = null ∧ ||θ L ||2 > lineDistance(q) then 20:
q ← (p, ⊥, lineDistance(q)) // Re-found the line in boundary-following.

21:

end if 22:

if ¬isF ollowing(q) ∧ θ L = null then 23:

Q ← Q ∪ {(p , ⊥, ||θ L ||2)} // continue line-search.

24:

else 25:

Q ← Q ∪ {(p , isF ollowing(q), lineDistance(q))} // continue current.

26:

end if 27:

end for 28:

(...Verify η...) // See Algorithm 2 for AR/IR (analogous for CR/M R) 29:

Q ← Q ∪ Q // Push 30: end while
For the perturbed gradient g(θ, ∂fj (x) ∂xi ), let g(θ) be the ReLU-FNN g ∂f j (x) ∂x i (θ ). Thus, the same consideration as above applies. Attention Inconsistency (ai). We assume both f ilter(•) and dist(•) are convex downward functions for calculating the maximum / minimum value by convex optimization. Specifically, f ilter(•) is one of the identity function (I), the absolute function (A), and the 3 × 3 mean filter (M). dist(•) is one of the L 1norm (L 1 ) and the L 2 -norm (L 2 ): where, w is the width of image x ∈ X.

Verifying CR and AR within an activation region

Our method leverages the fact that the gradient of a ReLU-FNN output with respect to the input is constant within an activation region (cf. Section 3); thus, Algorithm 2 (Expanding from Algorithm 1 for AR(x0; η, δ)/IR(x0; η, δ)) 1: (...Verify η...) 2: η ← simplif ied(η, F S) // limit the constraints on η to F S. (...Update Q such that ∀q ∈ Q. isF ollowing(q )...) // switch to boundaryfollowing. 16: end if CR/M R can be resolved by linear programming, and AR/IR can be resolved by just only one sampling if the saliency-map is expected to keep or convex optimization if the saliency-map is expected to move. Verifying CR/MR. When x0 is fixed, each activation region of the ReLU-FNN f (g(θ, x0)) : Θ → Y is a region in the perturbation parameter space Θ. Within an activation region η ⊂ Θ of the ReLU-FNN f (g(θ, x0)), CR(f, g, x0, η) is satisfied if and only if the ReLU-FNN output corresponding to the label of the original image x0 cannot be less than the ReLU-FNN outputs of all other labels, i.e., the following equation holds: min j∈Y \{f (x0)},θ∈η f f (x0) (x) -f j (g(θ, x0)) > 0 ⇔ CR(f, g, x0, η) Each DNN output f j (g(θ, x0)) is linear within η, and thus, the left-hand side of the above equation can be determined soundly and completely by using an LP solver (Eq. 3-(c) in Appendix I.1), such as scipy.optimize.linprog 3 . Similarly, M R(f, g, x0, η) is satisfied if and only if the ReLU-FNN output corresponding to the label of the original image x0 cannot be greater than the ReLU-FNN outputs of any other labels. Verifying AR/IR. Within an activation region η ⊂ Θ of the ReLU-FNN f (g(θ, x0)), AR(f, g, x0, η, δ) is satisfied if and only if the following equation holds: max θ∈η ai(θ, x0) ≤ δ ⇔ AR(f, g, x0, η, δ) If f ilter(•) and dist(•) are both convex downward functions, as the sum of convex downward functions is also a convex downward function, the left-hand side of the above equation can be determined by comparing the values at both ends. On the other hand, IR(f, g, x0, η, δ) is satisfied if and only if the following equation holds: min θ∈η ai(θ, x0) > δ ⇔ IR(f, g, x0, η, δ) The left-hand side of the above equation can be determined by Fig. 6. A running example of GBS. The upper row shows the basic traversing flow, while the lower row shows the flow of avoiding enclaves. h l,n denotes a half-space corresponding to neuron activity p l,n .

← (lo ≤ δ ≤ up) ∨ (δ -w δ ≤ lo ≤ δ + w δ ) ∨ (δ -w δ ≤ up ≤ δ + w δ ) 5: if lo ≤ up ≤ δ /*
Table 1. The ReLU-FNNs we used in the experiments: where, "Conv" and "FC" in column Layers denote convolutional and fully connected layers, respectively. using an convex optimizer, such as scipy.optimize.minimize 4 Note that if the saliency-map is expected to keep against perturbations, the above optimization is unnecessary because ai(θ ∈ eta, x0) is constant.

Experimental Evaluation

To confirm the usefulness of our method, we conducted evaluation experiments.

Setups.

Infrastructure (ABCI) 5 provided by National Institute of Advanced Industrial Science and Technology (AIST).

We implemented our method in a python tool for evaluation; in addition, we will make the tool available at https://zenodo.org/record/65449056 . RQ1: How much computation time is required to solve each problem? For each ReLU-FNN, we measured the computation time of algorithms GBS and BFS with 10 images selected from the end of each dataset (i.e., Indexes 69990-69999. These images were not used in the training of any ReLU-FNNs). GBS also distinguishes between gbs-CR that traverses the CR boundary, gbs-AR that traverses the AR boundary, and gbs-CRAR that traverses the boundary of the regions satisfying both CR and AR. Furthermore, we measured above per the combinations of semantic perturbations (BP), (TP), and (TB) that denote "brightness change / patch", "translation / patch", and "translation / brightness change", respectively. We used the definitions f ilter(x) def = x, dist(x, x ) def = ||xx || 2 , δ def = 3.0, and w δ = 0.2.

Figure 7-(C) shows the trend of increasing computation time with increasing the number of neurons for each algorithm as a box plot on a log scale. Note that each verification timed out at 2 hours, and thus, the upper limit of computation time (y-axis) was 7,200 seconds. We can see that algorithm BFS took more computation time than GBS. Figure 7-(D) shows the number of verified activation regions for each combination of perturbations; we can see that GBS reduced the number of regions to traverse compared to BFS as intended.

However, we can also see that gbs-AR took longer to traverse more activation regions than gbs-CR. Figure 7-(A) and (B) show the breakdown of each verification result for gbs-AR and gbs-CR; where, blue, red, gray, and black bars denote robust, not-robust, timed out, and out-of-memory, respectively. The figures show that gbs-AR timed out at a higher rate for smaller size DNNs than gbs-CR.

Moreover, we can also see that the median computation time increased exponentially with the number of neurons for all algorithms in Figure 7-(C). This result suggests that exact verification-based traversing is not applicable to practical-scale DNNs such as VGG16 [START_REF] Simonyan | Very deep convolutional networks for large-scale image recognition[END_REF], and fundamental scalability improvement measures, such as incorporating approximate verification, are needed. RQ2: What are the performance factors? Figure 7-(E) and (F) show the correlation between computation time and the number of verified activation regions and the number of face checking as scatter plots, respectively: where the results of experiments that timed out are excluded. The figures show strong positive correlations for each DNN size (the number of neurons), especially in the number of face checking; thus, reducing redundant regions and faces in understanding the boundaries should directly reduce verification time. For example, Figure 7-(G) shows an example of verifying activation regions near the AR boundary too extensively due to large hyperparameter w θ = 0.2. Like gbs-CR, AR boundary also needs to be able to narrow down the search to only the regions on the AR boundaries.

Discussion

Internal Validity. Using the outermost CR/AR boundary as a trend of weakness to a combination of semantic perturbations, not all regions inside the outermost CR/AR boundary satisfy the CR/AR property. Unlike CR, AR requires hyperparameters δ, w δ ∈ R; however, there are no clear criteria for setting them. External Validity. We focus here on brightness change, patch, and translation perturbations. Still, our method applies to any semantic perturbations as long as they can be represented or approximated with sufficient accuracy. Our method is not applicable to a semantic perturbation g for which a corresponding saliencymap change g cannot be defined and computed, e.g., DNNs that generate an image from an input text (such as [START_REF] Ramesh | Zero-shot text-to-image generation[END_REF]). Our method has not supported the MaxPool layer of CNNs [START_REF] Krizhevsky | Imagenet classification with deep convolutional neural networks[END_REF].

Performance Bottlenecks.

The computation time increases exponentially with the number of ReLU-FNN neurons. Thus, our current method is not yet applicable on a practical scale, such as VGG16 [START_REF] Simonyan | Very deep convolutional networks for large-scale image recognition[END_REF]. If it is difficult to enumerate all activation regions, GBS traverses only regions on the outermost boundary. In the future, it may be better to use ReLU relaxation for dense areas.

Related Work

Robustness Verification. To the best of our knowledge, there have been no reports that formulate the attention robustness verification problem or that propose the method for such problem; e.g., [11,[START_REF] Urban | A review of formal methods applied to machine learning[END_REF][START_REF] Ashmore | Assuring the machine learning lifecycle: Desiderata, methods, and challenges[END_REF]. [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] first verified robustness against image rotation, and [START_REF] Balunovic | Certifying geometric robustness of neural networks[END_REF] verified robustness against more semantic perturbations, such as image translation, scaling, shearing, brightness change, and contrast change. However, in this paper, we have demonstrated that attention robustness more accurately captures trends in weakness for the combinations of semantic perturbations than existing classification robustness in some cases. In addition, As [START_REF] Sotoudeh | Provable repair of deep neural networks[END_REF] reported, approximated verification methods like DeepPoly [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] fail to verify near the boundary. In contrast, our GBS enables verification near the boundary by exploratory and exact verification. [START_REF] Mohapatra | Towards verifying robustness of neural networks against a family of semantic perturbations[END_REF] proposed that any Lp-norm-based verification tools can be used to verify the classification robustness against semantic perturbations by inserting special DNN layers that induce semantic perturbations in the front of DNN layers for classification. In order to transform the verification problem on the inherently high-dimensional input image space X into one on the low-dimensional perturbation parameter space Θ, we adopted their idea, i.e., inserting DNN layers for semantic perturbations (Θ → X) in front of DNN layers for classification (X → Y ). However, it is our original idea to calculate the value range of the gradient for DNN output (∂f j (g(θ, x i ))/∂x i ) within an activation region on the perturbation parameter space (cf. Sections 4.3-4.4). Traversing activation regions. Since [START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF] first proposed the method to traverse activation regions, several improvements and extensions have been proposed [START_REF] Lim | Hierarchical verification for adversarial robustness[END_REF][START_REF] Fromherz | Fast geometric projections for local robustness certification[END_REF]. All of them use all breadth-first searches with a priority queue to compute the maximum safety radius or the maxima of the given objective function in fewer iterations. In contrast, our algorithm GBS uses a breadth-first search with a priority queue to reach the outermost CR/AR boundary in fewer iterations while avoiding enclaves.

[5] responded to the paper reviewer that traversing time would increase exponentially with the size of a DNN7 . Our experiment also showed that larger DNNs increase traversing time due to the denser activation regions. The rapid increase in the number of activation regions will be one of the biggest barriers to the scalability of traversing methods, including our method. Although the upper bound theoretical estimation for the number of activation regions increases exponentially with the number of layers in a DNN [START_REF] Hinz | An analysis of the piece-wise affine structure of ReLU feed-forward neural networks[END_REF], [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF] reported that actual DNNs have surprisingly few activation regions because of the myriad of infeasible activation patterns. Therefore, it will need to understand the number of activation regions of DNNs operating in the real world.

To improve scalability, there is the method of dividing the input space and verifying each in perfectly parallel [START_REF] Urban | Perfectly parallel fairness certification of neural networks[END_REF]. However, our method has not been fully parallelized yet, because we have focused on accurately calculating the outermost CR/AR boundary and attention robustness in this study. To improve scalability, there are several methods of targeting only low-dimensional subspaces in the high-dimensional input space for verification [24,26,[START_REF] Mirman | Robustness certification with generative models[END_REF]. We have similarly taken advantage of low-dimensionality, e.g., using low-dimensional perturbation parameters to represent high-dimensional input image pixels as mediator variables (i.e., curried perturbation function g x0 (θ) = x ) to reduce the elapsed time of LP solvers, determining the stability of neuron activity from few vertices of perturbation parameter space Θ. Saliency-Map. Since [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF] first proposed the method to obtain a saliency-map from the gradients of DNN outputs with respect to an input image (i.e., ∂f j (x)/∂x i ), many improvements and extensions have been proposed [3,[START_REF] Sundararajan | Axiomatic attribution for deep networks[END_REF][START_REF] Selvaraju | Gradcam: Visual explanations from deep networks via gradient-based localization[END_REF]. We formulated an attention-map primarily using the saliency-map definition by [START_REF] Simonyan | Deep inside convolutional networks: Visualising image classification models and saliency maps[END_REF]. However, it is a future work to formulate attention robustness corresponding to improvements, such as gradient-smoothing [3] and line-integrals [START_REF] Sundararajan | Axiomatic attribution for deep networks[END_REF].

It is known that semantic perturbations can significantly change the saliencymaps [17,[START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF][START_REF] Han | Explanation consistency training: Facilitating consistency-based semi-supervised learning with interpretability[END_REF]. [START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF] first claimed the saliency-map should consistently follow image translation and proposed the method to quantify saliency-map consistency. We formulated attention inconsistency ac primarily using the saliency-map consistency by [START_REF] Guo | Visual consistency under image transforms for multi-label image classification[END_REF].

Conclusion and Future Work

We, for the first time, have presented a verification method for attention robustness based on traversing activation regions on the DNN that contains layers for semantic perturbations and layers for classification. Attention robustness is the property that the saliency-map consistency is less than a threshold value. We have demonstrated that attention robustness more accurately captures trends in weakness for the combinations of semantic perturbations than existing classification robustness. Although the performance evaluation presented in this study is not yet on a practical scale, such as VGG16 [START_REF] Simonyan | Very deep convolutional networks for large-scale image recognition[END_REF], we believe that the attention robustness verification problem we have formulated opens a new door to quality assurance for DNNs. We plan to increase the number of semantic perturbation types that can be verified and improve scalability by using abstract interpretation in future work.

I Appendix

I.1 Linearity of Activation Regions

Given activation pattern p ∈ AP f as constant, within activation region ar f (p) each output of ReLU-FNN f j (x ∈ ar f (p)) is linear for x (cf. Figure 8) because all ReLU operators have already resolved to 0 or x [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF]. i.e., f j (x ∈ ar f (p)) = A j x + b j : where, A j and b j denote simplified weights and bias about activation pattern p and class j. That is, the gradient of each ReLU-FNN output f j (x) Fig. 8. An example of activation regions [START_REF] Hanin | Deep relu networks have surprisingly few activation patterns[END_REF]. ReLU-FNN output is linear on each activation region, i.e., each output plane painted for each activation region is flat.

within activation region ar f (p) is constant, i.e., the following equation holds: where C ∈ R is a constant value.

F easible f (p ∈ AP f ) ⇒ ∂f j (x) ∂x i = C (x ∈ ar f (p)) (1)
An activation region can be interpreted as the H-representation of a convex polytope on input space R N f . Specifically, neuron activity p l,n and p have a one-to-one correspondence with a half-space and convex polytope defined by the intersection (conjunction) of all half-spaces, because f (l) n (x) is also linear when p ∈ AP f is constant. Therefore, we interpret activation region ar f (p) and the following H-representation of convex polytope HConvex f (x; p) each other as needed: where, A and b denote simplified weights and bias about activation pattern p, and A l,n x ≤ b l,n is the half-space corresponding to the n-th neuron activity p l,n in the l-th layer.

HConvex f (x; p) def = A x ≤ b ≡ l,n A l,n x ≤ b l,n (2)

I.2 Connectivity of Activation Regions

When feasible activation patterns p, p ∈ AP f are in a relationship with each other that flips single neuron activity p l,n ∈ {0, 1}, they are connected regions because they share single face HF ace f l,n (x; p) def = A l,n x = b l,n corresponding to flipped p l,n [START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF]. It is possible to flexibly traverse activation regions while ensuring connectivity by selecting a neuron activity to be flipped according to a prioritization; several traversing methods have been proposed [START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF][START_REF] Lim | Hierarchical verification for adversarial robustness[END_REF][START_REF] Fromherz | Fast geometric projections for local robustness certification[END_REF]. However, there are generally rather many neuron activities that become infeasible when flipped [START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF]. For instance, half-spaces h 1,3 is a face of activation region η in Figure 6-(1a); thus, flipping neuron activity p 1,3 , GBS can traverse connected region η in Figure 6-(1b). In contrast, half-space h 1,1 is not a face of activation region η in Figure 6-(1a); thus, flipping neuron activity p 1,1 , the corresponded activation region is infeasible (i.e., the intersection of flipped half-spaces has no area).

I.3 Hierarchy of Activation Regions

When feasible activation patterns p, p ∈ AP f are in a relationship with each other that matches all of L f -th upstream activation pattern p

≤L f def = [p l,n | 1 ≤ l ≤ L f , 1 ≤ n ≤ N f l ] (1 ≤ L f ≤ L f ), they are included parent activa- tion region ar f ≤L f (p) corresponding to convex polytope HConvex f ≤L f (x; p) def = l≤L f ,n A l,n x ≤ b l,n [14]. That is, ∀x ∈ ar f (p). x ∈ ar f ≤L f (p) and ∀x ∈ R N f . HConvex f (x; p) ⇒ HConvex f ≤L f (x; p). Similarly, we define L f -th downstream activation pattern as p ≥L f def = [p l,n | L f ≤ l ≤ L f , 1 ≤ n ≤ N f l ] (1 ≤ L f ≤ L f ).

I.4 Linear Programming on an Activation Region

Based on the linearity of activation regions and ReLU-FNN outputs, we can use Linear Programming (LP) to compute (a) the feasibility of an activation region, (b) the flippability of a neuron activity, and (c) the minimum (maximum) of a ReLU-FNN output within an activation region. We show each LP encoding of the problems (a,b,c) in the SciPy LP form 8 : where, p ∈ AP f is a given activation pattern of ReLU-FNN f , and p l,n is a give neuron activity to be flipped.

(a) ∃x ∈ R N f . HConvex f (x; p) encode -→ min x 0x s.t., A x ≤ b (b) ∃x ∈ R N f . HConvex f (x; p) ∧ HF ace f l,n (x; p) encode -→ min x 0x s.t., A x ≤ b , A l,n x = b l,n (c) min x f j (x) s.t., HConvex f (x; p) encode -→ min x A j x s.t., A x ≤ b + b j (3)

I.5 Full Encoding Semantic Perturbations

. We focus here on the perturbations of brightness change (B), patch (P), and translation (T), and then describe how to encode the combination of them into ReLU-FNN g x0 : Θ → X: where, |θ (l) | = dim θ (l) , w is the width of image x0, px, py, pw, ph are the patch x-position, y-position, width, height, and tx is the amount of movement in x-axis direction. Here, perturbation parameter θ ∈ Θ consists of the amount of brightness change for (B), the density of the patch for (P), and the amount of translation for (T). In contrast, perturbation parameters not included in the dimensions of Θ, such as w, px, py, pw, ph, tx, are assumed to be given as constants before verification.

g(θ, x0) encode -→ g x0 (θ) // currying g with given constant x0.

g x0 (θ) = g (5) (θ • x0) // concat x0 g (1) (µ) = A (T ) µ // translate g (2) (µ) = A (P ) g (1) (µ) // patch g (3) (µ) = A (B) g (2) (µ) // brightness change g (4) (µ) = -ReLU (g (3) (µ)) + 1 // clip max(0, x i ) g (5) (µ) = -ReLU (g (4) (µ)) + 1 // clip min(1, x i )

A (B) = a (B) r,c , A (P ) = a (P ) r,c , A (T ) = a (T ) r,c a (B) r,c =      1 (c = 1 ∧ r ≥ |θ (l+1) |) // add θ (l) 1
1 (c = r + 1) // copy θ (l)
≥2 and x i 0 (otherwise)

a (P ) r,c =      1 (c = 1 ∧ On(r)) // add θ (l) 1
1 (c = r + 1) // copy θ (l)

≥2 and x i 0 (otherwise)

On(r) def = let i := r -|θ (l+1) |. (px ≤ i/w ≤ px + pw) ∧ (py ≤ i mod w ≤ py + ph)
8 https://docs.scipy.org/doc/scipy/reference/generated/scipy.optimize.linprog.html We used 10 images (i.e., Indexes 69990-69999) selected from the end of the MNIST dataset (cf. Figure 9) and the Fashion-MNIST dataset (cf. Figure 10), respectively. We did not use these images in the training of any ReLU-FNNs.

(T ) r,c =              1 (c = r + 1 ∧ r ≤ |θ (l+1) |) // copy θ (l) ≥2 0 (c = 1 ∧ ¬(1 ≤ t(r) ≤ s(r) ≤ N )) //

I.7 An example of Lemma 1

Lemma 1 is reprinted below.

I.8 Algorithm BFS

Algorithm BFS traverses entire activation regions in perturbation parameter space Θ, as shown in Figure 12.

Algorithm BFS initializes Q with ap f •g x0 ( 0) (Line 3). Then, for each activation pattern p in Q (Lines 5-6), it reconstructs the corresponding activation region η (subroutine constructActivationRegion, Line 8) as the H-representation of p (cf. Equation 2). Next, for each neuron in f •g x0 (Line 12), it checks whether the neuron activity p l,n cannot flip within the perturbation parameter space Θ, i.e., one of the half-spaces has no feasible points within Θ (subroutine isStable, Line 13). Otherwise, a new activation pattern p is constructed by flipping p l,n (subroutine flipped, Line 14) and added to the queue (Line 20) if p is feasible (subroutine calcInteriorPointOnFace, Lines 17-18). Finally, the activation

I.9 Details of experimental results

Table 2 shows breakdown of verification statuses in experimental results for each algorithm and each DNN size (cf. Section 5). In particular, for traversing AR boundaries, we can see the problem that the ratio of "Timeout" and "Failed (outof-memory)" increases as the size of the DNN increases. This problem is because gbs-AR traverses more activation regions by the width of the hyperparameter w δ than gbs-CR. It would be desirable in the future, for example, to traverse only the small number of activation regions near the AR boundary.

Table 2. Breakdown of verification statuses. "Robust" and "NotRobust" mean algorithm found "only robust regions" and "at least one not-robust region", respectively. "Timeout" and "Failed" mean algorithm did not finish "within 2 hours" and "due to out-of-memory", respectively.

Fig. 1 .

 1 Fig. 1. Misclassifications caused by combinations of semantic perturbations.

Fig. 2 .

 2 Fig.2. Perturbation-induced changes in images (first row), saliency-maps (second row) and the metric quantified the degree of collapse of each saliency-map (third row); where δ denotes the threshold to judge a saliency-map is valid or not.

Fig. 3 .

 3 Fig. 3. The outermost boundaries of classification robustness (left) and attention robustness (right); the origin at the bottom-left corresponds to the input image without perturbation, and each plotted point denotes the perturbed input image (middle). The shapes of the boundaries indicate the existence of regions that the DNN successfully classifies without sufficient evidence.

Fig. 4 .

 4 Fig. 4. Differences in changes in saliency-maps for two DNNs. Each saliency-map of DNN-1 above is more collapsed than DNN-2's: where columns (O), (B), (P), and (T) denote original (i.e., without perturbations), brightness change, patch, and translation, respectively.

Fig. 5 .

 5 Fig. 5. Illustration of outermost CR boundary on a 2-dimensional perturbation parameter space. The origin 0 is the original image without perturbation (θ1 = θ2 = 0).

3 :

 3 (lo, up) ← calcRange(x0; η) // the range ([lower and upper) of ai within η. 4: nearBoundary

Fig. 7 .

 7 Fig. 7. Experimental results.

Fig. 9 .

 9 Fig. 9. MNIST images used for experiments.

Fig. 10 .

 10 Fig. 10. Fashion-MNIST images used for experiments.

  a

  zero padding x0 tgt(r) -x0 src(r) (c = 1 ∧ r ≥ |θ (l+1) |) // add θ s(r) + |θ (l) | ∧ r > |θ (l+1) |) // copy x0 i 0 (otherwise) s(r) def = let i := r -|θ (l+1) |. ( i/w + tx -1)w + (i mod w) t(r) def = let i := r -|θ (l+1) |. ( i/w + tx -2)w + (i mod w) I.6 Images used for our experiments

  ∂f j (x) ∂x i = C (x ∈ {g x0 (θ) | θ ∈ ar f •g (p)})A small example of Lemma 1 (cf. Figure11)Let X = [0, 1] 3 , Y = R 2 , Θ = [0, 1] 1 , x0 ∈ X = (1, 0.5, 0.1), g x0 (θ ∈ Θ) ∈ X = ReLU (-θ 1 + x0), and f (x ∈ X) ∈ Y = ReLU (x 1 + x 2 , x 1 + x 3 ). Because g x0 (0.6) = ReLU (0.4, -0.1, -0.5) and f (g x0 (0.6)) = ReLU (0.4, 0.4), p = ap f •g (0.6) = [1, 0, 0|1, 1] ∈ AP f •g . Then, p ≥2 = [1, 1] = ap f (g x0 (0.6)) ∈ AP f . Here, ar f •g (p) corresponding to HConvex f •g (θ; p) ≡ -θ+1 ≥ 0∧-θ+0.5 ≤ 0 ∧ -θ + 0.1 ≤ 0 ∧ -θ + 1 ≥ 0 ∧ -θ + 1 ≥ 0 ≡ 0.5 ≤ θ ≤ 1, on the other hand, ar f (p ≥2 ) corresponding to HConvex f (x; p ≥2 ) ≡ x 1 + x 2 ≥ 0 ∧ x 1 + x 3 ≥ 0. Because 0 ≤ x 1 + x 2 = x 1 + x 3 = 1 -θ ≤ 0.5 (θ ∈ ar f •g (p)), ∀θ ∈ ar f •g (p). g x0 (θ) ∈ ar f (p ≥2 ).

Fig. 11 .

 11 Fig. 11. An image for a small example of Lemma 1.

Fig. 12 .

 12 Fig. 12. Examples of BFS results. (Near the edges, polygons may fail to render, resulting in blank regions.)

  f •g x0 (p) (cf. Appendix I.1). Algorithm 1 gbs(f, g, x0, Θ; δ, w) → (H CR , H M R , H CB , H AR , H IR , H AB ) Output: H CR , H M R , H CB , H AR , H IR , H AB ⊂ P(Θ) 1: H CR , H M R , H CB , H AR , H IR , H AB ← {}, {}, {}, {}, {}, {} 2: g x0 ← g(•, x0) // currying g with x0; i.e, g x0 (θ) = g(θ, x0). 3:

	Input: f, g, x0, Θ, δ

  queue for boundary search. 4: OBS ⊂ AP f •g x0 ← {} // observed activation patterns. 5: while #|Q| > 0 // loop for geometrical-boundary search. do 6:

  local queue for an iteration. 10:// Push each activation region connected to η.

11: for l = 1 to #layers of f • g x0 ; n = 1 to #neurons of the l-th layer do 12: continue if isStable(p, l, n, Θ) // skip if activation of x l,n cannot flip in Θ. 13: p ← f lipped(p, l, n) // flip activation status for neuron x l,n . 14: continue if p ∈ OBS else OBS ← OBS ∪ {p } // skip if p was observed. 15: θ F ← calcInteriorP ointOnF ace(η, l, n) 16: continue if θ F = null // skip if p is infeasible. 17:

Table 1

 1

	shows the ReLU-FNNs for classification used in our exper-
	iments; each FNN uses different training data and architectures. We inserted
	semantic perturbation layers (cf. Section 4.1) in front of each ReLU-FNN for
	classification during each experiment; the layers had total 1,568 neurons.
	All experiments were performed on virtual computational resource "rt C.small"
	(with CPU 4 Threads and Memory 30 GiB) of physical compute node "V" (with
	2 CPU; Intel Xeon Gold 6148 Processor 2.4 GHz 20 Cores (40 Threads), and
	12 Memory; 32 GiB DDR4 2666 MHz RDIMM (ECC)) in AI Bridging Cloud

https://docs.scipy.org/doc/scipy/reference/generated/scipy.optimize. linprog.html

https://docs.scipy.org/doc/scipy/reference/generated/scipy.optimize. minimize.html

https://docs.abci.ai/en/system-overview/

However, due to our internal procedures, we cannot publish it until at least May 21.

https://openreview.net/forum?id=zWy1uxjDdZJ