Year: 2021

Abstract:
Auditing trained deep learning (DL) models prior to deployment is vital for preventing unintended consequences. One of the biggest challenges in auditing is the lack of human-interpretable specifications for the DL models that are directly useful to the auditor. We address this challenge through a sequence of semantically-aligned unit tests, where each unit test verifies whether a predefined specification (e.g., accuracy over 95%) is satisfied with respect to controlled and semantically aligned variations in the input space (e.g., in face recognition, the angle relative to the camera). We enable such unit tests through variations in a semantically-interpretable latent space of a generative model. Further, we conduct certified training for the DL model through a shared latent space representation with the generative model. With evaluations on four different datasets, covering images of chest X-rays, human faces, ImageNet classes, and towers, we show how AuditAI allows us to obtain controlled variations for certified training. Thus, our framework, AuditAI, bridges the gap between semantically-aligned formal verification and scalability. https://sites.google.com/view/audit-ai

heading: 1 INTRODUCTION
text: Deep learning (DL) models are now ubiquitously deployed in a number of real-world applications, many of which are safety critical such as autonomous driving and healthcare (Kendall et al., 2019; Miotto et al., 2018; Senior et al., 2020). As these models are prone to failure, especially under domain shifts, it is important to know when and how they are likely to fail before their deployment, a process we refer to as auditing. Inspired by the failure-mode and effects analysis (FMEA) for control systems and software systems (Teng & Ho, 1996), we propose to audit DL models through a sequence of semantically-aligned unit tests, where each unit test verifies whether a pre-defined specification (e.g., accuracy over 95%) is satisfied with respect to controlled and semantically meaningful variations in the input space (e.g., the angle relative to the camera for a face image). Being semantically-aligned is critical for these unit tests to be useful for the auditor of the system to plan the model’s deployment.
The main challenge for auditing DL models through semantically-aligned unit tests is that the current large-scale DL models mostly lack an interpretable structure. This makes it difficult to quantify how the output varies given controlled semantically-aligned input variations. While there are works that aim to bring interpretable formal verification to DL models (Henriksen & Lomuscio, 2020; Liu et al., 2019), the scale is still far from the millions if not billions of parameters used in contemporary models (He et al., 2016; Iandola et al., 2014; Brown et al., 2020).
On the other hand, auditing has taken the form of verified adversarial robustness for DL models (Samangouei et al., 2018; Xiao et al., 2018a; Cohen et al., 2019). However, this has mostly focused on adversarial perturbations in the pixel space, for example, through Interval Bound Propagation (IBP), where the output is guaranteed to be invariant to input pixel perturbations with respect to Lp norm (Gowal et al., 2018; Zhang et al., 2019b). While these approaches are much more scalable to modern DL architectures, the pixel space variations are not semantically-aligned, meaning they do not directly relate to semantic changes in the image, unlike in formal verification. Consider a unit test that verifies against the angle relative to the camera for a face image. A small variation in the angle (e.g., facing directly at the camera versus 5◦ to the left) can induce a large variation in the pixel space. Current certified training methods are far from being able to provide guarantees with respect to such large variations in the pixel space with reasonable accuracy.
Our Approach. In order to overcome the above limitations, we develop a framework for auditing, AuditAI. We consider a typical machine learning production pipeline (Fig. 1) with three stages, the design and training of the model, its verification, and finally deployment. The verification is crucial in determining whether the model satisfies the necessary specifications before deployment.
We address the gap between scalability and interpretability by proposing to verify specifications for variations directly in a semantically-aligned latent space of a generative model. For example in Fig. 1, unit test 1 verifies whether a given face classification model maintains over 95% accuracy when the face angle is within d◦, while unit test 2 checks under what lighting condition the model has over 86% accuracy. Once the verification is done, the auditor can then use the verified specification to determine whether to use the trained DL model during deployment.
For semantically-aligned latent variations, we create a bridge between the generative model and the DL model such that they share the same latent space. We incorporate a variant of IBP (Zhang et al., 2019b) for verification with respect to perturbations in the latent space. Further this leads to a tighter and a much more practical bound in the output space compared to pixel-based certified training. We also show that AuditAI can verify whether a unit test is satisfied by generating a proof for verification based on bound propagation. Fig. 1 gives an overview of our auditing framework and Fig. 2 elaborates on the generative model bridge.

heading: Summary of Contributions:
text: 1. We develop a framework, AuditAI for auditing deep learning models by creating a bridge with a generative model such that they share the same semantically-aligned latent space. 2. We propose unit tests as a semantically-aligned way to quantify specifications that can be audited. 3. We show how IBP can be applied to latent space variations, to provide certifications of semanticallyaligned specifications.
We show that AuditAI is applicable to training, verification, and deployment across diverse datasets: ImageNet (Deng et al., 2009), Chest X-Rays (Irvin et al., 2019; Wang et al., 2017), LSUN (Yu et al., 2015), and Flicker Faces HQ (FFHQ) (Karras et al., 2019). For ImageNet, we show that AuditAI can train verifiably robust models which can tolerate 25% larger pixel-space variations compared to pixel-based certified-training counterparts for the same overall verified accuracy of 88%. The variations are measured as L2 distances in the pixel-space. The respective % increase in pixelspace variations that can be certified for Chest X-Rays, LSUN, and FFHQ are 22%, 19%, 24%. We conclude with a human-study of the quality of the generative model for different ranges of latent-space variations revealing that pixel-space variations up to 62% of the nominal values result in realistic generated images indistinguishable from real images by humans.
2 AUDITAI: A DEEP LEARNING AUDIT FRAMEWORK
In this section, we describe the details of our framework, AuditAI outlined in Fig. 1 for verifying and testing deep models before deployment. We propose to use unit tests to verify variations of interest that are semantically-aligned. The advantage of AuditAI is that the verified input ranges are given by several semantically aligned specifications for the end-user to follow during deployment. In the following sub-sections, we formally define unit tests, outline the verification approach, and describe the specifics of AuditAI with a GAN-bridge shown in Fig. 2.

heading: 2.1 UNIT TEST DEFINITION
text: Consider a machine learning model f : X → Y that predicts outputs y ∈ Y from inputs x ∈ X in dataset D. Each of our unit test can be formulated as providing guarantees such that:
F (x, y) ≤ 0 ∀x s.t. , ei(x) ∈ Si,in, y = f(x) (1)
Here, i subscripts an unit test, encoder ei extracts the variation of interest from the input x, and Si,in denotes the set of range of variation that this unit test verifies. If the condition is satisfied, then our unit test specifies that the output of the model f(x) would satisfy the constraint given by F (·, ·) ≤ 0. For example, x could be an image of a human face, and f could be a classifier for whether the person is wearing eyeglasses (f ≤ 0 means wearing eyeglasses and f > 0 means not wearing eyeglasses). Then ei(·) could be extracting the angle of the face from the image, and Si,in could be the set {ei(x)| ∀x |ei(x)| < 30◦} constraining the rotation to be smaller than 30◦. And F (x, y) = −f(x)f(x0◦) ≤ 0 says that our classifier output would not be changed from the corresponding output of x0◦ , the face image of x without any rotation. In this case, when the end-user is going to deploy f on a face image, they can first apply ei(·) to see if the face angle lies within Si,in to decide whether to use the model f .

heading: 2.2 VERIFICATION OUTLINE
text: Given a specification F (x, y) ≤ 0, we need to next answer the following questions: 1. How do we obtain the corresponding components (ei, Si,in) in Eq. (1)? 2. What can we do to guarantee that F (x, y) ≤ 0 is indeed satisfied in this case? For the sake of illustration, we first consider a scenario with a less realistic assumption. We will then discuss how we can relax this assumption. In this scenario, we assume that we are already given the encoder ei and a corresponding generator gi that inverts ei. Continuing the previous example, ei can extract the face angle of a given face image. On the other hand, gi(x0◦ , d◦) would be able to synthesize arbitrary face image xd◦ that is the same as x0◦ except being rotated by d◦.
Given the generator gi and the encoder ei, we propose to obtain Si,in building on interval bound propagation (IBP) (Gowal et al., 2018). We include a treatment of IBP preliminaries in Appendix A.1. Here, Si,in is the largest set of variations such that the specification F (x, y) ≤ 0 is satisfied. Given a set of variations Si,in, IBP-based methods can be used to obtain a bound on the output of the network Si,out = {y : ly ≤ y ≤ uy} and it can be checked whether the specification F (x, y) ≤ 0 is satisfied for all values in Si,out. We can start with a initial set S0i,in
and apply gi to this set. Then, we can first find out what would be the corresponding convex bound of variations of S0i,in in the image space X . We can subsequently propagate this bound in X through f to Y to get S0i,out and check whether F (x, y) ≤ 0 is satisfied. By iteratively searching for the largest set Sji,in such that F (x, y) ≤ 0 is still satisfied by S j i,out, we can obtain Si,in given F .

heading: 2.3 CERTIFIED TRAINING THROUGH LATENT REPRESENTATION
text: In the previous section, we are able to find the set Si,in such that Eq. (1) is satisfied given specification F , encoder ei, generator gi. However, there are several challenges that limit the practical application of this scenario. First and foremost, while significant progress has been made in generative models, especially controlled generation (Brock et al., 2018; Karras et al., 2017), the assumption of having gi apriori is still unrealistic. In addition, since the propagated bound is convex, one can imagine that the bound in X (high dimensional image-space) would be much larger than needed. This leads to a much narrower estimate of Si,in. While it could be true that Eq. (1) is satisfied, we still need a non-trivial size of Si,in for the framework to be useful. For example, if Si,in constrains face angle rotations to be within 1◦ then it may not be practical for the end-user.
For auditing ML models thoroughly, we require clear separation between the development and testing phases (i.e. black-box verification). However, it might also be desirable in practice to train the model in such a way that the unit tests are likely to be satisfied in the first place. In this case, we do have a tighter connection between the designer and the verifier. We show that by relaxing the black-box constraint, we can simultaneously address the previously listed challenges in a white-box setting.
Now that we have access to the internal working and design of the ML model f , we propose to bypass the image generation step in our verification process through the use of latent disentangled representations. More specifically, consider a ML model mapping f : X → Z → Y (denote by fd : Z → Y the downstream task) and a generative model mapping g : X → Z → X̂ , such that f and g share a common latent space Z by virtue of having a common encoder e(·) (Fig. 2). Since Si,in is a subset of the range of e, we have Si,in ⊆ Z . This further implies that we do not have to apply IBP through g and the whole f . Instead we only have to apply it through fd, which does not involve the expansion to the pixel space X . We show in the experiment (Section 4) that this is important to have a practically useful Si,in. In addition, AuditAI also alleviates the need of having a perfect generative model, as long as we can learn a latent space Z through an inference mechanism. Learning the latent space. There are three requirements for the latent space. First, it should be semantically-aligned for us to specify unit tests in this space. A good example is disentangled representation (Higgins et al., 2018; Tran et al., 2017), where a set of dimensions of the latent code would correspond to a semantically aligned variation of the original image. As shown in Figure 2, a latent dimension could correspond to the pose variation, and we can select ei to be the value of this dimension, and Si,in as the proper range that the model would be verified for. Second, our model should be verifiable, where the latent space is learned such that the corresponding Si,in is as large as possible given a specification function F . In this case, AuditAI can be seen as doing certified training (Zhang et al., 2019b) to improve the verifiability of the model. Finally, the latent space should be able to perform well on the downstream task through fd. Combining these three criteria, our full training criteria: L = Ltask + γLspec + δLgen combines three losses Lgen, Lspec, and Ltask that would encourage interpretability through the latent space of a generative model, verifiability, and task performance respectively. γ and δ are relative weights (between 0 and 1) for the loss function terms. We explain each of the losses below:
Verifiability (Lspec). Let fd be a feedforward model (can have fully connected / convolutional / residual layers) with K layers zk+1 = hk(Wkzk + bk), k = 0, ...,K − 1, where, z0 = e(x), zK denotes the output logits, and hk is the activation function for the kth layer. The set of variations Si,in could be such that the lp norm for the ith latent dimension is bounded by ϵ, i.e. Si,in = {z : ||zi − z0,i||p ≤ ϵ}. We can bound the output of the network Sout = {zK : lK ≤ zK ≤ uK} through a variant of interval bound propagation (IBP). Let the specification be F (z, y) = cT zK + d ≤ 0, ∀z ∈ Si,in, zK = fd(z). For a classification task, this specification implies that the output logits zK should satisfy a linear relationship for each latent space variation such that the classification outcome argmaxi zK,i remains equal to the true outcome ytrue corresponding to z0. To verify the specification, IBP based methods search for a counter-example, which in our framework amounts to solving the following optimization problem, and checking whether the optimal value is ≤ 0.
max z∈Sin
F (z, y) = cT zK + d s.t. zk+1 = hk(Wkzk + bk) k = 0, ...,K − 1 (2)
By following the IBP equations for bound-propagation, we can obtain upper and lower bounds [zK , zK ] which can be used to compute the worst case logit difference zK,y − zK,ytrue between the
true class ytrue and any other class y. We define ẑK = zK,y (if y ̸= ytrue); ẑK = zK,ytrue (otherwise). Then, we can define Lspec as Lspec = CE(ẑK , ytrue). In practice, we do not use IBP, but an improved approach CROWN-IBP (Zhang et al., 2019b) that provides tighter bounds and more stable training, based on the AutoLiRPA library (Xu et al., 2020). We mention details about this in the Appendix.
Task Performance (Ltask). Let, CE(·) denote the standard cross-entropy loss. Ltask captures the overall accuracy of the downstream task and can be expressed as Ltask = CE(zK , ytrue).
Generative Model (Lgen ). Finally, we have a loss term for the generative model, which could be a VAE, a GAN, or variants of these. If the model is a GAN, then we would have an optimization objective for GAN inversion. An assumption is being able to learn a disentangled latent space with semantically aligned concepts. Let the overall loss be Lgen which could also encapsulate other losses for more semantically-aligned disentanglement. Typically we would train this generative model on a large amount of unlabelled data that is not available for training the classifier we are auditing.

heading: 2.4 DEPLOYMENT
text: Based on the perturbation radius ϵ and the nominal z0, we have different ranges [zn0 − 1iϵ, zn0 + 1iϵ] for the verified error at the end of training the classifier. Here, zn0 = e(x
n) ∀ n = 1, ...N in the dataset Dtrain and 1i = 1 for the ith dimension (corresponding to the ith unit test) and is 0 otherwise. We can convert this per-sample bound to a global bound for the ith latent code, [zi, zi] by considering an aggregate statistic of all the ranges, for example
[zi, zi] = [µ({zn0,i − 1iϵ}Nn=1)− σ({zn0,i − 1iϵ}Nn=1), µ({zn0,i + 1iϵ}Nn=1) + σ({zn0,i + 1iϵ}Nn=1)]
Here, µ(·) denotes the mean and σ(·) denotes the standard deviation. Note that this is a global bound on the range of variations for only the latent dimension corresponding to the unit test, and does not concern the other dimensions. During deployment, the end-user receives the model spec-sheet containing values of [zi, zi] for each unit test i and results with different values of perturbation radius ϵ. Now, if the end-user wants to deploy the model on an evaluation input xeval, they can encode it to the latent Z space to get code zeval and check whether zeval,i ∈ [z0,i, z0,i] in order to decide whether to deploy the model for this evaluation input.

heading: 3 THEORETICAL RESULTS
text: We show that although AuditAI considers perturbations in the latent space that allows a large range of semantic variations in the pixel-space, it retains the theoretical guarantees of provable verification analogous to IBP-based adversarial robustness (Zhang et al., 2019b; Xu et al., 2020). Theorem 1 (Verification. The auditor can verify whether the trained model from the designer satisfies the specifications, by generating a proof of the same). Let x ∈ X be the input, z0 = e(x) be the latent code, fd be a feed-forward neural network with bounded derivatives, and Si,in = {z : ||zi−z0,i||p ≤ ϵ} be the set of latent perturbations. Then, the auditor is guaranteed to be able to generate a proof for verifying whether the linear specification on output logits cT zK + d ≤ 0 ∀z ∈ Si,in, zK = fd(z) (corresponding to unit test i) is satisfied.
Proof. Here we provide a proof sketch and mention details in the Appendix A.2. The verifier can generate a proof by searching for a worst-case violation maxz∈Si,in c
T zK + d s.t. zk+1 = hk(Wkzk + bk) k = 0, ...,K − 1. If the optimal value of this < 0, then the specification is satisfied. The verifier applies Interval-bound Propagation (IBP) to obtain an upper bound zK on the solution of this optimization problem, and checks whether the upper bound zK < 0.

heading: 4 EXPERIMENTS
text: We perform experiments with four datasets in different application domains. We choose the datasets ImageNet, LSUN, FFHQ, and CheXpert where current state of the art generative models have shown strong generation results (Karras et al., 2019; 2017; Brock et al., 2018). We show an illustration of what the generated images under latent perturbations look like in Fig 3. Through experiments, we aim to understand the following:
1. How do the verified error rates vary with the magnitude of latent perturbations? 2. How does AuditAI compare against pixel-perturbation based verification approaches? 3. How does AuditAI perform during deployment under domain shift?
4.1 IMAGENET
ImageNet contains 1000 different classes of objects. We consider a BigBiGAN model (Donahue & Simonyan, 2019) as the base generative model such that the latent space is class conditional, and we can obtain latent codes corresponding to specific classes. So, latent perturbations correspond to variations in different images within the same class. The specification for verification is that the classifier outputs the correct class for all latent perturbations ϵ. This is an unit test because we can verify with respect to each class separately. Table 1 shows results for different ϵ on the test set. The results confirm the intuition that increasing ϵ increases the verified error due to wider latent perturbations. In Table 2, we compare a pixel-based robust
training approach with our framework, both trained with the same underlying algorithm CROWNIBP (Zhang et al., 2019b). For the same verified test error, we have the corresponding latent perturbation for AuditAI (call it ϵ1) and the pixel perturbation for the pixel-based approach (call it ϵ2). Based on ϵ2 we compute the bound for the intermediate latent node, ϵ21. Since comparing ϵ1 and ϵ21 directly may not be meaningful due to different nominal values of the latent code, we consider the fraction ϵ/znom and plot the resulting values in Table 2. We observe that ϵ1/znom1 >> ϵ21/znom21 indicating tolerance to much larger latent variations. Since a wider latent variation corresponds to a wider set of generated images, AuditAI effectively verifies over a larger range of image variations, compared to perturbations at the level of pixels. In addition, when we translate the latent perturbations of AuditAI to the pixel space of the generative model, we obtain on average 20%, and 17% larger variations measured as L2 distances compared to the pixel-based approach for a verified error of 0.88 and 0.50 respectively.

heading: 4.2 CHEXPERT
text: CheXpert (Irvin et al., 2019) contains 200,000 chest radiograph images with 14 labeled observations corresponding to conditions like pneumonia, fracture, edema etc. We consider a PGGAN (Karras et al., 2017) as the base generative model such that the latent space is class-conditional. We consider three separate binary classification tasks with respect to the presence or absence of three conditions:
pneumonia, fracture, and edema. We consider the entire dataset for training the generative model, but for the classifiers we only use positive (presence of the condition) and negative (absence of the condition) data with an 80-20 train/test split. Table 3 shows results for different ϵ on the test set for each classifier.
As a sanity check, in order to determine whether the generative model behaves correctly with respect to class conditional generation, we consider an off-the-shelf classifier for pneumonia detection trained on real images of pneumonia patients (Rajpurkar et al., 2017). We randomly sample 1000 images from the generative model for each value of ϵ = 0.5, 1.0, 1.5, 2.0 and evaluate the accuracy of the offthe-shelf classifier on these generated images. We obtain respective accuracies 85%, 84%, 81%, 75% indicating highly reliable generated images.
Deployment under domain-shift. In order to better understand the process of deploying the trained model on a dataset different from the one used in training, we consider the dataset NIH Chest Xrays (Wang et al., 2017). This dataset contains (image, label) pairs for different anomalies including pneumonia and edema. We perform certified training on CheXpert for different values of ϵ (results of this are in Table 3) and deploy the trained model to the end-user. The end-user samples 5000 images from the NIH Chest X-rays dataset, encodes them to the latent space with trained encoder e(·) and uses the trained downstream task classifier fd(·) to predict the anomaly in the image. In Table 4, we list the precision, recall, and overall accuracy among the 5000 images for two conditions, presence of pneumonia and edema. We observe that the results for AuditAI are on average 5% higher than the pixel-based approach. This intuitively makes sense because from Table 2 and section 4.1, we see that AuditAI covers about 20% larger variations in the pixel space and so the odds of the images at deployment lying in the verified range are higher for AuditAI.

heading: 4.3 FFHQ
text: Flicker Faces HQ (Karras et al., 2019) contains 70,000 unlabeled images of normal people (and not just celebrities as opposed to the CelebA (Liu et al., 2015) dataset). We train a StyleGAN model (Karras et al., 2019) on this dataset and use existing techniques (Bau et al., 2020a; Shen & Zhou, 2020; Shen et al., 2020) to identify directions of semantic change in the latent space. We identify latent codes (set of dimensions of Z) corresponding to expression (smile), pose, and presence of eyeglasses. We define the task for the classifier to be detection of whether eyeglasses are present and define unit tests to be variations in the latent code with respect to expression and pose (while keeping the code for eyeglasses invariant). Table 5 shows the results of these unit tests corresponding to different latent perturbations ϵ. We see that the verified error is up to 20% for over 50% larger variations compared to nominal values. Based on this spec-sheet table, during deployment, the end-user can check whether the encoding of input image lies in the desired accuracy ranges for pose and expression, and then decide whether to use the model.

heading: 4.4 LSUN TOWER
text: The LSUN Tower dataset (Yu et al., 2015) contains 50,000 images of towers in multiple locations. Similar to the FFHQ setup above, we train a StyleGAN model on this dataset and use existing techniques (Shen & Zhou, 2020; Zhu et al., 2020) to identify directions of semantic change in the latent space. We identify latent codes corresponding to clouds, vegetation, and sunlight/brightness. We define the task for the classifier to be detection of whether vegetation is present and define unit tests to be variations in the latent code with respect to how cloudy the sky is, and how bright the scene is (while keeping the code for vegetation invariant). Table 5 shows the results of these unit tests corresponding to different latent perturbations ϵ. We see that the
verified error is up to 18% for over 50% larger variations compared to nominal values. Based on this spec-sheet table, during deployment, the end-user can check whether the encoding of input image lies in the desired accuracy ranges for clouds in the sky and brightness of the scene, and then decide whether to use the model.
4.5 ATTACKING IMAGES AUDITED BY AUDITAI IN THE PIXEL-SPACE
In this section, we analyze what fraction of images audited by AuditAI can be attacked in the pixel-space through adversarial corruptions. We create test examples with varying brightness of the scene, corresponding to the setting in Table 5. These are real variations directly by modifying pixels to changing the brightness of the scene . We evaluate AuditAI trained the same way as in Table 5, but evaluated on this test set after certified training. For ϵ = 0.5, 96 out of 1000 images (only 9.6%) certified by AuditAI can be attacked in the pixel-space, while for ϵ = 1.5, 85 out of 1000 images (only 8.5%) certified by AuditAI can be attacked. We use CROWN-IBP (Zhang et al., 2019b) to determine if an image is attackable in the pixel-space. These results show that the certification provided by AuditAI is robust, and although verification is done in the latent space of a generative model, the results hold under real pixel-perturbations as well.

heading: 5 HUMAN STUDY: HOW REALISTIC ARE THE GENERATED IMAGES?
text: We employ Amazon Mechanical Turk (Buhrmester et al., 2016) to better understand the generative model trained for the Chest X-ray dataset and determine the limits of latent space variations for which generations are realistic. This study is to determine the maximum value of ϵ for which generations are realistic to the human eye, such that we verify and report in the spec-sheet values of ϵ only up to the range of realistic generations. We note that this study is to understand the generative model and not the trained classifier. We employ a similar experimental protocol as (Isola et al., 2017; Zhang et al., 2016) and mention details in the Appendix A.4. We generated 2000 images by sampling latent codes within each ϵ range of variation. Alongside each ϵ we represent the % with respect to the nominal value it corresponds to (the nominal value of ϵ is 2.0, so ϵ = 0.5 is 25% of 2.0) in Fig 4. We see that the humans who participated in our study had close to 50% correct guesses for ϵ up to 1.0, indicating generations indistinguishable from real images. For ϵ ≥ 4.0 the correct guess rate is above 70% indicating that the generations in these ranges of latent variations are not realistic, and so the verified accuracy for these ranges should not be included in the spec-sheet.
6 RELATED WORK
Multiple prior works have studied a subset of the audit problem in terms of adversarial robustness (Raghunathan et al., 2018a; Dvijotham et al.). Adversarial examples are small perturbations to the input (for images at the level of pixels; for text at the level of words) which mislead the deep learning model. Generating adversarial examples has been widely studied (Xu et al., 2018; Zhang et al., 2019a) and recent approaches have devised defenses against adversarial examples (Xie et al., 2020; Zhang et al., 2019b). Some of these approaches like (Gowal et al., 2018) and (Zhang et al., 2019b) provide provable verification bounds on an output specification based on the magnitude of perturbations in the input. These approaches have largely showed robustness and verification to norm bounded adversarial perturbations
without trying to verify with respect to more semantically aligned properties of the input. Some papers (Mohapatra et al., 2020; Ruoss et al., 2020; Balunović et al., 2019; Wong & Kolter, 2020) consider semantic perturbations like rotation, translation, occlusion, brightness change etc. directly in the pixel space, so the range of semantic variations that can be considered are more limited. This is a distinction with AuditAI, where by perturbing latent codes directly (as opposed to pixels), the range of semantic variations captured are much larger.
A related notion to auditing is expalainable AI (Gunning, 2017). We note that auditing is different from this problem because explanations can be incorrect while remaining useful. Whereas in auditing, our aim is not to come up with plausible explanations for why the model behaves in a certain way, but to quantify how it behaves under semantically-aligned variations of the input.
Some papers (Mandelbaum & Weinshall, 2017; Van Amersfoort et al., 2020) have used model confidence and ucnertainty estimates for rejecting out-of-distribution samples at test time, which is a form of auditing. In (Mitchell et al., 2019) and (Gebru et al., 2018), the authors proposed a checklist of questions that should be answered while releasing DL models and datasets that relate to their motivation, intended use cases, training details, and ethical considerations. These papers formed a part of our motivation and provided guidance in formalizing the audit problem for DL models. We provide a detailed survey of related works in section A.6.

heading: 7 DISCUSSION AND CONCLUSION
text: In this paper we developed a framework for auditing of deep learning (DL) models. There are increasingly growing concerns about innate biases in the DL models that are deployed in a wide range of settings and there have been multiple news articles about the necessity for auditing DL models prior to deployment12. Our framework formalizes this audit problem which we believe is a step towards increasing safety and ethical use of DL models during deployment.
One of the limitations of AuditAI is that its interpretability is limited by that of the built-in generative model. While exciting progress has been made for generative models, we believe it is important to incorporate domain expertise to mitigate potential dataset biases and human error in both training & deployment. Currently, AuditAI doesn’t directly integrate human domain experts in the auditing pipeline, but indirectly uses domain expertise in the curation of the dataset used for creating the generative model. Although we have demonstrated AuditAI primarily for auditing computer vision classification models, we hope that this would pave the way for more sophisticated domain-dependent AI-auditing tools & frameworks in language modelling and decision-making applications.
1https://www.technologyreview.com/2021/02/11/1017955/auditors-testing-ai-hiring-algorithms-bias-bigquestions-remain/, Feb 11, 2021
2https://www.wired.com/story/ai-needs-to-be-audited/, Jul 10, 2019

heading: A APPENDIX

heading: A.1 PRELIMINARIES: INTERVAL-BOUND PROPAGATION
text: In this section, we provide a preliminary treatment of Interval-Bound Propagation based robust training and verification. Let f be a feedforward classifier model that outputs one of N classes. The input to the network is an image x0, and it has a certain ground truth class ytrue. The classifier is trained to minimize a certain misclassification loss. The verification problem is to check whether there is some set Sin(x0) around perturbations of x0 such that the classification output of the model remains invariant from that of ytrue.
Let f have K layers zk+1 = hk(Wkzk + bk), k = 0, ...,K − 1, such that z0 ∈ Sin(x0), zK denotes the output logits, and hk is the activation function for the kth layer. If we consider the set of variations to be Sin(x0) = {x|||x − x0||∞ ≤ ϵ}, then we want to verify the specification that argmaxi zK,i = ytrue ∀ z0 ∈ Sin(x0). We can write this as a general linear specification cT zK + d ≤ 0 ∀ z0 ∈ Sin(x0) To verify the specification, IBP based methods search for a counter-example that violates the specification constraint, by solving the following optimization problem and checking whether the optimal value ≤ 0.
max x∈Sin
cT zK + d s.t. zk+1 = hk(Wkzk + bk) k = 0, ...,K − 1 (3)
Since solving this optimization problem exactly is NP-hard (Zhang et al., 2019b), IBP finds an upper bound on the optimal value and checks whether the upper bound ≤ 0. To get an upper bound on zK , we can propagate bounds for each activate zk through axis-aligned bounding boxes, zk,i(ϵ) ≤ zk,i ≤ zk,i(ϵ), where i indexes dimension. Based on this, the specification is upperbounded by zK,y(ϵ)− zK,ytrue(ϵ). In addition to the verification problem, IBP can be used to perform certified training such that the specification is likely to be satisfied in the first place at the end of training. For this, the overall training loss would consist of two terms: usual classification loss like cross-entropy that maximizes log likelihood l(zK , ttrue), and a loss term that encourages satisfiying the specification l(ẑK(ϵ), ttrue). Here, ẑK,y(ϵ) = zK,y(ϵ) (if y ̸= ytrue) and ẑK,y(ϵ) = zK,ytrue(ϵ) (if y = ytrue). So, the overall loss for certified training can be represented as:
L = χl(zK , ttrue) + (1− χ)l(ẑK(ϵ), ttrue)
As reported in (Gowal et al., 2018; Zhang et al., 2019b; Xu et al., 2020), to stabilize training, χ is varied during training such that for a few initial epochs χ = 1 (normal training) and its value is slowly increased so that robust training kicks in gradually.

heading: A.2 PROOF OF THE THEOREM
text: Theorem 1 (Verification. The verifier can verify whether the trained model from the designer satisfies the specifications, by generating a proof of the same). Let x ∈ X be the input, z0 = e(x) be the latent code, fd be a feed-forward neural network with bounded derivatives, and Si,in = {z : ||zi−z0,i||p ≤ ϵ} be the set of latent perturbations. Then, the verifier is guaranteed to be able to generate a proof for verifying whether the linear specification on output logits cT zK + d ≤ 0 ∀z ∈ Si,in, zK = fd(z) (corresponding to unit test i) is satisfied.
Proof. Revisiting the notation in section 2, consider a network mapping f : X → Z → Y (denote by fd : Z → Y the downstream task) and a generative model mapping g : X → Z → X̂ , such that f and g share a common latent space Z by virtue of having a common encoder e(·) (Figure 2). Here we provide a proof based on fully-connected feed-forward network architecture for fd, an arbitrary architecture for f and using the Interval-Bound Propagation (IBP) method for obtaining output bounds. For a general network architecture for fd, we refer the reader to a recent library AutoLirpa (Xu et al., 2020).
Given input x ∈ X , let z0 = e(x) be the latent code, and Si,in = {z : ||zi − z0,i||p ≤ ϵ} be the set of latent perturbations. Let, z be d−dimensional. Here, zi denotes the dimensions(s) of z that are
perturbed, such that z = zd−i ⊕ zi. Without loss of generality, we can assume all the dimensions in zi to be contiguous. The verifier can generate a proof by searching for a worst-case violation
max z∈Si,in
cT zK + d s.t. zk+1 = hk(Wkz k + bk) k = 0, ...,K − 1
For the sake of simplicity, first consider the case where j = d i.e. all dimensions of z are perturbed. So, Sin = {z0 : ||z0 − z00 ||p ≤ ϵ. Here, we have denoted by z0 the latent code in Z space, and will use zk+1 = hk(Wkzk + bk) k = 0, ...,K − 1 to denote the subsequent intermediate variables in f1 : Z → Y . Based on Holder’s inequality we can obtain linear bounds for the first variable z1, [z1, z1] as follows:
z1 = −ϵ||W 0||q +W 0z0 + b0; z1 = −ϵ||W 0||q +W 0 z0 + b 0 ; 1/p+ 1/q = 1
Here, || · ||q denotes computation of the lq−norm for each row in the matrix and the values of W 0,W 0 can be computed with the functions described in Appendix A.1 of (Xu et al., 2020) depending on the type of non-linearity in h0(·). Now, when j ̸= d i.e. only j dimensions of d are perturbed, without loss of generality, we can consider all of the j dimensions to be contiguous such that z0 = z0d−j ⊕ z0j . We can then compute [z1j , z 1 j ] as follows:
z1j = −ϵ||W 0 j ||q +W 0 jz 0 + b0j ; z 1 = −ϵ||W 0j ||q +W 0 jz 0 + b 0 j ; 1/p+ 1/q = 1
We can compute z1d−j as follows:
z1d−j = h 0(W 0z0d−j + b 0)
Finally, we can obtain [z1, z1] as follows:
z1 = z1d−j ⊕ z1j ; z1 = z1d−j ⊕ z1j
Now, given the bound [z1, z1] and the relation zk+1 = hk(Wkzk + bk) k = 0, ...,K − 1, we can obtain the bound for zK , [zK , zK ] by recursively computing successive bounds as follows:
zk+1 = hk ( W ( zk + zk
2
) + b− |W | ( zk − zk
2
))
zk+1 = hk ( W ( zk − zk
2
) + b+ |W | ( zk − zk
2 )) Here we have assumed that hk is an element-wise monotonic function, which is is true for for most common actions like ReLU, tanh, sigmoid etc. Using [zK , zK ], the verifier can construct an upper and lower bound on the solution of maxz∈Si,in c T zK + d
max zK<z<zK
cT zK + d
It is important to note that the proof the verifier generates to check whether the specification holds relies on computing an upper bound zK and checking whether the upper bound zK < 0. If the upper bound is not tight, then there may be cases when the true solution < 0 (meaning the specification in Theorem 1 is indeed satisfied) while the upper bound zK > 0 (implying the verifier will state that the specification is not satisfied). This form of err on the side of caution is a natural consequence of proof by generating a worst case example, and follows directly from IBP.
A.3 IMPLEMENTATION DETAILS
We use a 32-GB V100 GPU for all our experiments. The implementation is in Python with a combination of PyTorch and Tensorflow deep learning libraries. Details about the specific experiments are mentioned below:
ImageNet. We use a pretrained BigBiGAN https://colab.research.google.com/ github/tensorflow/hub/blob/master/examples/colab/bigbigan_with_tf_ hub.ipynb as the base generative model, such that the encoder encodes images to the latent space. The downstream classifier from the latent space consists of 5 fully connected layers with ReLU non-linearities. We use ADAM optimizer with a learning rate of 0.0005. For each value of ϵ L2 perturbation in Table 1, we train for 100 epochs, using the AutoLiRPA library’s implementation of CrownIBP https://github.com/KaidiXu/auto_LiRPA. The first 5 epochs are standard training for warming up, and the rest of the epochs are robust training. The training time for 100 epochs is about 8 hours.
CheXpert. We train a PGGAN https://github.com/tkarras/progressive_ growing_of_gans on the CheXpert dataset. In order to learn latent embeddings from raw images, we need an inference mechanism. For this, we perform GAN inversion of this pretrained generator, using https://github.com/davidbau/ganseeing/blob/release/run_ invert.sh to obtain an encoder for projecting images to the latent space. The downstream classifier from the latent space consists of 5 fully connected layers with ReLU non-linearities. We use ADAM optimizer with a learning rate of 0.0005. For each value of ϵ L2 perturbation in Table 1, we train for 100 epochs, using the AutoLiRPA library’s implementation of CrownIBP https://github.com/KaidiXu/auto_LiRPA. The first 5 epochs are standard training for warming up, and the rest of the epochs are robust training. The training time for 100 epochs is about 7 hours.
LSUN and FFHQ. We train StyleGAN models https://github.com/NVlabs/ stylegan2-ada-pytorch on the FFHQ and LSUN datasets, and perform GAN inversion using https://github.com/genforce/idinvert_pytorch to obtain respective encoders for a disentangled latent space. The downstream classifier from the latent space consists of 5 fully connected layers with ReLU non-linearities. We use ADAM optimizer with a learning rate of 0.0005. For each value of ϵ L2 perturbation in Table 1, we train for 100 epochs, using the AutoLiRPA library’s implementation of CrownIBP https://github.com/KaidiXu/auto_LiRPA. The first 5 epochs are standard training for warming up, and the rest of the epochs are robust training. The training time for 100 epochs is about 7 hours each.

heading: A.4 DETAILS ABOUT THE AMAZON MTURK STUDY
text: Here we provide more details about the setup for the Amazon MTurk study whose results we presented in Fig. 4. We designed each Human Intelligence Task (HIT) to be comprised of 10 pairs of images sequentially presented, such that each pair consists of a real and a generated image. For different values of ϵ we show examples of images from each of the categories presented in the HITs through Fig. 5.
We recruited participants only from the “Master Worker” category. As defined in https://www. mturk.com/worker/help, “a Master Worker is a top Worker of the MTurk marketplace that has been granted the Mechanical Turk Masters Qualification.” These Workers have consistently demonstrated a high degree of success in performing a wide range of HITs across a large number of Requesters. The participants were paid 0.5 dollars for each HIT (i.e. for 10 pairs of images). Each pair was shown to the participants for 2 seconds, after which the images disappeared from the screen, but they could take as much time as they wanted to decide and form a response. We restricted the number of HITs per participant to 20.
The participants were shown the exact text below: Choose the more realistic image between options A and B. For each pair, you have 5 seconds to view the image and unlimited time to make the decision. Each task consists of 10 image pairs.

heading: A.5 RESULTS OF VERIFICATION WITH PRE-TRAINED CLASSIFIER
text: In this experiment, we pre-train the classifier through certified training with ϵ = 1.0 and perform verification for different values of ϵ.

heading: A.6 EXTENDED RELATED WORKS
text: Adversarial robustness. Multiple prior works have studied a subset of the audit problem in terms of adversarial robustness (Carlini et al., 2019; Jia et al., 2019; Gowal et al., 2018; Zhang et al., 2018; Singh et al., 2019; Weng et al., 2018; Singh et al., 2018; Wang et al., 2018; Raghunathan et al., 2018a;b; Dvijotham et al.). Adversarial examples are small perturbations to the input (for images at the level of pixels; for text at the level of words) which mislead the deep learning model. Generating adversarial examples has been widely studied (Zhao et al., 2017; Athalye et al., 2018; Carlini & Wagner, 2017a;b; Goodfellow et al., 2015; Madry et al., 2018; Papernot et al., 2016; Xiao et al., 2019b; 2018b;c; Eykholt et al., 2018; Chen et al., 2018; Xu et al., 2018; Zhang et al., 2019a) and recent approaches have devised defenses against adversarial examples (Guo et al., 2018; Song et al., 2017; Buckman et al., 2018; Ma et al., 2018; Samangouei et al., 2018; Xiao et al., 2018a; 2019a; Xie et al., 2020; Cohen et al., 2019; Gowal et al., 2018; Zhang et al., 2019b). Some of these approaches like (Gowal et al., 2018) and (Zhang et al., 2019b) provide provable verification bounds on an output specification based on the magnitude of perturbations in the input. These approaches have largely showed robustness and verification to norm bounded adversarial perturbations without trying to verify with respect to more semantically aligned properties of the input. Some papers (Mohapatra et al., 2020; Ruoss et al., 2020; Balunović et al., 2019) consider semantic perturbations like rotation, translation, occlusion, brightness change etc. directly in the pixel space, so the range of semantic
variations that can be considered are more limited. This is a distinction with AuditAI, where by perturbing latent codes directly (as opposed to pixels), the range of semantic variations captured are much larger. In (Wong & Kolter, 2020), the authors model perturbation sets for images with perturbations (like adversarial corruptions) explicitly such that a conditional VAE can be trained. While, for AuditAI, we identify directions of latent variations that are present in pre-trained GANs, and as such do not require explicit supervision for training the generative model, and can scale to datasets like ImageNet and CheXpert, and high dimensional images like that in FFHQ.
Neural network interpretability. With the rapid rise of highly reliable generative models, many recent works have sought to analyze the latent space of such models and how the latent space can be manipulated to obtain semantic variations in the output image. (Bau et al., 2021) use text embeddings from CLIP (Radford et al., 2021) to perform directed semantic changes in the generated images, for example introduction of a particular artifact in the room or change in the color of a bird. (Bau et al., 2020a; Shen & Zhou, 2020; Shen et al., 2020) identify latent code dimensions corresponding to pose of the body/face, expression of the face, orientation of beds/cars in the latent space of generative models like PGGAN (Karras et al., 2017) and StyleGAN (Karras et al., 2019). By manipulating these latent dimensions, the output images can be controllably varied. In addition, there have been other papers that sought to understand what the neural network weights are learning in the first place (Bau et al., 2020b; Yeh et al., 2020) in an attempt to explain the predictions of the networks.
Auditing. While we proposed a framework for auditing of DL models, a complimentary problem is to audit datasets that are used for training DL models. In (Gebru et al., 2018), the authors proposed a checklist of questions to be answered while releasing datasets that relate to the motivation, composition, collection process, processing, and distribution of the dataset. In (Mitchell et al., 2019), the authors proposed a checklist of questions that should be answered while releasing DL models that relate to their motivation, intended use cases, training details, and ethical considerations. These papers formed a part of our motivation and provided guidance in formalizing the audit problem for DL models.

Review summaries:
This paper proposes a new and useful direction: AI model audit. The proposed solution (framework) is very interesting. The experiments show the effectiveness of the proposed method.

This paper presents, AuditAI, a system for verifying that a trained model meets a particular `specification', and also for certified training. The system uses a generative model to construct embeddings for inputs and then tests whether these embedding vectors belong to a particular set. Membership in the pre-specified set is reduced to satisfying the test. The key technical insight in this work is applying the interval bound propagation technique to embedding/latent codes in order to verify semantic behaviors of trained models.

This paper presents a framework for auditing deep learning models in regards to a specification. The goal is to increase the confidence in a trained model. The auditing is performed by generating variations in input data to evaluate the boundaries in the input for an expected output. An evaluation was performed against a pixel-based training approach and under consideration of 4 different datasets.