Introduction

Recent advancements in machine learning are now being considered for integration in safety-critical systems like medical equipment, critical infrastructure, and transport networks (autonomous vehicles, avionics, spaceflights) where software flaws could be detrimental to humans and the environment. While these systems are subject to strict regulations, a lack of evidence that the machine learning (ML) models deployed in these systems are safe for operation, can directly affect their trustworthiness.

Considering the inherently probabilistic nature of these models, standard industry practices like software testing are often unsuitable to provide any guarantees about operational safety. In this context, to help ensure trustworthiness, Artificial Intelligence (AI) systems can benefit from scrutiny through formal methods. Formal verification can be a tool to analyse the safety properties of software operating over a multi-dimensional space. Evidence based on formal verification can be used in a safety assurance case, which is a structured record of rea-soning with compelling and comprehensible arguments for a system being acceptably safe in a given context [25].

The formal methods community has recently been exploring the robustness properties of vision-based AI systems used in autonomous vehicles [5]. An important role of these vision-based systems is sending correct information about road signs to the vehicle's control system. However, the road signs encountered in the real world may appear different to that in the test set. Real-world phenomena like the banking of roads cause changes to the road surface topography in which the outer edges are raised at an angle above the inner edge to provide the necessary centripetal force to the vehicles for safe turns. This phenomenon, combined with rapid changes in lighting (time of day, light reflections from vehicles), and the fact that road signs have reflective elements, can produce different versions of the road signs. Along with being rotated, parts of these signs may appear lighter and darker depending on the light interactions (absorption, reflection, and so on). The same principle can be applied to other geometric transformations like scaling, in which the road sign appears zoomed out when the vehicle is at a distance, and translation, in which the road sign gradually moves out of the camera frame as it is approached by the vehicle. While the different versions of these road signs are correctly interpretable by humans, an ML model could misread these signs and the effects could be disastrous. This calls for formal verification of these models to ensure classifier stability in the presence of composite geometric perturbations that the system may encounter in real-world deployment settings.

In this paper, we present a method to precisely capture these perturbations as abstract intervals to verify tree-ensemble based classifiers against specified safety properties. Since our goal is to support safety arguments in assurance cases, the verifiability of the models is of paramount importance. The simple structure of the tree-based models makes them easier to systematically analyze in the formal verification process. However, larger models may still prove hard to verify due to the combinatorial explosion. We present a method where composite geometric perturbations are applied to input data and shown to prove a lack of stability even in the presence of data augmentation during training. This is demonstrated by applying our method to digit/character recognition problems. The contributions of this paper are as follows, -A method to capture composite geometric perturbations based on real-world phenomena (like the combined effects of axial rotations, scaling, or translation together with changes in lighting) in the interval domain through feature space modelling for visionbased systems.

-Realisation of the method, implemented as an extension to the Verifier of Tree Ensembles [3] (VoTE), a formal verification tool that uses abstract interpretation, along with the application of the method to two case studies commonly found in the literature.

The rest of the paper is structured as follows. Section 2 discusses related works on the verification of tree ensembles against different classes of perturbations. Section 3 presents the preliminaries on tree-ensembles, the VoTE toolsuite, and composite geometric perturbations. Section 4 presents our abstraction function and feature space modelling process along with the implementation in VoTE. Section 5 presents the application of the method to two case studies commonly found in the literature. Section 6 concludes the paper and summarizes the learnings.

Related Works

Recent machine learning advances are gradually finding their way into safety-critical systems. However, there is a lack of verification techniques to build formal arguments for operational safety in such systems. There has been extensive research on formal verification of 𝑙 𝑝 -norm bounded perturbations (mathematical distances that define the perturbations) in neural networks. A recent survey [11] gives a broad overview of the safety and trustworthiness of deep neural networks with a specific focus on topics like verification, testing, adversarial defence, and interpretability.

Engstrom et al. [12], show that state of the art neural network classifiers are vulnerable to natural classes of perturbations, especially simple translations and rotations for a significant fraction of their inputs. Another interesting observation they made is that data augmentation does not necessarily provide a significant boost to robustness, which we also confirm for tree ensembles in this paper.

Pei et al. [13] and Mohapatra et al. [14] propose verification frameworks called VERIVIS and Semantify-NN for evaluating the robustness of machine learning systems. The VERIVIS framework checks for violations of the parameter space (like the range of angles) when the inputs are subjected to semantic perturbations while the Semantify-NN framework converts semantic perturbations to 𝑙 𝑝 -norm based threat models thereby enabling the use of any 𝑙 𝑝 -norm based verification method for robustness verification of deep neural networks. Balunović et al. [15] study the certification of neural networks against natural geometric transformations like rotation and scaling. They use sampling, interpolation and Lipschitz optimisation to find the bounds for their certification process. The authors implement their certification framework in a system called DEEPG that uses a restricted Polyhedra with custom approximations for the operations used in several geometric transformations. Our approach, however, uses a feature space modelling process in conjunction with an abstraction function to get precise upper and lower bounds for the inputs as they are perturbed by real-world elements.

Wu et al. [16], study the certification of deep neural networks against real-world distribution shifts. They train a generative model to learn perturbations from the data to improve robustness precision. Yang et al. [17] mention that geometric image transformations that arise in the real world, such as scaling and rotation, have been shown to easily deceive deep neural networks. They propose a training formulation known as Certified Geometric Training (CGT) that improves the deterministic certified robustness of neural networks with respect to geometric transformations. Gowal et al. [19], use generative models to systematically transfer image attributes that are likely to be misclassified across image instances to achieve better robustness. They also mention that 𝑙 𝑝 -norm bounded perturbations do not necessarily cover plausible real-world variations that preserve the semantics of the input. We agree that composite geometric perturbations based on real-world phenomena (that preserve the semantics of the input) are outside the 𝑙 𝑝 -norm reach. Hence, we deploy a feature space modelling process for defining the multidimensional perturbation regions. Also, while using generative models can help with robust training, this in itself cannot be used for building up a safety case in systems that use ML components. Our approach aims to provide formal proof-based evidence to support safety assurances in these systems.

Outside formal verification and robust training, significant research has been done to tackle the issue of real-world perturbations like axial rotations in images in the form of rotation-invariant networks [20] and rotation-equivariant networks [21]. In Scher et al. [10], the authors formally define real-world perturbations and differentiate them between adversarial perturbations and distribution shifts. They model the perturbations around a point as a probability distribution and succeed in the estimation of robustness using Monte Carlo Sampling for low to medium dimensional data. While their method provides probabilistic guarantees, our approach aims to provide formal deterministic guarantees which can form the basis for reasoning about safety in safety-critical systems.

Preliminaries

In this section, we present the background knowledge on tree-based ensembles, semantic perturbations, interpolated/geometric and pixel-wise transformations, composite geometric perturbations based on real-world phenomena, and the toolsuite VoTE [3].

Decision Trees

Decision trees are employed as prediction models in machine learning and can be used in vision-based systems to solve image classification problems (among other applications). A decision tree model contains rules to predict the output class and implements a prediction function 𝑡 ∶ 𝑋 𝑛 → ℝ 𝑚 that maps disjoint sets of points 𝑋 𝑖 ⊂ 𝑋 𝑛 to a single output point 𝑦 𝑖 ∈ ℝ 𝑚 , i.e.,

𝑡(𝑥) = ⎧ ⎨ ⎩ (𝑦 1,1 , ..., 𝑦 1,𝑚 ) 𝑥 ∈ 𝑋 1 ⋮ (𝑦 𝑘,1 , ..., 𝑦 𝑘,𝑚 ) 𝑥 ∈ 𝑋 𝑘 (1)

Where 𝑘 is the number of disjoint sets and

𝑋 𝑛 = 𝑘 ⋃ 𝑖=1 𝑋 𝑖

The n-dimensional input domain 𝑋 𝑛 includes elements 𝑥 as tuples in which each input variable 𝑥 𝑖 captures some feature of interest of the system [3]. The tree structure is evaluated in a top-down manner, where decision functions determine which path to take towards the leaves. Each internal node in the decision tree is associated with a decision function that recursively splits the input space, thereby separating regions from each other. When a leaf is hit, the output 𝑦 ∈ ℝ 𝑚 associated with the leaf becomes the output associated with the input from which the top-down evaluation started.

In this paper, we only consider binary trees with linear decision functions with one input variable, which Irsoy et al. [4] call univariate hard decision trees. State-of-the-art implementations of tree-based ensembles typically use univariate hard decision trees, for example, scikit-learn [6] and CatBoost [7].

Random Forests

Decision trees are known to suffer from a phenomenon called overfitting in which the models are fitted so tightly to their training data that they memorize the data itself instead of learning the patterns associated with the data in order to make generalized predictions. To counteract these issues with decision trees concerning bias and variance, Breiman [1] proposes Random Forests.

A random forest 𝑓 ∶ 𝑋 𝑛 → ℝ 𝑚 is an ensemble of 𝐵 decision trees that produces outputs by averaging the values emitted by each individual tree. i.e.,

𝑓 (𝑥) = 1 𝐵 𝐵 ∑ 𝑏=1 𝑡 𝑏 (𝑥)(2)

Where 𝑡 𝑏 is the 𝑏 𝑡ℎ tree in the ensemble To reduce the correlation between trees, each tree is trained on overlapping random subsets of the training data (with replacement) using techniques like bagging or boosting.

Gradient Boosting Machines

Similar to Random Forests, Freidman [2] proposes gradient boosting machines that employ several decision trees to create a prediction function. Unlike Random Forests, these trees are trained in a sequential manner with each succeeding tree correcting the errors made by the predecessor tree. The errors are corrected using gradient descent (hence the name). Although conceptually different from random forests in a learning context, these two models have several features in common when performing predictions.

A gradient boosting machine 𝑓 ∶ 𝑋 𝑛 → ℝ 𝑚 is an ensemble of 𝐵 additive decision trees, i.e.,

𝑓 (𝑥) = 𝐵 ∑ 𝑏=1 𝑡 𝑏 (𝑥)(3)

Where 𝑡 𝑏 is the 𝑏 𝑡ℎ tree in the ensemble

Classifier

Decision trees and tree-ensemble models can be used as classifiers to categorize samples from an input domain into one or more classes and assign each sample a label unique to its class. In this paper, we only consider functions that map each point from an input domain to exactly one class. Let 𝑓 (𝑥) = (𝑦 1 , ..., 𝑦 𝑚 ) represent a model trained to predict the probability 𝑦 𝑖 associated with a class 𝑖 within disjoint regions in the input domain, where 𝑚 is the number of classes. A classifier 𝑓 𝑐 (𝑥) may then be defined as,

𝑓 𝑐 (𝑥) = 𝑎𝑟𝑔𝑚𝑎𝑥 𝑖 𝑦 𝑖 (4)

Verifier of Tree Ensembles

VoTE [3] (Verifier of Tree Ensembles) is a toolsuite for formally verifying that tree ensembles comply with specific properties that the user can define through implementing a property checker. The tool is based on abstract interpretation which yields equivalence classes in a tree ensemble, i.e. sets of points in the input domain that yield the same output tuple through an iterative refinement in the interval domain, such that the lowest level of abstract (the concrete) domain is equivalent to an exhaustive search down to all leaves in the model. This technique can be used to verify any property of interest defined within VoTE's property checker. For instance, in [26], VoTE was used to verify versatile application-specific properties of the aircraft collision avoidance system called ACAS Xu [18]. However, in this work, the property checker defined earlier (see Figure 1) checks for stability. The VoTE Core is instantiated from the ensemble subject to verification, 𝑓 ∶ 𝑋 𝑛 → 𝑅 𝑚 . It takes as input a hyperrectangle defining 𝑋 𝑛 , and the outcome of the formal verification is pass (when the tree ensemble satisfies the concerned property) and fail when it does not.

Semantic Perturbations

As opposed to perturbations that change the value of each feature by a constant value, semantic perturbations take an input image and 𝑝 parameters to perform a parameterized operation that perturbs the image while preserving its semantic information. Semantics-preserving perturbations can include object-level shifts (like changing the shape or size of an object in a color classification problem), geometric transformations (scaling, rotations) and common image corruptions (fog, blurs) [8]. Most of these perturbations cannot be naturally represented using the 𝑙 𝑝 -norm (‖ 𝑥 − 𝑥 ′ ‖ 𝑝 ≤ 𝜖) that most robustness verification methods are designed for. Using a large value of 𝜖 to try and capture these types of perturbations is usually not recommended in practice as the image quality degrades significantly [8]. Hence, we propose a feature space modelling process to precisely capture these multidimensional perturbations.

Geometric Perturbations

Geometric Perturbations are a class of semantic perturbations [8] that involve an affine transformation on each pixel's row and column indices, followed by an interpolation operation [17]. In this paper, we consider three types of affine transformations -rotations, scaling and translation.

Let 𝑇 𝜃 ∶ ℝ 2 → ℝ 2 (in 2D) be an invertible affine transformation (like rotation) parameterized by 𝜃 (like the angle of rotation). Let 𝜙 𝑥 (𝑗) and 𝜙 𝑦 (𝑖) be functions that transform 𝑖, 𝑗 pixel indices to 𝑥, 𝑦 co-ordinates with respect to the center of the image. However, as these transformed co-ordinates may not align exactly with the integer-valued pixel indices, bilinear interpolation ( 𝐼 ) is necessary. Yang et al. [17] define the general form of a geometric perturbation for an image 𝑋 as,

𝑋 ′ 𝑖,𝑗 = 𝐼 (𝑇 −1 𝜃 (𝜙 𝑥 (𝑗) , 𝜙 𝑦 (𝑖)))(5)

Where 𝑋 ′ is the perturbed image. For each geometric perturbation, they present the inverse transform function 𝑇 −1 𝜃 which is used to instantiate equation ( 5),

Rotation, parameterized by angle, 𝜃 ∈ [0, 2𝜋]

𝑇 −1 𝜃 (𝑥, 𝑦) = [ 𝑐𝑜𝑠𝜃 𝑠𝑖𝑛𝜃 −𝑠𝑖𝑛𝜃 𝑐𝑜𝑠𝜃 ] [ 𝑥 𝑦 ] = [ 𝑥𝑐𝑜𝑠𝜃 + 𝑦𝑠𝑖𝑛𝜃 −𝑥𝑠𝑖𝑛𝜃 + 𝑦𝑐𝑜𝑠𝜃 ](6)

Translation, parameterized by horizontal and vertical shifts ℎ ∈ ℝ, 𝑣 ∈ ℝ

𝑇 −1 ℎ,𝑣 (𝑥, 𝑦) = [ 𝑥 − ℎ 𝑦 − 𝑣 ](7)

Scaling, parameterized by a scaling factor, 𝜙 ∈ ℝ, 𝜙 > −1,

𝑇 −1 𝜙 (𝑥, 𝑦) = [ 1 1+𝜙 0 0 1 1+𝜙 ] [ 𝑥 𝑦 ] = [ 𝑥/(1 + 𝜙) 𝑦/(1 + 𝜙) ](8)

Pixel-wise Transformations

Pixel-wise transformations are defined by the cumulative effects of brightness and contrast (i.e., simply changes in lighting) acting on a pixel 𝑋 𝑖,𝑗 of an image 𝑋 where the respective brightness and contrast parameters are 𝑐, 𝑏 ∈ ℝ. These transformations are defined by Balunovic et al. [15] and Mohapatra et al. [14] as,

𝑋 ′ 𝑖,𝑗 = min(1, max(0, (1 + 𝑐) ⋅ 𝑋 𝑖,𝑗 + 𝑏))(9)

In our work, the pixel-wise transformations are parameterized by darkening and brightening offsets, 𝜁 𝐿 , 𝜁 𝐻 ∈ ℝ, and the upper and lower bounds for the perturbations are specified as,

𝑋 ′ 𝑖,𝑗 = (𝑋 𝑖,𝑗 − 𝜁 𝐿 , 𝑋 𝑖,𝑗 + 𝜁 𝐻 )(10)

Composite Geometric Perturbations

Composite geometric perturbations based on real-world phenomena are a combination of one affine transformation (like rotation, translation or scaling) and a pixel-wise transformation (like changes in lighting). These perturbations are visually represented in figure 2 as,

Proposed Method

In this section, we present a method to capture composite geometric perturbations based on real-world phenomena (like the combined effects of axial rotations and changes in lighting) in the form of abstract intervals. The basic idea is to pass these abstract intervals to the VoTE property checker [3] to verify stability and compute the extended stability metrics, which will be explained in this section.

Abstracting the Perturbations

For a particular input pixel 𝑥, if 𝑠 is the total number of geometric transformation (eg. rotation) steps for a given transformation, there exists a function, 𝜆(𝑥) that projects the effects of the transformation on this pixel at each step

𝜆(𝑥) = {𝑥 1 , ..., 𝑥 𝑠 }(11)

such that 𝑥 𝑖 is the outcome of the transformation at each step 𝑖, 1 ≤ 𝑖 ≤ 𝑠. In order to capture these pixel values in the interval domain, we use the abstraction function 𝛼, which is designed to compute an over-approximation of the problem, These pixel-level perturbation margins are then applied to the initial pixel value before the transformations to get the pixel-level perturbation bounds that are representative of composite geometric perturbations (like rotations and changes in lighting).

𝛼(𝜆(𝑥)) = (𝑚𝑖𝑛 𝜆(𝑥), 𝑚𝑎𝑥 𝜆(𝑥))(12)

(𝑝 + 𝜖 𝐿 , 𝑝 + 𝜖 𝐻 ) = (5 + (−5), 5 + 2) = (0, 7)

From this example, we see that the pixel 𝑥 can take on any value between (0, 7) during a composite geometric transformation.

Feature Space Modelling

The abstraction process helps determine the upper and lower pixel-level perturbation margins in order to achieve efficient computations during the verification process. Since VoTE operates based on abstracting each point with an interval in one dimension, when applying to a multidimensional space we need to extend the abstraction function through feature space modelling to simulate these perturbations for vision-based systems.

Verification Workflow

In this section, we present the verification workflow that shows the feature space modelling process incorporated into the VoTE [3] framework. We will use one of the case studies in section 5.1 to illustrate the flow in Figure 3. If we consider rotations between 0°and 10°, 𝐼 𝐿 (which is the image generated by applying 𝜖 𝐿 associated with all pixels in a particular image) and 𝐼 𝐻 (the corresponding image generated by applying 𝜖 𝐻 ) represent the first and last images in the verification process. We then ask the VoTE Property Checker to verify all the images in the transformed series. The property checker returns a pass when the classifier makes stable predictions on all the images in the transformed series. If the result of the verification process is fail, the property does not hold (the classifier is not stable). In this case, the VoTE property checker can be configured to return a counterexample that can help with further analysis. The illustration of the approach in more detail is described with use cases in section 5.

Classifier Correctness

The correctness of a classifier (𝑓 𝑐 ), with respect to an input 𝑥, denoted by 𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥) is proven when 𝑓 𝑐 predicts the correct label (𝑙) for an input sample (𝑥) according to a ground truth. This notion of correctness computed over a test set (𝑋 𝑡𝑒𝑠𝑡 ) can be used to quantify accuracy as

accuracy = |{ 𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 | 𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥)}| |𝑋 𝑡𝑒𝑠𝑡 | (14)

Safety Property: Classifier Stability

Accuracy on a test set is the most commonly used metric to evaluate a classification model. However, accuracy alone is not enough for convincing safety arguments in models that use machine learning. In this paper, we consider Stability, a property commonly used in related works. Robustness (and other metrics consistent with the literature) are generalised to a notion of classifier stability and correctness [9]. Note that compliance with stability and its associated metrics alone isn't generally enough to ensure system safety. Safety Engineers typically define requirements on software functions that are much richer than this property alone.

Let

The above expression can easily be extended over a test set (𝑋 𝑡𝑒𝑠𝑡 ). Note that 𝜔 when added to the base image (𝑥) produces a version of that base image that represents the combined effects of a geometric transformation and changes in lighting. These different versions of the base image can then be analyzed by the verification engine.

Extended Stability Metrics

Stability and Robustness are standard metrics commonly used in the literature on adversarial machine learning. They are generally used to quantify the security of classifiers at test time (for e.g., evasion attacks). Beyond stability, Ranzato and Zanella [9] define four additional metrics -robustness (R), fragility (F), vulnerability (V) and breakage (B) that combine classifier stability with prediction accuracy in the presence of input perturbations. We recall

R = |{ 𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 | 𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥) ∧ 𝐼 𝑠𝑆𝑡𝑎𝑏𝑙𝑒(𝑓 𝑐 , 𝑥) }| |𝑋 𝑡𝑒𝑠𝑡 | F = |{ 𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 | 𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥) ∧ ¬𝐼 𝑠𝑆𝑡𝑎𝑏𝑙𝑒(𝑓 𝑐 , 𝑥) }| |𝑋 𝑡𝑒𝑠𝑡 | V = |{ 𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 | ¬𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥) ∧ 𝐼 𝑠𝑆𝑡𝑎𝑏𝑙𝑒(𝑓 𝑐 , 𝑥) }| |𝑋 𝑡𝑒𝑠𝑡 | B = |{ 𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 | ¬𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥) ∧ ¬𝐼 𝑠𝑆𝑡𝑎𝑏𝑙𝑒(𝑓 𝑐 , 𝑥) }| |𝑋 𝑡𝑒𝑠𝑡 |

We incorporate these definitions into VoTE's Property Checker which formally verifies classifier stability and automatically computes these metrics at the same time.

VoTE Property Checker

Recall that from the preliminaries, the VoTE property checker (VoTE-Pc) returns a pass if the property is satisfied. For a tree-ensemble model (𝑓 𝑐 ), and a test sample 𝑥 (𝑥 ∈ 𝑋 𝑡𝑒𝑠𝑡 ), the following equations are used to verify stability and correctness, which can be extended to compute the metrics from the equations in section 4.6.

is_correct ← VoTE-Pc (𝑥 , 𝐼 𝑠𝐶𝑜𝑟𝑟𝑒𝑐𝑡(𝑓 𝑐 , 𝑥))(16

)

is_stable ← VoTE-Pc (𝑥 , 𝐼 𝑠𝑆𝑡𝑎𝑏𝑙𝑒(𝑓 𝑐 , 𝑥))(17)

Case Studies

We apply our three affine transformations combined with changes in lighting to two case studies. We verify stability and compute the extended metrics associated with classifier stability and correctness. Due to space restrictions, we will only show the outcomes of composite rotations in one study and composite scaling in the other. We use scikit-learn [6] to train random forests and CatBoost [7] to train gradient boosting machines. Experiments are conducted on a Windows 11 Machine running Ubuntu 20.04 in WSL Mode (Windows Subsystem for Linux). The machine comes equipped with an Intel Core i7-10875H CPU and 16 GB RAM.

Digit Recognition

The MNIST dataset [22] is a collection of hand-written digits commonly used to evaluate machine learning algorithms. The dataset contains 70,000 gray scale images with a resolution of 28x28 pixels at 8bpp, encoded as a tuple of 784 pixels. The input regions surrounding each sample in the test set were defined using feature space modelling (section 4.3). The parameters for rotation were chosen as follows: Rotation Range = 0 − 10°, Rotation Steps = 1001. For the changes in lighting, the parameters were chosen as: 𝜁 𝐿 = 2 (darkening) and 𝜁 𝐻 = 3 (brightening). To make this case study even more realistic, the training data was augmented (doubled to 120,000 training samples) by adding samples that were randomly rotated in the range of ±10°using Keras [24]. The verification process was carried out on 10,000 test samples. Figure 4 shows the construction of the first and last images in the verification series for a particular sample.

From this figure, it is visible that the two images, i.e., the first and the last resemble the ground truth, and the rest of the images in the series are similar in that sense.

Handwritten Character Recognition

In our next experiments, we use the EMNIST-Letters dataset, which is a variant of the EMNIST Dataset [23] that includes upper and lower case handwritten characters. This dataset contains 145,600 samples across 26 balanced classes. Each sample has a resolution of 28x28 pixels at 8bpp, encoded as a tuple of 784 pixels. The input regions surrounding each sample in the test set were defined using feature space modelling. The parameters for scaling were chosen as follows: Scaling Steps = 201, Scale Factor = ±10% which represents a 10% Zoom (in and out). For the changes in lighting, the parameters were chosen as: 𝜁 𝐿 = 2 (darkening) and 𝜁 𝐻 = 3 (brightening). To make this case study even more realistic, the training data was augmented (doubled to 249,600 training samples) by adding samples that were randomly scaled in the range of ±10% using Keras [24]. The verification process was carried out on 10,000 test samples. Table 2 lists random forests (RF) and gradient boosting machines (GB) included in the experiments with their maximum tree depth (d), number of trees (B), accuracy (A), the extended stability metrics -robustness (R), fragility (F), and breakage (B) along with the elapsed time (T) taken for verification (in seconds). Again, the column for vulnerability was omitted as it was zero in all experiments.

In regard to this case study, if we consider the EMNIST [23] letter a and scaling in the range of ±10 %, with 𝜁 𝐿 = 2 and 𝜁 𝐻 = 3, 𝐼 𝐿 and 𝐼 𝐻 represent the first and last images in the verification process. We then ask the VoTE Property Checker to verify all the images in the transformed series. Figure 5 shows a fragment of the verification flow.

Discussions

From the experimental results in Table 1 and Table 2, we note that the robustness of the learned models with respect to composite geometric perturbations is much lower compared to the standard model accuracy (which is somewhat expected). In the first case study, gradient boosting machines performed slightly better than random forests in terms of robustness. Increasing the number of trees improves accuracy but causes a drop in robustness. This indicates that the models were overfitted and that adding compositely perturbed images to the training set may improve robustness. The high numbers for fragility indicated that while these samples were identified correctly, the classifier was unable to make stable predictions on them in presence of these types of perturbations. We would also like to mention that the verification process would require a domain expert, due to the complex nature of these perturbations. For instance, if you pick a large rotation range (or a large scaling or translation range), there will be a significant number of images in the verification series that won't resemble the ground truth label. In this case, the verification process needs to be done in small ranges.

Figure 6: Comparing Verification Metrics

We repeated the experiments in the second case study by varying the scale factors as: ±2%, ±4%, ±6%, ±8%, ±10% for the largest Gradient Boosting Machine. In figure 6, we can see that as the scale factor is increased, the robustness of the model decreases and the verification runtime increases. This is expected as the number of perturbed pixels increases as the scale factor is increased.

Also, while the tree ensemble models chosen for the experiments could be considered trivial, we would like to point out that the verification problem was certainly non-trivial considering the composite nature of these perturbations, and the fact that the models were trained on high-dimensional data. What is positive in this context is the fact that performing such analyses in tractable time is at all possible given the enormous search space for these perturbations.

Considering the complexity of the verification problem, it is impressive that VoTE was able to efficiently verify these models within a fraction of a second for most of the experiments. For larger models, while the verification time does increase, this issue is resolvable since due to the memory-efficient structure of the VoTE core algorithm, computations can always be parallelised (not used in our experiments).

VoTE captures multiple inputs (precisely) in the interval domain, but whenever a prediction model violates the stability property, the property checker returns a counterexample which lies in the violating region. Figure 7 represents a few of the many counterexamples discovered by VoTE during the verification process (MNIST-Digits). Since the perturbations are almost indistinguishable by the naked eye, they are highlighted in pink. These counterexamples can be used for debugging or further analysis to repair or retrofit the models iteratively until provable stability is eventually achieved. For instance, counterexamples used for guided model training can be embedded into a loss function to achieve better stability.

Conclusions and Future Works

Applying formal verification to show that a system exhibits its intended behaviour can help increase the trustworthiness of the decisions made by intelligent systems. In this work, we show that tree-ensemble based models with comparatively good prediction accuracies perform spectacularly poorly when presented with samples containing composite geometric perturbations based on real-world phenomena.

Apart from the profound impacts on safety, these types of perturbations can also violate the security properties of classifiers which could be detrimental in safety-critical scenarios. To address this issue, the parameters in our method can be tweaked to simultaneously check for adversarial perturbations in addition to composite geometric perturbations. This represents a step towards safe and secure AI. Finally, our method can also be used with different types of models and verification engines depending on the context.

For future works, we plan on exploring different abstract domains which can be used to tightly capture these perturbations to increase the scalability of VoTE to even higher-dimensional inputs. We also plan to explore different tree selection strategies, i.e., a systematic analysis of the order in which the trees in the ensemble are analyzed in VoTE's abstraction-refinement pipeline to further enhance the efficiency of the verification process against the large nature of these perturbations.