Neural Network Verification

This is the blog post covering the topics discussed in "Bias Field Robustness Verification of Large Neural Image Classifiers" [1] by P. Henriksen, K. Hammernik, D. Rueckert, and A. Lomuscio (published at BMVC 2021) and "Efficient Neural Network Verification via Adaptive Refinement and Adversarial Search" [2] by P. Henriksen and A. Lomuscio (published at ECAI 2020).

Introduction

Despite their black-box nature, it is easy to mistake neural networks as bullet-proof predictors due to their incredible performance in tasks across scientific domains. But can we trust neural networks in safety-critical domains such as autonomous driving, robotics, or medicine? Numerous publications [26, 27, 28, 29, 30] have demonstrated adversarial attacks on standard architectures in these domains. These attacks include intentionally designed (often minor) perturbations to an input that cause the neural network to make a mistake [3]. While these attacks are artificial, the implication is that these networks are not fit for real-world applications (yet).

Verification of neural networks aims to establish trust formally by proving that a neural network has some desired properties [6a]. For instance, one such property, which we consider in this blog post, is robustness, i.e. the output of a neural network not spuriously changing within a pre-defined perturbation set.

Robustness Verification

Broadly speaking, to verify the robustness of a neural network for a perturbation set, we prove that the prediction of a network for point $//<![CDATA[ \begin{array}{l}x_{0}\end{array} //]]>$ is stable in a perturbation set around this point. More formally, given an input space $//<![CDATA[ \begin{array}{l}\mathcal{D}_{x}\end{array} //]]>$ and an output space $//<![CDATA[ \begin{array}{l}\mathcal{D}_y\end{array} //]]>$, an input constraint imposed by $//<![CDATA[ \begin{array}{l}\mathcal{X} \subseteq \mathcal{D}_x\end{array} //]]>$ with $//<![CDATA[ \begin{array}{l}x_0 \in \mathcal{X}\end{array} //]]>$, which represents the perturbation set, and an output constraint $//<![CDATA[ \begin{array}{l}\mathcal{Y} \subseteq \mathcal{D}_y\end{array} //]]>$, the verification problem requires showing that the following assertion holds [5]:

The perturbation set may simply be a $//<![CDATA[ \begin{array}{l}\epsilon\end{array} //]]>$ ball for any $//<![CDATA[ \begin{array}{l}\ell_{p}\end{array} //]]>$ norm. More complex perturbations, such as bias fields [1], or combinations of multiple perturbations may also be defined that might have a more direct connection to real-world concerns.

To give an example for this definition: Suppose we have a network that predicts a score of whether a magnetic resonance imaging (MRI) image depicts no abnormalities. If it says $//<![CDATA[ \begin{array}{l}x_0\end{array} //]]>$ represents no abnormality, then we want all points x in the perturbation set $//<![CDATA[ \begin{array}{l}\mathcal{X}\end{array} //]]>$ around $//<![CDATA[ \begin{array}{l}x_0\end{array} //]]>$ to receive a positive score, i.e. belonging to the class "normal". We prove that by showing that the worst-case example within this set still receives a positive score:

Challenges

There are two main challenges in the robustness verification of neural networks that stem from the problem definition and the idea of neural networks themselves:

1. Infinite cardinality of the perturbation set: We consider a perturbation set of inputs, i.e. a continuous, multi-dimensional input set, which effectively contains an infinite number of points. Merely taking a large sample and verifying a neural network based on this subset is insufficient as seemingly robust networks might still be vulnerable to adversarial attacks [4, 5].
2. Non-linearity of activation functions: Non-linear activation functions do not permit straightforward bounds estimation in every case. The Rectified Linear Unit (ReLU) activation function has three distinct states based on the lower and upper bounds of a given input set: Two stable states (strictly negative, or strictly positive), and an unstable state.

Approaches

A classification of verification has been proposed in [5] based on three categories of analysis:

• Reachability: Layer-by-layer reachability analysis of the neural network. These methods compute the reachable set $//<![CDATA[ \begin{array}{l}\mathcal{R}(\mathcal{X}, f) := \{ y: y = f(x), \forall x \in \mathcal{X} \}\end{array} //]]>$, with the verification problem assumption being violated iff $//<![CDATA[ \begin{array}{l}\mathcal{R}(\mathcal{X}, f) \nsubseteq \mathcal{Y}\end{array} //]]>$ [5]. Depending on the implementation, the reachability set may also be reported for individual neurons.
• Optimization: Falsification of the assertion through optimization. The function represented by the neural networks is the core constraint in this optimization alongside the constraints to describe the perturbation set $//<![CDATA[ \begin{array}{l}\mathcal{X}\end{array} //]]>$ and output set $//<![CDATA[ \begin{array}{l}\mathcal{Y}\end{array} //]]>$. Activation functions may be encoded as linear constraints in primal optimization through the use of mixed-integer programming [10, 11]. Due to the very nature of neural networks and its activations functions [8, 9], the resulting optimization problem is not convex and it has been shown in [12] that it is NP-complete for deep neural networks with ReLU activation functions. Dual optimization strategies have also been conceived [13, 14].
• Search: Finding a counterexample to falsify the assertion. This approach is usually combined with either reachability or optimization as they provide directions for the search [5].

Both verification methods discussed in this blog post are sound, i.e. they only report robustness if the network is indeed robust. Furthermore, the methods are also complete, i.e. if the network is robust, they will report it. The final performance of the verification method hinges on the chosen approach to tackle these challenges, desired precision of the lower and upper bounds, and efficiency considerations [5]: Sound but incomplete reachability-based methods are highly efficient nowadays [5, 6a] but turning them into complete methods requires the sacrifice of solving performance [6b, 7].

In this blog post, we consider two state-of-the-art verification algorithms with VeriNet [2] being a representative of the combination of search and reachability, and $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN [6b, 7] being an amalgamation taking inspirations from every category. In this blog post, we omit optimization-based algorithms to limit the scope. To simplify the examples, we operate with binary classification neural networks.

alpha-beta-CROWN

The winning verification method $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN [6b, 7] in the 2021 edition of the annual International Verification of Neural Networks Competition (VNN-COMP) [7] represents the combination of two previous versions aptly named $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$-CROWN [16] and $//<![CDATA[ \begin{array}{l}\beta\end{array} //]]>$-CROWN [17]. Before discussing their core contributions, we first explore the underlying CROWN verification algorithm [23] in-depth to grasp how a verification algorithm operates.

CROWN Algorithm

CROWN [23] seeks to efficiently compute a linear lower bound that permits testing if the label of the worst-case sample is not flipped, rendering the classifier robust, i.e. we seek $//<![CDATA[ \begin{array}{l}f^*_{CROWN} \leq f^* := min_{x \in C} f(x)\end{array} //]]>$, which allows us to test robustness based on the implication $//<![CDATA[ \begin{array}{l}f^*_{CROWN} > 0 \implies f^* > 0\end{array} //]]>$. The core idea of CROWN is to propagate bounds backwards for the output neuron w.r.t. the current (hidden or input) neuron. For linear layers, this operation is straightforward as we can immediately apply their linear operation to the result of the previous layer to obtain the output of the neural network: Given $//<![CDATA[ \begin{array}{l}z^{(3)} = f(x)\end{array} //]]>$, we have $//<![CDATA[ \begin{array}{l}w^{(3) T} \hat{z}^{(2)} = f(x)\end{array} //]]>$.

Moving to $//<![CDATA[ \begin{array}{l}z^{(2)}\end{array} //]]>$, we would now need to propagate the bounds for a ReLU. However, non-linear activation functions do not permit straightforward bounds estimation in every case. As mentioned above, a stable ReLU permits this but its unstable case does not. To counteract this issue, we introduce linear relaxations in exchange for exact bounds. Defining such relaxations and ensuring they are still tight w.r.t. their original function is an active field of research and beyond the scope of this blog post. For ReLU we seek two linear functions that confine it within the lower and upper bound [6b]:

Naturally, these relaxations introduce some error and move us away from the original function described by the neural network. Based on these two linear functions, we build a diagonal matrix $//<![CDATA[ \begin{array}{l}D^{(2)}\end{array} //]]>$ that takes the lower or upper bound based on the worst-case representing the following approximation [6b]:

With matrix $//<![CDATA[ \begin{array}{l}D^{(2)}\end{array} //]]>$ we can then continue to propagate a linear lower bound as follows (details omitted for brevity, see [6b]):

The final lower bound approximation $//<![CDATA[ \begin{array}{l}f(x) \geq w^{(3) T} D^{(2)} W^{(2)} D^{(1)} W^{(1)}x + const.\end{array} //]]>$ can be converted to the form $//<![CDATA[ \begin{array}{l}\alpha^T_{CROWN} x + c_{CROWN} =: f_{CROWN}\end{array} //]]>$, where $//<![CDATA[ \begin{array}{l}\alpha_{CROWN}\end{array} //]]>$ and $//<![CDATA[ \begin{array}{l}c_{CROWN}\end{array} //]]>$ are functions of neural network weights that can be efficiently computed using a GPU [6b]. Taking the second formulation of the verification problem as mentioned above, we now have the following optimization problem:

With the relaxations we introduced, however, the lower bound may now be (too) loose. Thus, we could report a worst-case label flip even if it would not occur for the neural network under consideration. If the method reports a flipped label, we do not know if it is indeed adversarial or occurred due to the relaxation. Consequently, CROWN is sound but not complete.

Alpha and Beta

$//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN extends the CROWN algorithm by a heap of innovations in  $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$-CROWN and $//<![CDATA[ \begin{array}{l}\beta\end{array} //]]>$-CROWN, with this blog post focusing on the two most crucial ones:

In $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$-CROWN [16], an incomplete solver, the linear lower and upper bounds in ReLU relaxation gain an additional parameter $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$ to modify their slope. Using a method called linear relaxation-based perturbation analysis (LiPRA) [18], the lower and upper bound estimates of each layer are jointly optimized based on their gradients w.r.t. $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$ via projected gradient descent [16]. As this optimization can run on a GPU, it provides an efficient method to further tighten the bounds. The use of LiPRA in itself brings notable improvements as it provides a generalization of linear bounds estimation by operating on computational graphs [18] rather than a narrow set of models, thus supporting complex architectures like DenseNet [19] or Transformer [20]-based architectures.

$//<![CDATA[ \begin{array}{l}\beta\end{array} //]]>$-CROWN [17], a complete solver, implements the branch and bound technique [24, 25] for activation function relaxations to achieve completeness. We successively undo relaxations until we can either prove robustness or observe the network is truly not robust (see figure for explanation). This branching approach ultimately gives us completeness as we resolve the relaxations of unstable activation functions until the lower bound is sufficiently tight. If the tree is exhausted, i.e. no further ReLU can be split, and the lower bound is still less or equal to zero, we now know that the network is not robust.

VeriNet

The runner-up to $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN in the 2021 edition of VNN-COMP, VeriNet [2], is based on two verifiers called ReluVal [21] and Neurify [22] whose core algorithm we briefly explore:

Symbolic Interval Propagation

In contrast to CROWN, layer-wise bound propagation may also occur in a forward fashion, starting from the perturbation set $//<![CDATA[ \begin{array}{l}\mathcal{X}\end{array} //]]>$. In this manner, through simple arithmetic on the intervals, the lower and upper bounds are adjusted with each layer. Considering this approach, take a very simple neural network that computes $//<![CDATA[ \begin{array}{l}f(x) = 2x - x\end{array} //]]>$ with the input being restricted by $//<![CDATA[ \begin{array}{l}x \in [0, 1]\end{array} //]]>$. Simple interval arithmetics would yield the intervals $//<![CDATA[ \begin{array}{l}[0, 2]\end{array} //]]>$ and $//<![CDATA[ \begin{array}{l}[-1, 0]\end{array} //]]>$ for the first two neurons $//<![CDATA[ \begin{array}{l}2x\end{array} //]]>$ and $//<![CDATA[ \begin{array}{l}-x\end{array} //]]>$. The unifying addition would then yield the very broad interval $//<![CDATA[ \begin{array}{l}[-1, 2]\end{array} //]]>$ for $//<![CDATA[ \begin{array}{l}f(x)\end{array} //]]>$. ReluVal introduces symbolic interval propagation (SIP) [21] that allows us to achieve a much tighter bound. Instead of evaluating the symbols ($//<![CDATA[ \begin{array}{l}x\end{array} //]]>$) at each node, we keep track of them and operate on them directly, allowing us to capture the dependencies between nodes layer-by-layer [5]. Thus, we would obtain $//<![CDATA[ \begin{array}{l}[2x, 2x]\end{array} //]]>$ and $//<![CDATA[ \begin{array}{l}[-x, -x]\end{array} //]]>$, and finally the bounds $//<![CDATA[ \begin{array}{l}[2x - x, 2x - x] = [x, x] = [0, 1]\end{array} //]]>$, which match our expectations.

Compared to CROWN, the bound approximation in ReluVal for an unstable ReLU activation function is very rudimentary [5]: The lower bound is set to $//<![CDATA[ \begin{array}{l}0\end{array} //]]>$. For the upper bound, we consider the lower bound that we obtain after resolving the symbolic upper bound (e.g., for the symbolic bounds $//<![CDATA[ \begin{array}{l}[-(x+1), x] =: [u, l]\end{array} //]]>$ and input $//<![CDATA[ \begin{array}{l}[0, 1]\end{array} //]]>$, we obtain the symbolic bounds $//<![CDATA[ \begin{array}{l}\{ [-2, -1], [0, 1] \} =: \{ [\underbar{h}(l), \bar{h}(l)], [\underbar{h}(u), \bar{h}(u)] \}\end{array} //]]>$ with $//<![CDATA[ \begin{array}{l}\underbar{h}(u) = 0\end{array} //]]>$ representing the lower bound of the symbolic upper bound; a ReLU unit is considered unstable in ReluVal iff $//<![CDATA[ \begin{array}{l}\underbar{h}(l) < 0\end{array} //]]>$ and $//<![CDATA[ \begin{array}{l}\bar{h}(u) > 0\end{array} //]]>$ hold). If this bound ($//<![CDATA[ \begin{array}{l}\underbar{h}(u)\end{array} //]]>$) smaller than $//<![CDATA[ \begin{array}{l}0\end{array} //]]>$, its symbolic dependencies are discarded ($//<![CDATA[ \begin{array}{l}\underbar{h}(u) \gets 0\end{array} //]]>$), otherwise, they are kept and the upper bound is not modified. Neurify introduces symbolic linear relaxation (SLR) [22], which adds a more intricate ReLU relaxation. For unstable units, triangular relaxations are used for the lower and upper bounds [5] (example w.l.o.g. for the upper bound):

Compared to ReluVal, this formulation does not drop symbolic dependencies for the upper bound [5]. In [22], the authors claim that SLR can cut 59.64% more over-approximation error than SIP in ReluVal, highlighting the importance of well-chosen (tight) approximations.

Beyond this refinement, VeriNet implements several further optimizations to these two core methods, including a gradient-based search for counterexamples, a departure from calculating both, lower and upper, bounds (in favor of only the lower bound and an error value), and optimal relaxations for the sigmoid and tanh activation functions. As these go beyond scope of this blog post, we refer to [2] for further details.

Comparison to alpha,beta-CROWN

Having introduced two aspects of solvers, namely bounds propagation and methods to achieve completeness, we observed that $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN and ReluVal follow different approaches for either (VeriNet only in terms of bounds propagation). It is noteworthy, however, that activation function splitting, which is used to achieve completeness, has been introduced to Neurify and refined in VeriNet, suggesting it is a preferable method for bound refinement in high-performing solvers. Whether there is a benefit to using CROWN [23] or SIP [21]/SLR [22] is unclear as direct comparisons do not seem to exist. As solvers in the VNN-COMP 2021 [7] differ in a variety of aspects beyond their bound propagation method, the results of the competition cannot be used to draw comparisons between individual methodological differences.

While $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN did not win every benchmark category in the VNN-COMP 2021 [7], the results nonetheless suggest that it is a universally good choice. For smaller networks, however, e.g., VeriNet might be a better choice [7, 2]. Again, due to the comparison caveat of the competition, it is difficult to gauge why VeriNet is superior $//<![CDATA[ \begin{array}{l}\alpha,\beta\end{array} //]]>$-CROWN for such networks.

Note that we omitted a large part of these differences to limit the scope of this blog post. We point the interested reader to the solver papers [16, 17, 2, 22, 21], a broad, albeit slightly outdated survey of the field [5], and the VNN-COMP 2021 results [7] for an in-depth explanation of these.

Status Quo

Considering the development of this field since its early days in 2017, where only very simple feed-forward neural networks with ReLU activations could be verified [6a], nowadays complex Transformer architectures with a wide range of activation functions and layers (e.g. convolution, pooling, normalization) are supported [16, 17, 7]. Thanks to their increase in efficiency and the introduction of GPU-accelerated verification, large-scale neural networks (>100k neurons) can now be verified [6a] in reasonable time. Achieving efficient approximations with tighter bounds than SIP/SLR or the bounds given by $//<![CDATA[ \begin{array}{l}\alpha\end{array} //]]>$-CROWN, which would require even less refinement, offers further room for improvement in terms of bounds precision and solving speed.

In future competitions, it will be interesting to see if (groups of) solvers are becoming more similar due to methodological convergence (such as activation function splitting), or if the improvement of performance starts to saturate. These phenomena have been observed with Boolean satisfiability (SAT) solvers [31], a field that in its evolution may be compared to neural network verification methods. That field also suffers from limited comparability as well as limited understanding of the methods themselves, which has caused modern SAT solvers to be described as black boxes [32]. While the core concern in verification is to determine the robustness of black box neural networks, it might be worth asking if the tools to determine that should become black boxes themselves. The inability to properly compare the underlying methods of the two top-performing state-of-the-art solvers might indicate that this has already happened.

Nonetheless, their contribution to the adoption of neural networks in safety-critical domains cannot be understated. Provable robustness guarantees are a crucial step towards trust and have been identified as a key element for future regulation [33]. While the field of neural network verification still has to catch up to the eclipsing size of modern architectures that are ever-growing in their number of neurons, its past evolution indicates that this point may be reached in the near future.

References

[1] Henriksen, P., Hammernik, K., Rueckert, D. and Lomuscio, A., 2021. Bias Field Robustness Verification of Large Neural Image Classifiers. In In proceedings of the 32nd British Machine Vision Conference (BMVC21).

[2] Henriksen, P. and Lomuscio, A., 2020. Efficient neural network verification via adaptive refinement and adversarial search. In ECAI 2020 (pp. 2513-2520). IOS Press.

[3] OpenAI. 2017. "Attacking Machine Learning with Adversarial Examples." URL: https://openai.com/blog/adversarial-example-research/ Accessed on: June 23, 2022

[4] Papernot, N., P. McDaniel, S. Jha, M. Fredrikson, Z. B. Celik, and A. Swami. 2016. “The limitations of deep learning in adversarial settings”. In: IEEE European Symposium on Security and Privacy (EuroS&P).

[5] Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C. and Kochenderfer, M.J., 2021. Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization, 4 (3-4), pp.244-404.

[6a] Zhang, H., Xu, K., Wang, S. and Hsieh, C. 2022. Part I: Introduction to NN Verification. AAAI 2022 Tutorial on Neural Network Verification. https://neural-network-verification.com/ Accessed on: June 10, 2022

[6b] Zhang, H., Xu, K., Wang, S. and Hsieh, C. 2022. Part II: Algorithms for NN Verification. AAAI 2022 Tutorial on Neural Network Verification. https://neural-network-verification.com/ Accessed on: June 10, 2022

[7] Bak, S., Liu, C. and Johnson, T., 2021. The second international verification of neural networks competition (vnn-comp 2021): Summary and results. arXiv preprint arXiv:2109.00498.

[8] Choromanska, A., Henaff, M., Mathieu, M., Arous, G.B. and LeCun, Y., 2015, February. The loss surfaces of multilayer networks. In Artificial intelligence and statistics (pp. 192-204). PMLR.

[9] Bach, F., 2017. Breaking the curse of dimensionality with convex neural networks. The Journal of Machine Learning Research, 18(1), pp.629-681.

[10] Lomuscio, A. and Maganti, L., 2017. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351.

[11] Sun, Y., Huang, X., Kroening, D., Sharp, J., Hill, M. and Ashmore, R., 2018. Testing deep neural networks. arXiv preprint arXiv:1803.04792.

[12] Katz, G., Barrett, C., Dill, D.L., Julian, K. and Kochenderfer, M.J., 2017, July. Reluplex: An efficient SMT solver for verifying deep neural networks. In International conference on computer aided verification (pp. 97-117). Springer, Cham.

[13] Wong, E. and Kolter, Z., 2018, July. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning (pp. 5286-5295). PMLR.

[14] Raghunathan, A., Steinhardt, J. and Liang, P., 2018. Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344.

[15] Salman, H., Yang, G., Zhang, H., Hsieh, C.J. and Zhang, P., 2019. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems, 32.

[16] Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X. and Hsieh, C.J., 2020. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824.

[17] Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J. and Kolter, J.Z., 2021. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34, pp.29909-29921.

[18] Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.W., Huang, M., Kailkhura, B., Lin, X. and Hsieh, C.J., 2020. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33, pp.1129-1141.

[19] Huang, G., Liu, Z., Van Der Maaten, L. and Weinberger, K.Q., 2017. Densely connected convolutional networks. In Proceedings of the IEEE conference on computer vision and pattern recognition (pp. 4700-4708).

[20] Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, Ł. and Polosukhin, I., 2017. Attention is all you need. Advances in neural information processing systems, 30.

[21] Wang, S., Pei, K., Whitehouse, J., Yang, J. and Jana, S., 2018. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18) (pp. 1599-1614).

[22] Wang, S., Pei, K., Whitehouse, J., Yang, J. and Jana, S., 2018. Efficient formal safety analysis of neural networks. Advances in Neural Information Processing Systems, 31.

[23] Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J. and Daniel, L., 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31.

[24] Land, A.H. and Doig, A.G., 2010. An automatic method for solving discrete programming problems. In 50 Years of Integer Programming 1958-2008 (pp. 105-132). Springer, Berlin, Heidelberg.

[25] Morrison, D.R., Jacobson, S.H., Sauppe, J.J. and Sewell, E.C., 2016. Branch-and-bound algorithms: A survey of recent advances in searching, branching, and pruning. Discrete Optimization, 19, pp.79-102.

[26] Eykholt, K., Evtimov, I., Fernandes, E., Li, B., Rahmati, A., Xiao, C., Prakash, A., Kohno, T. and Song, D., 2018. Robust physical-world attacks on deep learning visual classification. In Proceedings of the IEEE conference on computer vision and pattern recognition (pp. 1625-1634).

[27] Finlayson, S.G., Bowers, J.D., Ito, J., Zittrain, J.L., Beam, A.L. and Kohane, I.S., 2019. Adversarial attacks on medical machine learning. Science, 363(6433), pp.1287-1289.

[28] Hirano, H., Minagi, A. and Takemoto, K., 2021. Universal adversarial attacks on deep neural networks for medical image classification. BMC medical imaging, 21(1), pp.1-13.

[29] Bortsova, G., González-Gonzalo, C., Wetstein, S.C., Dubost, F., Katramados, I., Hogeweg, L., Liefers, B., van Ginneken, B., Pluim, J.P., Veta, M. and Sánchez, C.I., 2021. Adversarial attack vulnerability of medical image analysis systems: Unexplored factors. Medical Image Analysis, 73, p.102141.

[30] Asgari Taghanaki, S., Das, A. and Hamarneh, G., 2018. Vulnerability analysis of chest X-ray image classification against adversarial attacks. In Understanding and interpreting machine learning in medical image computing applications (pp. 87-94). Springer, Cham.

[31] Oh, C., 2015, September. Between SAT and UNSAT: the fundamental difference in CDCL SAT. In International Conference on Theory and Applications of Satisfiability Testing (pp. 307-323). Springer, Cham.

[32] Soos, M., Kulkarni, R. and Meel, K.S., 2019, July. CrystalBall: Gazing in the Black Box of SAT Solving. In International Conference on Theory and Applications of Satisfiability Testing (pp. 371-387). Springer, Cham.

[33] Hamon, R., Junklewitz, H. and Sanchez Martin, J., Robustness and Explainability of Artificial Intelligence, EUR 30040 EN, Publications Office of the European Union, Luxembourg, 2020, ISBN 978-92-76-14660-5, doi:10.2760/57493, JRC119336.