Since machine learning components are now being considered for integration in safety-critical systems, safety stakeholders should be able to provide convincing arguments that the systems are safe for use in realistic deployment settings. In the case of vision-based systems, the use of tree ensembles calls for formal stability verification against a host of composite geometric perturbations that the system may encounter. Such perturbations are a combination of an afine transformation like rotation, scaling, or translation and a pixel-wise transformation like changes in lighting. However, existing verification approaches mostly target small norm-based perturbations, and do not account for composite geometric perturbations. In this work, we present a novel method to precisely define the desired stability regions for these types of perturbations. We propose a feature space modelling process that generates abstract intervals which can be passed to VoTE, an eficient formal verification engine that is specialised for tree ensembles. Our method is implemented as an extension to VoTE by defining a new property checker. The applicability of the method is demonstrated by verifying classifier stability and computing metrics associated with stability and correctness, i.e., robustness, fragility, vulnerability, and breakage, in two case studies. In both case studies, targeted data augmentation pre-processing steps were applied for robust model training. Our results show that even models trained with augmented data are unable to handle these types of perturbations, thereby emphasising the need for certified robust training for tree ensembles.
CEUR htp:/ceur-ws.org ISN1613-073 CEUR
Workshop Proceedings (CEUR-WS.org)
ML model could misread these signs and the efects
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 afect 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
∗Corresponding author.
could be disastrous. This calls for formal verification recent survey [
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.
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,
Pei et al. [13] and Mohapatra et al. [14] propose
verification frameworks called VERIVIS and
SemantifyNN 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
- A method to capture composite geometric perturba- enabling the use of any -norm based verification
tions based on real-world phenomena (like the com- method for robustness verification of deep neural
bined efects of axial rotations, scaling, or transla- networks. Balunović et al. [15] study the certification
tion together with changes in lighting) in the interval of neural networks against natural geometric
transfordomain through feature space modelling for vision- mations like rotation and scaling. They use sampling,
based systems. interpolation and Lipschitz optimisation to find the
- Realisation of the method, implemented as an exten- bounds for their certification process. The authors
sion to the Verifier of Tree Ensembles [
The rest of the paper is structured as follows. Section 2 discusses related works on the verification of tree ensembles against diferent 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.
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
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
tree structure is evaluated in a top-down manner, where
real-world phenomena (that preserve the semantics of
decision functions determine which path to take towards
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
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
in systems that use ML components. Our approach aims input from which the top-down evaluation started.
real-world perturbations like axial rotations in images
ensembles typically use univariate hard decision trees,
in the form of rotation-invariant networks [20] and
for example, scikit-learn [
Decision trees are known to sufer 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 [
Similar to Random Forests, Freidman [
using gradient descent (hence the name).
A gradient boosting machine ∶ → ℝ is an 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
rotation-equivariant networks [21]. In Scher et al. [
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 [
⋮ ⎧( 1,1, ..., 1, ) ∈ 1 ⎩( ,1 , ..., , ) ∈
In this paper, we only consider binary trees with
linear decision functions with one input variable,
which Irsoy et al. [
Decision trees and tree-ensemble models can be used as classifiers to categorize samples from an input domain then be defined as, bel 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 () =
VoTE [
(3) (4) into one or more classes and assign each sample a la- feature by a constant value, semantic perturbations take 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.
As opposed to perturbations that change the value of each
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
prob′
lem), geometric transformations (scaling, rotations) and
common image corruptions (fog, blurs) [
Geometric Perturbations are a class of semantic
perturbations [
Let ∶ ℝ 2 →
ℝ2 (in 2D) be an invertible afine 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( () , ())) 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 ] Scaling, parameterized by a scaling factor, ∈ ℝ, > −1 , sic idea is to pass these abstract intervals to the VoTE
(7)
In this section, we present a method to capture composite
geometric perturbations based on real-world phenomena
(like the combined efects of axial rotations and changes
in lighting) in the form of abstract intervals. The
baproperty checker [
Pixel-wise transformations are defined by the cumulative efects of brightness and contrast (i.e., simply changes in lighting) acting on a pixel , of an image the respective brightness and contrast parameters are where , ∈ ℝ . These transformations are defined by Balunovic et al. [15] and Mohapatra et al. [14] as,
′ , = min(1, max(0, (1 + ) ⋅ , + ))
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 efects of the transformation on this pixel at each step () = {
1, ..., } (9) such that is the outcome of the transformation at each step , 1 ≤ ≤ . In order to capture these pixel values in In our work, the pixel-wise transformations are parame- the interval domain, we use the abstraction function , terized by darkening and brightening ofsets, , ∈ ℝ, and the upper and lower bounds for the perturbations are specified as,
′ , = ( , − , , + )
(10)
Composite geometric perturbations based on real-world phenomena are a combination of one afine transformation (like rotation, translation or scaling) and a pixel-wise transformation (like changes in lighting). These perturbations are visually represented in figure 2 as,
() = {6, 2, 3, 1, 4} (()) = (1, 6) If = = 1, applying equation (13), (()) = ((1 − 1) − 5, (6 + 1) − 5)
( , ) = (−5, 2) 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).
( + , + ) = (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.
The abstraction process helps determine the upper and lower pixel-level perturbation margins in order to achieve eficient 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. Note that while Algorithm 1 contains axial rotations as the afine transformation, this can be easily adapted to the corresponding other afine transformations, i.e., scaling or translation computed by similar respective algorithms analogously.
In this section, we present the verification workflow that
shows the feature space modelling process incorporated
into the VoTE [
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)
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 [
Safety Engineers typically define requirements on software functions that are much richer than this property alone. and only if Let ∶ → ifcation where
be the classifier subject to veri (the image) is an n-array vector consisting of individual pixels, and is the output class or label. , ∈ ℝ are lower and upper perturbation margins ( < ) associated with an individual pixel
in the image. If is the number of pixels in the image, Δ = (( 1, 1), ..., ( ,
)) is a sequence containing tuples of pixel-level perturbation margins associated with the image. is an n-tuple of perturbations, with = ( sample and all possible variations of , the classifier 1, ..., ) and ⩽ ⩽ . If we consider a test is stable on that sample (denoted by ( , ) ) if () = ( ′) , where ′ = + (15) 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 efects of a geometric transformation and changes in lighting. These diferent versions of the base image can then be analyzed by the verification engine.
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 [
R = We incorporate these definitions into VoTE’s Property Checker which formally verifies classifier stability and automatically computes these metrics at the same time.
Recall that from the preliminaries, the VoTE property ( ∈ checker (VoTE-Pc) returns a pass if the property is satisifed. 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 ( , ( is_stable ← VoTE-Pc ( , ( , )) , )) (16) (17)
We apply our three afine 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 [
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. 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.
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.
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 Figure 5: Verification Workflow Fragment (EMNIST) pixels at 8bpp, encoded as a tuple of 784 pixels. The input regions surrounding each sample in the test set were Discussions defined using feature space modelling. The parameters for scaling were chosen as follows: Scaling Steps = 201, From the experimental results in Table 1 and Table 2, Scale Factor = ±10% which represents a 10% Zoom (in we note that the robustness of the learned models with respect to composite geometric perturbations is much verify these models within a fraction of a second for lower compared to the standard model accuracy (which most of the experiments. For larger models, while the is somewhat expected). In the first case study, gradi- verification time does increase, this issue is resolvable ent boosting machines performed slightly better than since due to the memory-eficient structure of the VoTE random forests in terms of robustness. Increasing the core algorithm, computations can always be parallelised number of trees improves accuracy but causes a drop in (not used in our experiments). robustness. This indicates that the models were overiftted and that adding compositely perturbed images to VoTE captures multiple inputs (precisely) in the the training set may improve robustness. The high num- interval domain, but whenever a prediction model bers for fragility indicated that while these samples were violates the stability property, the property checker identified correctly, the classifier was unable to make returns a counterexample which lies in the violating stable predictions on them in presence of these types of region. Figure 7 represents a few of the many counperturbations. We would also like to mention that the ver- terexamples discovered by VoTE during the verification ification process would require a domain expert, due to process (MNIST-Digits). Since the perturbations are the complex nature of these perturbations. For instance, almost indistinguishable by the naked eye, they are if you pick a large rotation range (or a large scaling or highlighted in pink. These counterexamples can be used translation range), there will be a significant number of for debugging or further analysis to repair or retrofit the images in the verification series that won’t resemble the models iteratively until provable stability is eventually ground truth label. In this case, the verification process achieved. For instance, counterexamples used for guided needs to be done in small ranges. model training can be embedded into a loss function to achieve better stability. 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 eficiently
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 diferent types of models and verification engines depending on the context. For future works, we plan on exploring diferent abstract domains which can be used to tightly capture these perturbations to increase the scalability of VoTE to