Satoshi Munakata

Caterina Urban

Haruki Yokoyama

Koji Yamamoto

Kazuki Munakata

Verifying Attention Robustness of Deep Neural Networks against Semantic Perturbations

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 saliencymap. 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. We empirically evaluate the effectiveness and performance of our method on DNNs trained on popular image classification datasets.

Introduction

Classification Robustness. Deep neural networks (DNN) are now dominant solutions in computer vision, notably for 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 [START_REF] Ashmore | Assuring the machine learning lifecycle: Desiderata, methods, and challenges[END_REF]. From an assurance point of view, one key property that has been extensively studied is the robustness of the classification against input perturbations [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability[END_REF]. In particular, a long line of work has focused on robustness to adversarial input perturbations [35]. However, DNNs have been shown to also be vulnerable to input perturbations likely to naturally occur in practice, such as small brightness changes, translations, rotations, and other spacial transformations [START_REF] Fawzi | Manitest: Are Classifiers Really Invariant?[END_REF]19,[START_REF] Xiao | Spatially Transformed Adversarial Examples[END_REF][START_REF] Engstrom | Exploring the landscape of spatial robustness[END_REF]11]. In this paper we focus on such semantic perturbations. A number of approaches have been proposed to determine the range of perturbation parameters (e.g., the amount of brightness change and translation) that do not change the classification [3,[START_REF] Mohapatra | Towards verifying robustness of neural networks against a family of semantic perturbations[END_REF]. However, we argue that classification robustness is not a sufficient quality assurance criterion in safety-critical scenarios. 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 [28,[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 [26]"), 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 saliencymaps [24,[START_REF] Guo | Visual attention 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 3 , 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 saliencymap 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 attention 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 specialize in the gradient-based saliency-maps for the image classification DNNs [28] and 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 only 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 Fig. 1: Misclassifications caused by combinations of semantic perturbations.

Fig. 2: Perturbation-induced changes in images (first row), saliency-maps (second row) and the metric quantified the degree of collapse of each saliencymap (third row); where δ denotes the threshold to judge a saliency-map is valid or not. 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. ReLU-FNNs include fully-connected neural networks and convolutional neural networks (CNNs). 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 classifi-cation 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 [28] 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 [28,[START_REF] Tsipras | Robustness may be at odds with accuracy[END_REF], 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 [28]. 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 attention 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 (

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 H.8, we describe a baseline Breadth-First Search (BFS ) method for solving P rob CR , and P rob AR (enumerating all perturbation parameter regions).

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 H.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 would have 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 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 the region is close to the boundary or not. The hyperparameter w δ should be greater than 0 to verify attention/inconsistency robustness because attention inconsistency changes discretely for ReLU-FNNs (cf. 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 q ← popM axLineDistance(Q); p ← p(q); OBS ← OBS ∪ {p} 7:

∂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.
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 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. the small example in Appendix H.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 f •g x0 (p) (cf. Appendix H.1). 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 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 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 1 -norm (L 1 ) and the L 2 -norm (L 2 ): where, w is the width of image x ∈ X.

← (lo ≤ δ ≤ up) ∨ (δ -w δ ≤ lo ≤ δ + w δ ) ∨ (δ -w δ ≤ up ≤ δ + w δ ) 5: if lo ≤ up ≤ δ /*

Verifying CR/MR and AR/IR

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, 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., 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 H.1). 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 (CDFs), as the sum of CDFs is also a CDF, the left-hand side of the above equation can be determined by comparing the values Table 1: ReLU-FNNs used in our experiments. Networks with name prefix "M-" ("F-") is trained on MNIST (Fashion-MNIST). In column Layers, "FC' denotes fully connected layers while "Conv" denotes convolutional layers. 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 using a convex optimizer. Note that if the saliency-map is expected to keep against perturbations, the above optimization is unnecessary because ai(θ ∈ eta, x0) is constant. Thus, it is straightforward to conclude that our GBS method is sound and complete for verifying CR/MR and AR/IR over the explored activation regions: Theorem 1. Our GBS method shown in Algorithm 1 and 2 is sound and conditionally complete for solving P rob CR ob , and P rob AR ob .

-If the outermost CR/AR boundary truly exists in Θ and the boundary bisects Θ into two parts, one with the origin ⃗ 0 and the other with its diagonal point (cf. Figure 5), then our GBS method always explores the boundary. -Otherwise, our GBS method does not always find CR/AR boundaries (including enclaves) that should be considered the outermost CR/AR boundary.

Experimental Evaluation

Our GBS method is implemented as an open-source Python tool. It is available at https://zenodo.org/record/6544905. We evaluated GBS on ReLU-FNNs trained on the MNIST [START_REF] Deng | The MNIST Database of Handwritten Digit Images for Machine Learning Research[END_REF] and Fashion-MNIST [START_REF] Xiao | Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms[END_REF] datasets. In our evaluation, we considered three variants of GBS: gbs-CR, which searches the CR boundary, gbs-AR, which searches the AR boundary, and gbs-CRAR, which searches the boundary of the regions satisfying both CR and AR. For gbs-AR and gbs-CRAR we used the definitions f ilter(x) def = x, dist(x, x ′ ) def = ||x-x ′ || 2 , δ def = 3.0, and w δ = 0.2 (for gbs-CR we used δ = 0 and w δ = 0, cf. Section 4.2). Figure 7a and 7c show the breakdown of the verification result for gbs-AR and gbs-CR over 10 images (not used for training) from each dataset considering three combinations of semantic perturbations (brightness+patch (BP), transla-tion+patch (TP), translation+brightness (TB)). The blue, red, gray, and black bars denote robust (i.e., all explored activation regions were verified to be robust), not-robust (i.e., all activation regions on the outermost CR/AR boundary were explored and at least one of them was found to violate robustness), timed out, and out-of-memory, respectively. We used a time out of two hours for each robustness verification. The figures show that gbs-AR timed out at a higher rate for smaller size DNNs than gbs-CR. This is due to the fact that gbs-AR verified robustness for more images and generally explored more activation regions than gbs-CR as also shown in Figure 7d, which compares the number of verified (explored) activation regions for each combination of perturbations. Looking further into this difference, it turns out that the choice of the hyperparameter w θ = 0.2 also caused gbs-AR to explore the AR boundary more extensively than necessary. It remains for future work to study how to choose a good value for w θ to narrow this search. Overall, however, Figure 7d shows that GBS (which searches the outermost CR/AR boundary) reduces as intended the number of explored activation regions with respect to the baseline BFS (which enumerates all perturbation parameter regions). This, in turn, directly affects the performance of the algorithms as demonstrated in Figure 7b, which shows the trend of increasing computation time with increasing the number of neurons for each algorithm as a box plot on a log scale. The figure also shows that the median computation time increases exponentially with the number of neurons for all algorithms. This result is expected [START_REF] Jordan | Provable certificates for adversarial examples: Fitting a ball in the union of polytopes[END_REF][START_REF] Fromherz | Fast geometric projections for local robustness certification[END_REF]42] and suggests that incorporating abstractions and approximate verification methods [START_REF] Singh | An abstract domain for certifying neural networks[END_REF]43,[START_REF] Müller | PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations[END_REF] is needed in order to scale to very large DNNs such as VGG16 [START_REF] Simonyan | Very deep convolutional networks for large-scale image recognition[END_REF].

Related Work

Robustness Verification. To the best of our knowledge, we are the first to formulate and propose an approach for the attention robustness verification problem (see, e.g., recent surveys in the area [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability[END_REF][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 classification robustness against image rotation, and [3] verified classification robustness against other semantic perturbations such as translation, scaling, shearing, brightness change, and contrast change. However, in this paper, we have argued that attention robustness more accurately captures trends in weakness for the combinations of semantic perturbations than existing classification robustness in some cases (cf. Section 2). In addition, approximate verification methods such as DeepPoly [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] fail to verify near the boundary [START_REF] Sotoudeh | Provable repair of deep neural networks[END_REF] while our GBS method 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.

[9] responded to the paper reviewer that traversing time would increase exponentially with the size of a DNN [START_REF] Fromherz | Fast geometric projections for local robustness certification -openreview[END_REF]. 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 are several methods of targeting only low-dimensional subspaces in the high-dimensional input space for verification [START_REF] Sotoudeh | Computing linear restrictions of neural networks[END_REF]33,[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., partially applied 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 Θ. Another possibility to improve scalability is the method of partitioning the input space and verifying each partition in a perfectly parallel fashion [START_REF] Urban | Perfectly parallel fairness certification of neural networks[END_REF]. Our implementation has not been fully parallelized yet but it should be relatively straightforward to do as part of our future work. Saliency-Map. Since [28] first proposed the method to obtain a saliency-map from the gradients of DNN outputs with respect to an input image, many improvements and extensions have been proposed [START_REF] Daniel | Smoothgrad: removing noise by adding noise[END_REF][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 [28]. However, it remains for future work to formulate attention robustness corresponding to improvements, such as gradient-smoothing [START_REF] Daniel | Smoothgrad: removing noise by adding noise[END_REF] and line-integrals [START_REF] Sundararajan | Axiomatic attribution for deep networks[END_REF].

It is known that semantic perturbations can significantly change the saliencymaps [24,[START_REF] Guo | Visual attention 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 attention 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 saliencymap consistency by [START_REF] Guo | Visual attention consistency under image transforms for multi-label image classification[END_REF]. While there have been works on the empirical studies of the attribution robustness [4,17], the verification of it has not been studied.

Conclusion and Future Work

We 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 provided a few cases 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.

42. Xu, S., Vaughan, J., Chen, J., Zhang, A., Sudjianto, A.: Traversing the local polytopes of relu neural networks: A unified approach for network verification. In: AdvML. AAAI (2022) 43. Yang, P., Li, J., Liu, J., Huang, C., Li, R., Chen, L., Huang

H Appendix

H.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)

H.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).

H.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 ),
≥L ′f def = [p l,n | L ′f ≤ l ≤ L f , 1 ≤ n ≤ N f l ] (1 ≤ L ′f ≤ L f ).

H.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 4 : 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)

H.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 (θ) // partially applying given constant x0 to g. 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 ) 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.

A (B) = a (B)

H.7 An example of Lemma 1

Lemma 1 is reprinted below.

H.9 Details of experimental results

Table 2 shows the 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. 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 saliencymap 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.

Fig. 6 :

 6 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 .

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.

Fig. 12 :

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

  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 ).

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, Θ, δ)

  The gradient 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) // partially applying x0 to g; i.e, g x0 (θ) = g(θ, x0). 3:

	Input: f, g, x0, Θ, δ
	∂g x0 i ∂θ = ∂xi ∂θ is

  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

  they are included parent activation region ar f ≤L ′f (p) corresponding to convex polytopeHConvex f ≤L ′f (x; p) def = l≤L ′f ,n A ′′ l,n x ≤ b ′′ l,n[START_REF] Lim | Hierarchical verification for adversarial robustness[END_REF]. 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

In this paper, the term "attention" refers to the focus of certain specific pixels in the image, and not to the "attention mechanism" used in transformer models[START_REF] Vaswani | Attention is all you need[END_REF].

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

A small example of Lemma 1 (cf. Figure 11)

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

H.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


Luca Negrini
email: luca.negrini@corvallis.it

Static Analysis of Data Transformations in Jupyter Notebooks

Keywords: CCS Concepts:, Theory of computation → Program analysis, Abstraction, • Software and its engineering → Automated static analysis Static Analysis, Abstract Interpretation, Data Science, Jupyter Notebooks

Jupyter notebooks used to pre-process and polish raw data for data science and machine learning processes are challenging to analyze. Their data-centric code manipulates dataframes through call to library functions with complex semantics, and the properties to track over it vary widely depending on the verification task. This paper presents a novel abstract domain that simplifies writing analyses for such programs, by extracting a unique CFG from the notebook that contains all transformations applied to the data. Several properties can then be determined by analyzing such CFG, that is simpler than the original Python code. We present a first use case that exploits our analysis to infer the required shape of the dataframes manipulated by the notebook.

Introduction

The ever-increasing usage of data-driven decision processes led to data science (DS) and machine learning (ML) permeating several areas of everyday life, reaching outside the boundaries of computer science and software engineering. Ensuring correctness of these processes is particularly important when they are employed in critical areas like medicine, public policy, or finance. In contrast to robustness verification of trained ML models [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF], data pre-processing of the DS/ML has received little attention. As raw data is often inconsistent or incomplete, pre-processing programs, typically implemented in Jupyter notebooks, apply transformations to polish it to the point where it can be visualized or used for training. Errors and inconsistencies at this stage can silently propagate downwards in the DS/ML chain, leading to incorrect conclusions and below-par models [START_REF] Chen | Why is My Classifier Discriminatory?[END_REF].

Verification of notebooks can take different directions, such as detecting data leakages (i.e., sharing of information between the training and test datasets [START_REF] Subotić | A Static Analysis Framework for Data Science Notebooks[END_REF]) or warning about the introduction of bias or skews [START_REF] Yang | Fairness-Aware Instrumentation of Preprocessing Pipelines for Machine Learning[END_REF]. Regardless, Jupyter notebooks are challenging to analyze: code comes in blocks that can be executed in any order with repetitions, and data is manipulated through calls to a vast number of library functions with complex and possibly overlapping semantics.

This paper proposes an abstract interpretation approach to simplify the implementation of verification techniques for Jupyter notebooks containing DS/ML programs. We propose an abstract domain that tracks transformations made to dataframes, that is, the in-memory tables containing the input data, in a unique graph. The latter contains data transformations as nodes that are linked by edges encoding the order in which they are applied. The final graph produced at the end of the analysis is a control flow graph (CFG) containing only dataframe transformations: analyses such as the ones mentioned above can be implemented as fixpoints over this CFG, instead of tackling the more complex Python code.

This paper is structured as follows. Section 2 discusses related work. Section 3 introduces PyLiSA, the analyzer used to evaluate our domain, and LiSA, the framework it relies on. Section 4 defines the abstraction for dataframe values. We then explore a first use-case in Section 5, where we use our abstraction for inferring the shape of the dataframes used by a program. We then conclude with a preliminary experiment on a real DS notebook in Section 6.

Related Work

Obtaining formal guarantees on the safety and fairness of ML models has been a subject of recent widespread interest [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF].

Our work builds upon this large ecosystem and proposes a verification framework for the data pre-processing stage of the ML pipeline. The closest body of work is [START_REF] Subotić | A Static Analysis Framework for Data Science Notebooks[END_REF] which also analyses DS notebooks along with their peculiar execution semantics and proposes an abstraction to detect data leakage. Our approach towards the shape inference of input data follows the work of [START_REF] Urban | What Programs Want: Automatic Inference of Input Data Specifications[END_REF] and extends it to support inputs to programs which contain datasets. Similarly, our objective of inferring input data usage directly derives from the compound data structure usage analysis presented in [START_REF] Urban | An Abstract Interpretation Framework for Input Data Usage[END_REF] and adds the ability to track the usage of selections of datasets. The objective of detecting bias/skew introduction is inspired from the mlinspect tool proposed in [START_REF] Grafberger | MLINSPECT: A Data Distribution Debugger for Machine Learning Pipelines[END_REF]. This tool builds a directed acyclic graph (DAG) of operations (like filters or projections) applied to the data by analyzing the code and using framework-specific backends (like scikit-learn). After analyzing the DAG, it suggests potential sources of bias/skew. Although this is promising, it only places syntactic checks and cannot concretely detect which operations cause these problems. Lastly, [START_REF] Mohammad Hossein Namaki | Vamsa: Automated Provenance Tracking in Data Science Scripts[END_REF] is an automated data provenance system for Python. However, it requires executing the code which is not always be feasible when large datasets are involved.

LiSA and PyLiSA

LiSA [START_REF] Ferrara | Static Analysis for Dummies: Experiencing LiSA[END_REF][START_REF] Negrini | A generic framework for multilanguage analysis[END_REF] (Library for Static Analysis) is a modular framework for developing static analyzers based on the abstract interpretation theory. LiSA analyzes CFGs whose statements do not have predefined semantics: instead, users of the framework define custom statement instances implementing language-specific semantic functions, enabling the analysis of a wide range of programming languages and the development of multilanguage analyses. The analysis infrastructure is partitioned into three main areas: call evaluation, memory modeling and value analysis. Each area corresponds to a separate analysis component, that operates agnostically w.r.t. how the others are implemented. At first, calls are abstracted by the Interprocedural Analysis, that leaves the remaining components with call-less programs. Then, memory-related expressions are abstracted by the Heap Domain, yielding calland memory-less programs for the Value Domain to analyze. Code parsing and semantics are defined in Frontends, that can also provide implementations for LiSA's components. In this paper, we employ the Python frontend PyLiSA1 .

The Dataframe Graph Domain

We present an abstraction able to capture the structure of the dataframes manipulated in Python code. Intuitively, we employ a graph structure to keep track of all operations that involve dataframes, with edges encoding the order in which they are performed. The graph thus represents the state of each dataframe at a given program point. Nodes of this graph can be referenced by variables of the program. The latter thus refers to the dataframe corresponding to the sub-graph obtained with a backward DFS starting from the node. We adopt a two-level mapping: program variables point to labels, and the latter are mapped to the nodes. This enables simple handling of dataframe aliasing (i.e., two variables will be mapped to the same label) and updates (i.e., by changing the nodes pointed by a label, we indirectly update all variables pointing to the label).

Our domain D # is meant to be an abstraction of the portion D of the program state that stores information about dataframes: we rely on an auxiliary domain to reason about the remainder of the state. As, in our experience, non-dataframe values appearing in the notebooks we target are mostly constants, D # cooperates with a simple constant propagation domain CP # . We rely on the semantics of CP # to abstract:

• a string expression s as a constant string 𝜎;

• a list of strings cl as a constant list of constant strings ⟨𝜎 1 , . . . , 𝜎 𝑛 ⟩; • a list of dataframes dl as a constant list of abstract labels ⟨ℓ 1 , . . . , ℓ 𝑛 ⟩ that will be introduced shortly; • the left-hand side of an assignment x to a set of identifiers {x 1 , . . . , x 𝑛 }.

We begin defining D # by introducing the graph structure, where a graph 𝑔 # = (𝑁 , 𝐸) ∈ G # is composed by a set of nodes 𝑁 ⊆ 𝒩 and a set of edges 𝐸 ⊆ ℰ. Elements of 𝒩 are:

• read(𝜎), initializing a dataframe with the contents of file 𝜎; • access(𝜎 1 , . . . , 𝜎 𝑘 ), accessing columns 𝜎 1 , . . . , 𝜎 𝑘 , 𝑘 ∈ N; • transform(𝑓 ), transforming values through an auxiliary function 𝑓 ; • concat, concatenating multiple dataframes;

• filter(𝜎, 𝑜𝑝, 𝑣), selecting rows where 𝑣 𝜎 𝑜𝑝 𝑣 holds (with 𝑣 𝜎 being the value of column 𝜎); • assign(𝜎 1 , . . . , 𝜎 𝑘 ), assigning columns 𝜎 1 , . . . , 𝜎 𝑘 , 𝑘 ∈ N to a new value. where 𝜎 and 𝑣 are string and value abstractions in CP # , 𝑜𝑝 ∈ {=, ≠, >, ≥, <, ≤} and 𝑓 is the signature of a Python function. Instead, elements of ℰ are (with 𝑛, 𝑛 ′ ∈ 𝒩, 𝑖 ∈ N):

• 𝑛 → 𝑛 ′ is an edge encoding the sequential order of operations; • 𝑛 ⇝ 𝑖 𝑛 ′ is a concatenation edge, where 𝑛 is the 𝑖-th dataframe in the concatenation that builds 𝑛 ′ (note that 𝑛 ′ can have more incoming concatenation edges using the same 𝑖, indicating multiple candidates for the same index); • 𝑛 ↠ 𝑛 ′ is an assign edge, where 𝑛 is the right-hand side of the assignment 𝑛 ′ (once more, 𝑛 ′ can have more incoming assign edges, indicating multiple candidates for the right-hand side).

D # also contains two maps, both relying on abstract labels. A label ℓ ∈ ℒ is an arbitrary synthetic identifier that serves as an abstract name for a set of nodes in 𝒩, where ℒ is the finite set of all possible labels. While we do not impose any specific structure on ℒ, a common characterization of labels is to have one for each program point. D # contains (i) a function ℒ → ℘(𝒩) ∈ L # from labels to sets of nodes, and (ii) a map V𝑎𝑟 → ℘(ℒ) ∈ V # keeping track of which possible labels a variable can refer to. Notice that, depending on the analyzer's infrastructure, variables can correspond to abstract memory locations or program variables.

We can now define D # as the Cartesian product V # × L # × G # , that is a complete lattice since G # is a Cartesian product of powersets, and V # and L # are functional lifts of powersets. One concern with infinite lattices such as D # is the convergence of fixpoint iterations over them. As G # intuitively does not satisfy ACC2 , a widening operator is required. As, in our experience, the DS notebooks that this domain targets mostly contain sequential code with very few loops that stabilize in few iterations, we employ a naive widening as

𝑑 # 1 ∇ 𝑑 # 2 = 𝑑 # 1 if 𝑑 # 1 = 𝑑 # 2 , ⊤ otherwise.
With such an operator we ensure termination of the analysis, and we leave the study of a more precise widening as future work.

Example. Figure 2 reports the 𝑑 # instance abstracting the code of Figure 1. For the sake of clarity, nodes of 𝑔 # are enriched with a numerical identifier on the top-left corner to easily identify them. Such identifiers are used in the codomain of 𝑙 # to represent them. We show how this graph is constructed while defining the abstract semantics.

The connection between D and D # is established by the abstraction function 𝛼 and the concretization function 𝛾. A set of functions { d1 , . . . , d𝑚 }, d𝑖 ∈ D, 1 ≤ 𝑖 ≤ 𝑚, 𝑚 ∈ N ∞ can be abstracted to an element 𝑑 # ∈ D # through function 𝛼 : ℘(D) → D # , defined as the lub of the abstractions of each individual d. The abstraction of a single function is defined as 𝛼 ( d) = (𝑣 # , 𝑙 # , 𝑔 # ), with:

• d = {(𝑣 1 , 𝑑 1 ), . . . , (𝑣 𝑘 , 𝑑 𝑘 )}, 1 ≤ 𝑖 ≤ 𝑘, 𝑘 ∈ N; • (𝑔 # 𝑖 , 𝑛 𝑖 ) = shape(𝑑 𝑖 ), 𝑔 # = 𝑖 𝑔 # 𝑖 ; • 𝑙 # = {(ℓ 1 , {𝑛 1 }), . . . , (ℓ 𝑘 , {𝑛 𝑘 })}; • 𝑣 # = {(𝑣 1 , {ℓ 1 }), . . . , (𝑣 𝑘 , {ℓ 𝑘 })}.
The abstraction of a single dataframe map exploits shape : D → G # × 𝒩, an auxiliary function that extracts the shape of a concrete dataframe as a single-path graph containing only a read node followed by an access node reporting all the existing columns, and returning the graph itself and its

𝑣 # = {(df1, {ℓ 1 }), (df2, {ℓ 4 }), (df3, {ℓ 5 })} 𝑙 # = {(ℓ 1 , {4}), (ℓ 2 , {3}), (ℓ 3 , {5}), (ℓ 4 , {6}), (ℓ 5 , {7})} Figure 2.
Example 𝑑 # abstracting the code of Figure 1 unique leaf. The abstraction of a set of states is thus the union of the abstraction of each individual state, generated by creating the graph 𝑔 # containing the shape (that is, the access to all columns 𝐶 optionally preceded by the reading of source 𝑆) of all existing dataframes, having each variable refer to the corresponding node in 𝑔 # .

As 𝛼 is join-preserving, the concretization function 𝛾 can be defined in terms of 𝛼, according to Proposition 7 of [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF], also inducing the Galois connection ⟨℘(D), ⊆⟩ ---→ ← ---𝛼 𝛾 ⟨D # , ⊑⟩, where ⊑ is the lift of ⊆ to functions and Cartesian products.

Abstract Semantics. The abstract semantics of D # is defined w.r.t the one of CP # , that is used to evaluate nondataframe expressions. D # evaluates dataframe expressions to a set of labels, identifying nodes representing the dataframes that correspond to the expression. In the following, we give intuitive definitions of the semantics of expressions that involve dataframes.

Assignment. Whenever the right-hand side of an assignment x = df is a dataframe expression, 𝑣 # must be updated for the corresponding variable. Specifically, as df evaluates to a set of labels {ℓ 1 , . . . , ℓ 𝑤 }, and x evaluates to a set of identifiers {x 1 , . . . , x 𝑛 }, 𝑣 # can be updated to

𝑣 ′ = 𝑣 ′ [x 𝑖 ↦ → {ℓ 1 , . . . , ℓ 𝑤 }], ∀x 𝑖 ∈ {x 1 , . . . , x 𝑛 }.
Example. When evaluating the assignment at line 2 of Figure 1, the semantics stores the label pointing to the read node (whose creation is dictated by the abstract semantics of read). 𝑣 # is thus extended with the pair (df1, {ℓ 1 }), where {ℓ 1 } is the label returned by the semantics of read.

Variable evaluation. Whenever a variable is referenced throughout the program, our semantics must evaluate it to the corresponding labels if it refers to a dataframe, while the remaining variables are handled by CP # . Thus, when x resolves to a dataframe, it evaluates to 𝑣 # (x).

Example. When evaluating line 6 of Figure 1, df1 and df2 must be first resolved to the dataframes they represent: df1 evaluates to {ℓ 1 } while df2 is evaluated to {ℓ 4 }, as the two variables are mapped to {ℓ 1 } and {ℓ 4 } in 𝑣 # , respectively. Dataframe initialization. When dataframes are initialized with the contents of an external resource through read, the operation cannot be precisely modeled statically as the contents of the resource are unknown at compile time. We thus symbolically record the source of the data by adding a read node to the graph. If the argument of read is abstracted by CP # as 𝜎, the semantics adds a new read(𝜎) and returns a unique label { l } that points to the freshly added node.

Example. When the read call at line 2 of Figure 1 is evaluated, 𝑔 # is still empty. A single read('italy.csv') node is added to 𝑔 # by the semantics, that then extends 𝑙 # with a fresh label ℓ 1 , that is mapped to a set containing the node itself, and is used as the only label in the result of the evaluation.

Column access. The access transformation accesses a set of columns of the target dataframe. As this operation does not create a new dataframe, it is modeled as an in-place operation, directly affecting the nodes pointed by the labels of its argument: the semantics adds an access(𝜎 1 , . . . , 𝜎 𝑛 ) node (where 𝜎 1 , . . . , 𝜎 𝑛 is the CP # abstraction for the column list), connecting it to the nodes of the first argument using normal edges → and mapping it to a new label.

Example. When the access to column birth at line 3 of Figure 1 is evaluated, df1 is first processed, producing {ℓ 1 } as abstract value. Then, the evaluation of the column names yields ⟨ ′ birth ′ ⟩, resulting in the creation of node access('birth'). The graph is then extended adding (i) the newly created node with id 2, and (ii) a normal edge connecting nodes 1 and 2. Furthermore, ℓ 1 is remapped to {2} inside the resulting 𝑙 # (the mapping is not visible in Figure 2 as evaluation of following statements overwrites it).

Value transformation. Tracking transformations of dataframe values can be problematic, as the functions carrying the transformation must be summarized somehow. Instead, we provide a lightweight semantics that records the signature of the used function inside a node of the graph, deferring further reasoning to successive abstractions. As this is not an in-place operation, the semantics creates a new label that is mapped to the transformation node, and the latter is connected to nodes representing the target dataframe (thus branching off the original dataframe). The label is then returned as the unique result of the evaluation. The new transform(𝑓 ) node is also connected to the nodes of the receiving dataframe using normal edges →.

Example. When the to_datetime call at line 3 of Figure 1 is evaluated, our semantics first evaluates the column access, producing {ℓ 1 } as shown earlier. The semantics then (i) creates a unique transform(to_datetime) node, (ii) adds it to the graph with id 3, and (iii) connects it to node 2 with a normal edge. The mapping between ℓ 2 , a fresh and unused label, and the singleton set containing node 3 is also introduced in 𝑙 # , and {ℓ 2 } is returned as the evaluation's result.

Dataframe assignment. When a portion of a dataframe is overwritten with new values, the semantics of variable assignment cannot be employed, as no variable changes value.

Instead, the semantics of assign records the assignment as an assign(𝜎 1 , . . . , 𝜎 𝑛 ) node in the graph (with 𝜎 1 , . . . , 𝜎 𝑛 is the abstraction of the column list produced by CP # ), connected to both the dataframe receiving it (using normal edges →) and the value being stored (using assign edges ↠).

Example. When the assignment at line 3 of Figure 1 is evaluated, df1 is evaluated to {ℓ 1 }, the column names evaluate to the constant list ⟨ ′ birth ′ ⟩, and the transform expression is resolved to {ℓ 2 }. The semantics proceeds by (i) creating an assign('birth') node, (ii) adding it to the graph with id 4, (iii) connecting it to node 3 (image of ℓ 2 in 𝑙 # ) with an assign edge, and finally (iv) connecting it to node 2 (image of ℓ 1 in 𝑙 # ) with a normal edge. To conclude, ℓ 1 is remapped to a set containing node 4 in 𝑙 # , as the assignment has side-effects.

Rows filtering. Similarly to value transformations, abstracting rows filters can be problematic, as different facts about the filtering conditions can be of interest depending on the target analysis. We thus record the condition as-is within a filter(𝜎, 𝑜𝑝, 𝑣) node, delegating its interpretation to successive abstractions. Note that this is not an in-place operation: original dataframes are not modified, but a filtered view of them is returned by the operation. We reflect this in our formalization by yielding a fresh label pointing to the filtering node. The semantics connects the filter node to the ones of the receiving dataframe with normal edges →.

Example. When rows are filtered at line 5 of Figure 1 is evaluated, the semantics first evaluates its arguments: df2 is evaluated to {ℓ 3 }, the column name evaluates to 'age', and the value used for the comparison to the constant 50. A filter('age', <, 50) node is then created, and it is added the graph with id 6. A normal edge connecting it to node 5 (image of ℓ 3 in 𝑙 # ) is also introduced, and the label ℓ 4 is created and mapped to a set containing node 6 in 𝑙 # .

Concatenation. The semantics of the concatenation must create a new dataframe with the contents of all of its arguments, that come compacted into a list. For of our domain, this means connecting all nodes of each argument to a concat node, that will be the image of a new label, using concatenation edges ⇝ with the corresponding indexes.

Example. When the concat call at line 6 of Figure 1 is evaluated, the semantics first evaluates the list of target dataframes, producing ⟨{ℓ 1 }, {ℓ 4 }⟩ as abstraction for the elements of the list. The semantics then (i) creates the concat node, (ii) adds it to the graph with id 7, and (iii) connects it to nodes 4 and 6 (images of ℓ 1 and ℓ 4 in 𝑙 # ) with concatenation edges indexed with 1 and 2. A fresh label ℓ 5 is generated, and is mapped to a singleton set containing node 7 in 𝑙 # .

As a first experiment, we selected the "Coronavirus (COVID-19) Visualization & Prediction" 3 dataframe, one of the most popular notebooks aggregating data from different sources on Kaggle, a public repository of Jupyter notebooks for DS. The graph produced when analyzing such code is published on a GitHub Gist 4 as it is too large for this manuscript. Note that the implemented analysis supports additional pandas constructs w.r.t. the ones presented in this paper, that have been omitted as they do not contribute further to the intuition behind the domain. In the graph, these take the form of additional node kinds, whose intuitive meaning is explained in the Gist's introduction. The analysis generates the following warnings (where URL of csv files have been trimmed for compactness), correctly identifying all column names that appear in the notebook: [File:

Conclusion

This paper presents an abstract interpretation approach to analyze Python programs employed in data science and machine learning. Such programs manipulate dataframes, that is, complex in-memory tables collecting data that can be used to guide decision processes or train machine learning models. We designed an abstract domain that extracts the operations performed over dataframes, building a graph that encodes the order in which they are performed. Such a graph can be the subject of further analyses, inferring several properties such as the shape of the dataframes read by the program, or the absence of data leakages between training and testing phases of a machine learning process. As a guiding example of how to exploit our domain, we defined a simple abstract interpretation that computes, for each file read by the source program (and thus present inside the graph), the set of columns that are either accessed before being assigned, or defined through an assignment. We provided an early implementation of both domains in PyLiSA, a LiSA frontend for Python programs.

There are plenty of future directions that our work can take. As this work is still ongoing, the obvious first line of axis is to prove the soundness of the proposed semantics 3 https://www.kaggle.com/code/therealcyberlord/coronavirus-covid-19visualization-prediction, version 722. 4 https://gist.github.com/lucaneg/9621f3296b7b47b12c5ee1c52066b3d1. abstractions, followed by an investigation on their completeness to further improve the domain. Besides, inferring the shape of dataframes is not the only useful analysis one can employ for DS software. In fact, after strengthening shape inference to incorporate rows and cell properties, we aim at providing abstractions to detect data leakages and biases. Lastly, we aim at extending the abstraction to more pandas functions, and to further libraries other than pandas itself.

Figure 1 .

 1 Figure 1. Python DS running example

https://github.com/lisa-analyzer/pylisa.

As 𝒩 and ℰ are infinite sets, one can keep adding new nodes and edges without the graph ever stabilizing.

A First Application: Shape InferenceTracking dataframe transformations through D # is just the beginning. In general, successive analyses targeting D # instead of starting from the Python code can still be formalized

and implemented as abstract interpretations. Fixpoint algorithms can be applied over instances of G # , treating the nodes as code. In this context, one has to define the abstract semantics w.r.t. each node's meaning, possibly taking into account the edges attached to them. In this section, we explore one of the possible objectives in the analysis of DS programs, as we aim at inferring the shape of each dataframe read from an external source.

We start by defining the domain C # of columns. Denoting as Σ = Σ * ∪ {⊤, ⊥} the set possible string abstractions provided by CP # , elements of C # are functions ℘(Σ) → (℘(Σ) × ℘(Σ)) whose domain is composed by sets of strings {𝜎 1 , . . . , 𝜎 𝑝 } representing sources of data, and whose codomain is built over pairs of sets { 𝜎 1 , . . . , 𝜎 𝑛 }, { σ1 , . . . , σ𝑚 }. Each 𝜎 𝑖 is a column that is accessed before being assigned (and thus must be part of the original dataframe to prevent runtime errors), and each σ𝑖 is a column that is assigned during the execution (and thus might not exist in the original dataframe). The columns domain thus aims at inferring, for each external source of data, what columns must exist for the program to not crash. In our abstraction, we consider sets of sources as function keys since dataframes can be created through concatenation, and can thus have multiple sources. In this case, all accessed columns must exist in at least one source. Note that C # is a complete lattice, as it is a functional lift of a Cartesian product of powersets.

We informally define the semantics of C # w.r.t. nodes of G # , as this kind of analysis does not need variable information stored in L # and V # . The semantics relies on the auxiliary function sources : 𝒩 → ℘(Σ) that extracts all sources (i.e., arguments of read nodes) whose data is used to build the dataframe identified by the given node.

Read. When reading data from an external resource, no particular column is accessed. Instead, we define an entry in our state corresponding to the possible abstractions of the resource identifier.

Concat. Similarly to read, concat does not access any column, but instead introduces a new entry in the post-state corresponding to the union of its sources.

Transform. A transformation does not access any column explicitly, as it operates on the entirety of the dataframe that receives the transformation. As such, its semantics is defined as the identity function.

Access. The column access is the main vector for referencing columns by-name. This is reflected by its semantics, that adds every column name to the left-most set of the corresponding sources if we have no evidence of it being defined earlier.

Filter. As rows filtering is expressed as a condition over the value of a specific column, it indirectly represents a column access. This is once more reflected as the addition of the column name to the left-most set of the corresponding sources, if it was not defined before.

Assign. The dataframe assignment is the only node kind that can safely define non-existing columns. The semantics of this node adds the abstract column names to the rightmost set of the corresponding sources.

Example. We now use C # to infer the shape of the dataframes abstracted by the graph in Figure 2. For the sake of clarity, we first analyze the left-most branch of the graph as a whole, followed by the right-most one, concluding the analysis with the concat node. The analysis begins applying the semantics of read to node 1, using an empty C # instance 𝑐 # 0 = {} as pre-state, and producing the entry for the read resource 𝑐 # 1 = {({'italy.csv'}, (∅, ∅))}. This is in turn used as pre-state for the evaluation of node 2, where the semantics of access populates the function with the accessed column, producing 𝑐 # 2 = {({'italy.csv'}, ({'birth'}, ∅))}. As the semantics of transform is the identity function, the pre-state of node 4 is the join of the post-state of both predecessors:

When such result is used as argument for the assign semantics, it produces the post-state 𝑐 # 3 = {({'italy.csv'}, ({'birth'}, {'birth'}))}. Equivalently, the analysis starts with the same empty pre-state 𝑐 # 0 at node 5, applying the read semantics and producing the post-state 𝑐 # 4 = {({'france.csv'}, (∅, ∅))}. Then, 𝑐 # 4 is used to compute the result of the filter semantics at node 6, that is 𝑐 # 5 = {({'france.csv'}, ({'age'}, ∅))}. Lastly, at node 7, the pre-state is built as the lub of the predecessors' post-states 𝑐 # 6 = 𝑐 # 3 ∪ 𝑐 # 5 that thus contains both entries. The semantics of concat can then be applied to 𝑐 # 6 , producing the final state of the analysis:

({'italy.csv'}, ({'birth'}, {'birth'})), ({'france.csv'}, ({'age'}, ∅)), ({'italy.csv', 'france.csv'}, (∅, ∅))

6 An Early Experiment Using PyLiSA

Both D # and C # have been implemented in PyLiSA, that analyzes Jupyter notebooks by extracting the Python code from the cells that contains it. Cells are analyzed according to a specific user-defined execution sequence, defaulting to the order in which cells are defined in the notebook. We provide the semantics of pandas library's functions through LiSA's native CFGs. These are special CFGs that contain a single statement. Calls to native CFGs are evaluated by computing the semantics of their unique node, without running additional fixpoints: the node's semantics thus becomes an abstract summary of the modeled function. Specifically, the semantics of native CFGs modeling pandas functions converts them to the nodes presented in Section 4. D # has been implemented as a Value Domain, directly embedding the constant propagation domain. At the end of the analysis, a G # instance is extracted from the post-state of the last instruction, and a fixpoint is executed over the it using C # . Warnings are then issued to inform the user about columns accessed and assigned for each data source.