# Verifiable Learning for Robust Tree Ensembles

Stefano Calzavara<EMAIL_ADDRESS>Università Ca’ Foscari
VeneziaItaly ,  Lorenzo Cazzaro<EMAIL_ADDRESS>0001-6479-2949
Università Ca’ Foscari VeneziaItaly ,  Giulio Ermanno Pibiri
<EMAIL_ADDRESS>Università Ca’ Foscari VeneziaItaly and  Nicola
Prezza<EMAIL_ADDRESS>0003-3553-4953 Università Ca’ Foscari
VeneziaItaly

###### Abstract.

Verifying the robustness of machine learning models against evasion attacks at
test time is an important research problem. Unfortunately, prior work
established that this problem is NP-hard for decision tree ensembles, hence
bound to be intractable for specific inputs. In this paper, we identify a
restricted class of decision tree ensembles, called _large-spread_ ensembles,
which admit a security verification algorithm running in polynomial time. We
then propose a new approach called _verifiable learning_ , which advocates the
training of such restricted model classes which are amenable for efficient
verification. We show the benefits of this idea by designing a new training
algorithm that automatically learns a large-spread decision tree ensemble from
labelled data, thus enabling its security verification in polynomial time.
Experimental results on publicly available datasets confirm that large-spread
ensembles trained using our algorithm can be verified in a matter of seconds,
using standard commercial hardware. Moreover, large-spread ensembles are more
robust than traditional ensembles against evasion attacks, while incurring in
just a relatively small loss of accuracy in the non-adversarial setting.

##  1\. Introduction

Machine learning (ML) is now phenomenally popular and found an incredible
number of applications. The more ML becomes pervasive and applied to critical
tasks, however, the more it becomes important to verify whether automatically
trained ML models satisfy desirable properties of interest. This is
particularly relevant in the security setting, where models trained using
traditional learning algorithms proved vulnerable to _evasion attacks_ , i.e.,
malicious perturbations of inputs designed to force mispredictions at test
time (BiggioCMNSLGR13, ; SzegedyZSBEGF13, ). For example, an attacker may
attempt to evade a ML model designed to detect malware by performing
semantics-preserving modifications of existing malicious software with the
goal of making it to be incorrectly classified as benign (DemetrioCBLAR21, ).

Unfortunately, verifying the security of ML models against evasion attacks is
a computationally hard problem, because verification must account for all the
possible malicious perturbations that the attacker may perform. In this work,
we are concerned about the security of _decision tree ensembles_
(BreimanFOS84, ), a well-known class of ML models particularly popular for
non-perceptual classification tasks, which already received significant
attention by the research community. Kantchelian et al. (KantchelianTJ16, )
first proved that the problem of verifying security against evasion attacks
for decision tree ensembles is NP-complete when malicious perturbations are
modeled by an arbitrary $L_{p}$-norm. In more recent work, Wang et al.
(WangZCBH20, ) further investigated the problem and observed that the existing
negative result largely generalizes to the apparently simpler case of decision
stump ensembles, i.e., ensembles including just trees of depth one. They thus
proposed _incomplete_ verification approaches for decision tree and decision
stump ensembles, which can formally prove the absence of evasion attacks, but
may incorrectly report evasion attacks also for secure inputs. This
conservative approach is efficient and provides formal security proofs,
however it is approximated and can draw a pessimistic picture of the actual
security guarantees provided by the ML model. Complete verification approaches
against specific attackers, e.g., modeled in terms of the $L_{\infty}$-norm,
have also been proposed (ChenZS0BH19, ; RanzatoZ20, ). They proved to be
reasonably efficient in practice for many cases, however they have to deal
with the NP-hardness of security verification, hence they are inherently bound
to fail in the general setting, especially when the size of the decision tree
ensembles increases. As a matter of fact, prior experimental evaluations show
that security verification does not always terminate within reasonable time
and memory bounds, leading to approximated estimates of the actual robustness
of the decision tree ensemble against evasion attacks (we also confirm this
limitation in our own experiments).

#### Contributions

In this paper we propose a novel approach to the security verification of
decision tree ensembles, which we call _verifiable learning_. Our key idea is
moving away from the intractable verification problems arising from arbitrary,
unconstrained models to rather focus on learning restricted model classes
designed to be easily verifiable in practice. In particular:

  1. (1)

We identify a restricted class of decision tree ensembles, called _large-
spread_ ensembles, which admit a security verification algorithm running in
polynomial time for evasion attacks modeled in terms of an arbitrary
$L_{p}$-norm, thus moving away from existing NP-hardness results (Section 3).

  2. (2)

We propose a new training algorithm that automatically learns a large-spread
decision tree ensemble amenable for efficient security verification. In short,
our algorithm first trains a traditional decision tree ensemble and then
prunes it to satisfy the proposed large-spread condition (Section 4).

  3. (3)

We implement our training algorithm and experimentally verify its
effectiveness on three public datasets. Our large-spread ensembles are more
robust than traditional ensembles against evasion attacks and admit a much
more efficient security verification, while incurring in just a relatively
small loss of accuracy in the non-adversarial setting (Section 5).

#### Code availability

To support reproducible research, we make all our code publicly available
online (https://tinyurl.com/54sw5v56).

##  2\. Background

In this section we review a few notions required to appreciate the rest of the
paper. To improve readability, we summarize the main notation used in this
paper in Table 1.

$\vec{x},\vec{z}$ | Instances drawn from the feature space $\mathcal{X}$
---|---
$x_{i}$ |  $i$-th component of the vector $\vec{x}$
$y$ | Class label drawn from the set of labels $\mathcal{Y}$
$d$ | Number of features of $\vec{x}$ (i.e., dimensionality of $\mathcal{X}$)
$t$ | Decision tree
$n$ | Number of nodes of a decision tree
$T$ | Tree ensemble
$N$ | Number of nodes of a tree ensemble
$m$ | Number of trees of a tree ensemble
$\vec{\delta}$ | Adversarial perturbation
$\Delta$ | Norm of an adversarial perturbation
$A_{p,k}$ | Attacker based on $L_{p}$-norm (max. perturbation $k$)
Table 1. Summary of notation. In the definitions of $n$, $N$, $m$ we assume
that the decision tree and tree ensemble we are predicating upon are clear
from the context.

###  2.1. Supervised Learning

Let $\mathcal{X}\subseteq\mathbb{R}^{d}$ be a $d$-dimensional vector space of
real-valued features. An _instance_ $\vec{x}\in\mathcal{X}$ is a
$d$-dimensional feature vector $\langle x_{1},x_{2},\ldots,x_{d}\rangle$
representing an object in the vector space $\mathcal{X}$. Each instance is
assigned a class label $y\in\mathcal{Y}$ by an unknown _target_ function
$f:\mathcal{X}\rightarrow\mathcal{Y}$. As common in the literature, we focus
on binary classification, i.e., we let $\mathcal{Y}=\\{+1,-1\\}$, because any
multi-class classification problem can be encoded in terms of multiple binary
classification problems.

Supervised learning algorithms automatically learn a _classifier_
$g:\mathcal{X}\rightarrow\mathcal{Y}$ from a _training set_ of correctly
labeled instances
$\mathcal{D}_{\textit{train}}=\\{(\vec{x}_{i},f(\vec{x}_{i}))\\}_{i}$, with
the goal of approximating the target function $f$ as accurately as possible
based on the empirical observations in the training set. The performance of
classifiers is normally estimated on a _test set_ of correctly labeled
instances
$\mathcal{D}_{\textit{test}}=\\{(\vec{z}_{i},f(\vec{z}_{i}))\\}_{i}$, disjoint
from the training set, yet drawn from the same data distribution. For example,
the standard _accuracy_ measure $a(g,\mathcal{D}_{\textit{test}})$ counts the
percentage of test instances where the classifier $g$ returns a correct
prediction.

###  2.2. Decision Trees and Tree Ensembles

In this paper, we focus on traditional _binary decision trees_ for
classification (BreimanFOS84, ). Decision trees can be inductively defined as
follows: a decision tree $t$ is either a leaf $\lambda(y)$ for some label
$y\in\mathcal{Y}$ or an internal node $\sigma(f,v,t_{l},t_{r})$, where
$f\in\\{1,\ldots,d\\}$ identifies a feature, $v\in\mathbb{R}$ is a threshold
for the feature, and $t_{l},t_{r}$ are decision trees (left and right child).
We just write $\sigma(f,v)$ to represent an internal node when $t_{l},t_{r}$
are unimportant. Decision trees are learned by initially putting all the
training set into the root of the tree and by recursively splitting leaves
(initially: the root) by identifying the threshold therein leading to the best
split of the training data, e.g., the one with the highest information gain,
thus transforming the split leaf into a new internal node.

At test time, the instance $\vec{x}$ traverses the tree $t$ until it reaches a
leaf $\lambda(y)$, which returns the prediction $y$, denoted by
$t(\vec{x})=y$. Specifically, for each traversed tree node
$\sigma(f,v,t_{l},t_{r})$, $\vec{x}$ falls into the left sub-tree $t_{l}$ if
$x_{f}\leq v$, and into the right sub-tree $t_{r}$ otherwise. Fig. 1
represents an example decision tree of depth 2, which assigns label $+1$ to
the instance $\langle 12,7\rangle$ and label $-1$ to the instance $\langle
8,6\rangle$.

To improve their performance, decision trees are often combined into an
_ensemble_ $T=\\{t_{1},\ldots,t_{m}\\}$, which aggregates individual tree
predictions, e.g., by performing majority voting. We write $T(\vec{x})$ for
the prediction of $T$ on $\vec{x}$ and we let $N$ stand for the number of
nodes of the ensemble $T$ when such ensemble is clear from the context. For
simplify, we focus on majority voting to aggregate individual tree
predictions, assuming that the number of trees $m$ is odd to avoid ties. While
ensembles trained using existing frameworks (like sklearn) may use more
sophisticated aggregation techniques, our focus on large-spread ensembles
trained using a custom algorithm gives us freedom on the choice of the
aggregation strategy and majority voting already proves effective in practice.
Notable ensemble methods include Random Forest (Breiman01, ) and Gradient
Boosting (KeMFWCMYL17, ).

$x_{1}\leq 10$$x_{2}\leq 5$$+1$$-1$$x_{2}\leq 8$$+1$$-1$ Figure 1. Example of
decision tree

###  2.3. Robustness

Classifiers deployed in adversarial settings may be susceptible to _evasion
attacks_ , i.e., malicious perturbations of test instances crafted to force
prediction errors (BiggioCMNSLGR13, ; SzegedyZSBEGF13, ). To capture this
problem, the _robustness_ measure has been introduced (MadryMSTV18, ). Below,
we follow the presentation in (RanzatoZ20, ).

An _attacker_ $A:\mathcal{X}\rightarrow 2^{\mathcal{X}}$ is modeled as a
function from instances to sets of instances, i.e., $A(\vec{x})$ represents
the set of all the adversarial manipulations of the instance $\vec{x}$,
corresponding to the possible evasion attack attempts against $\vec{x}$. The
_stability_ property requires that the classifier does not change its original
prediction on some input for all its possible adversarial manipulations.

###### Definition 2.1 (Stability).

The classifier $g$ is _stable_ on $\vec{x}$ for the attacker $A$ iff for all
$\vec{z}\in A(\vec{x})$ we have $g(\vec{z})=g(\vec{x})$.

Stability is certainly a desirable property for classifiers deployed in
adversarial settings; however, a classifier that always predicts the same
class for all the instances trivially satisfies stability for all the
attackers, but it is useless in practice because it lacks any predictive
power. Robustness improves upon stability by requiring the classifier to also
perform correct predictions.

###### Definition 2.2 (Robustness).

The classifier $g$ is _robust_ on $\vec{x}$ for the attacker $A$ iff
$g(\vec{x})=f(\vec{x})$ and $g$ is stable on $\vec{x}$ for $A$.

Based on the definition of robustness, for a given attacker $A$, we can define
the robustness measure $r_{A}(g,\mathcal{D}_{\textit{test}})$ by computing the
percentage of test instances where the classifier $g$ is robust.

In the following, we focus on attackers represented in terms of an arbitrary
$L_{p}$-norm, i.e., the attacker’s capabilities are defined by some
$p\in\mathbb{N}\cup\\{0,\infty\\}$ and the maximum perturbation $k$. For fixed
$p$ and $k$, we assume the attacker
$A_{p,k}(\vec{x})=\\{\vec{z}\in\mathcal{X}~{}|~{}||\vec{z}-\vec{x}||_{p}\leq
k\\}$.

##  3\. Efficient Robustness Verification for Tree Ensembles

In this section we first review existing results regarding the robustness
verification problem for single decision trees (Section 3.1). We then
generalize the result to $m$ trees by introducing _large-spread_ decision tree
ensembles (Section 3.2), which enable robustness verification in $O(N+m\log
m)$ time. This is a major improvement over traditional decision tree
ensembles, for which robustness verification is NP-complete (KantchelianTJ16,
).

###  3.1. Decision Trees

The robustness verification problem can be solved in $O(nd)$ time for a
decision tree with $n$ nodes when the attacker is expressed in terms of an
arbitrary $L_{p}$-norm (WangZCBH20, ). This generalizes a previous result for
the $L_{\infty}$-norm (ChenZS0BH19, ). The key idea of the algorithm is that
stability on the instance $\vec{x}$ can be verified by identifying all the
leaves that are reachable as the result of an evasion attack attempt
$\vec{z}\in A_{p,k}(\vec{x})$; hence, stability holds iff all such leaves
predict the same class. This set of leaves can be computed by means of a
simple tree traversal. Correspondingly, assuming that $\vec{x}$ has label $y$,
a decision tree $t$ is robust on $\vec{x}$ iff $t(\vec{x})=y$ and there does
not exist any reachable leaf assigning to $\vec{x}$ a label different from
$y$. The algorithm operates in two steps: (1) tree annotation and (2)
robustness verification.

####  3.1.1. Step 1 – Tree Annotation

The first step of the algorithm is a pre-processing operation – performed only
once – where each node of the decision tree is annotated with auxiliary
information for the second step. The annotations are hyper-rectangles that
symbolically represent the set of instances which may traverse the nodes upon
prediction. The algorithm first annotates the root with the $d$-dimensional
hyper-rectangle $(-\infty,+\infty]^{d}$, meaning that every instance will
traverse the root. Children are then annotated by means of a recursive tree
traversal: concretely, if the father node $\sigma(f,v,t_{1},t_{2})$ is
annotated with $(l_{1},r_{1}]\times\ldots\times(l_{d},r_{d}]$, then the
annotations of the roots of $t_{1}$ and $t_{2}$ are defined as
$(l_{1}^{1},r_{1}^{1}]\times\ldots\times(l_{d}^{1},r_{d}^{1}]$ and
$(l_{1}^{2},r_{1}^{2}]\times\ldots\times(l_{d}^{2},r_{d}^{2}]$ respectively,
where:

(1)
$(l_{i}^{1},r_{i}^{1}]=\begin{cases}(l_{i},r_{i}]\cap(-\infty,v]=(l_{i},\min\\{r_{i},v\\}]&\textnormal{if
}i=f\\\ (l_{i},r_{i}]&\textnormal{otherwise},\end{cases}$

and:

(2)
$(l_{i}^{2},r_{i}^{2}]=\begin{cases}(l_{i},r_{i}]\cap(v,+\infty)=(\max\\{l_{i},v\\},r_{i}]&\textnormal{if
}i=f\\\ (l_{i},r_{i}]&\textnormal{otherwise}.\end{cases}$

The annotation process terminates when all the nodes have been annotated. Note
that the complexity of this annotation step is $O(nd)$, because all $n$ nodes
are traversed and annotated with a hyper-rectangle of size $d$.

####  3.1.2. Step 2 – Robustness Verification

Given an annotated decision tree and an instance $\vec{x}$, it is possible to
identify the set of leaves which may be reached by $\vec{x}$ upon prediction
in presence of adversarial manipulations.

Let $H=(l_{1},r_{1}]\times\ldots\times(l_{d},r_{d}]$ be the hyper-rectangle
annotating a leaf $\lambda(y^{\prime})$. The minimal perturbation required to
push $\vec{x}$ into $\lambda(y^{\prime})$ is
$\textit{dist}(\vec{x},H)=\vec{\delta}\in\mathbb{R}^{d}$, where:111We write
$x_{i}-l_{i}+\varepsilon$ to stand for the minimum floating point number which
is greater than $x_{i}-l_{i}$. The original paper (ChenZS0BH19, ) uses
$l_{i}-x_{i}$ rather than $l_{i}-x_{i}+\varepsilon$, but this is incorrect
because $\vec{\delta}$ identifies the minimal perturbation such that
$\vec{x}+\vec{\delta}\in H$, however
$x_{i}+l_{i}-x_{i}=l_{i}\not\in(l_{i},r_{i}]$. We also assume here that $H$ is
not empty, i.e., there does not exist any $(l_{j},r_{j}]$ in $H^{\prime}$ such
that $l_{j}\geq r_{j}$.

(3) $\delta_{i}=\textit{dist}(\vec{x},H_{i})=\begin{cases}0&\textnormal{if
}x_{i}\in H_{i}=(l_{i},r_{i}]\\\ l_{i}-x_{i}+\varepsilon&\textnormal{if
}x_{i}\leq l_{i}\\\ r_{i}-x_{i}&\textnormal{if }x_{i}>r_{i}.\end{cases}$

Thus, given the instance $\vec{x}$ with label $y$, it is possible to compute
the set:

$\displaystyle D=\Big{\\{}||\vec{\delta}||_{p}\,|\,\exists\,$ $\displaystyle
H:\textit{dist}(\vec{x},H)=\vec{\delta}\wedge||\vec{\delta}||_{p}\leq k$ (4)
$\displaystyle\wedge\,$ $\displaystyle H\textnormal{ annotates a leaf
}\lambda(y^{\prime})\textnormal{ with }y^{\prime}\neq y\Big{\\}}.$

In other words, during the visit we find the leaves with a wrong class where
$\vec{x}$ might fall as the result of adversarial manipulations by the
attacker $A_{p,k}$ and we compute the norms $||\vec{\delta}||_{p}$ of the
minimal perturbations $\vec{\delta}$ to be applied to $\vec{x}$ to push it
there. Hence, the tree is robust against the attacker $A_{p,k}$ iff
$D=\varnothing$. This computation can be performed in $O(nd)$ time, since we
have $O(n)$ leaves and each vector $\vec{\delta}$ with its norm can be
computed in $\Theta(d)$ time.

###  3.2. Generalization to Tree Ensembles

$x_{1}\leq 10$$t_{1}$$-1$$+1$$x_{1}\leq 12$$t_{2}$$+1$$-1$$x_{1}\leq
17$$t_{3}$$+1$$-1$ Figure 2. Example of tree ensemble with three decision
trees.

The robustness verification problem is NP-complete for tree ensembles when the
attacker is expressed in terms of an arbitrary $L_{p}$-norm (KantchelianTJ16,
). Of course, this negative result predicates over _arbitrary_ tree ensembles,
but does not exclude the possibility that restricted classes of ensembles may
admit a more efficient robustness verification algorithm. In this section we
introduce the class of _large-spread_ tree ensembles, which rule out the key
source of complexity from the robustness verification problem and allow
robustness verification in $O(N+m\log m)$ time.

####  3.2.1. Key Intuitions

The key idea of the proposed large-spread condition allows one to verify the
robustness guarantees of the individual decision trees in the ensembles and
_compose their results_ to draw conclusions about the robustness of the whole
ensemble.

To understand why composing robustness verification results is unfeasible for
arbitrary ensembles, consider the ensemble $T$ in Fig. 2 and an instance
$\vec{x}$ with label $+1$ such that $x_{1}=11$. Consider the attacker
$A_{1,2}$ who can modify feature 1 of at most $\pm 2$, then for every
adversarial manipulation $\vec{z}\in A_{1,2}(\vec{x})$ we have
$z_{1}\in[9,13]$. We observe that the trees $t_{1}$ and $t_{2}$ are not robust
on $\vec{x}$, because there exists an adversarial manipulation that forces
them to predict the wrong class $-1$. However, the whole ensemble $T$ is
robust on $\vec{x}$, because $T(\vec{x})=+1$ and for every adversarial
manipulation $\vec{z}\in A_{1,2}(\vec{x})$ we have $T(\vec{z})=+1$, because
either $t_{1}$ or $t_{2}$ alone is affected by the attack, hence at least two
out of the three trees in the ensemble always perform the correct prediction.
The example is deliberately simple to show that attacks against two different
trees might be _incompatible_ , i.e., an attack working against one tree does
not necessarily work against the other tree and vice-versa. This implies that
the combination of multiple non-robust trees can lead to the creation of a
robust ensemble, as it is easy to observe in our example; note that
interactions across different trees can be complex and take place arbitrarily
down their decision paths.

The key intuition enabling our compositional reasoning is that interactions
among different trees are only possible when the thresholds therein are close
enough to each other. Indeed, in our example we showed that there exists an
instance $\vec{x}$ which can be successfully attacked in both $t_{1}$ and
$t_{2}$, yet no attack succeeds against both trees at the same time. The
reason why this happens is that the thresholds in the roots of the trees (10
and 12 respectively) are too close to each other when taking into account the
possible adversarial manipulations: an adversarial manipulation can corrupt
the original feature value 11 to produce an arbitrary value in the interval
$[9,13]$, which suffices to enable attacks in both $t_{1}$ and $t_{2}$.
However, none of the attacks against $t_{1}$ works against $t_{2}$ and vice-
versa. Conversely, it is not possible to find any instance $\vec{x}$ which can
be attacked in both $t_{2}$ and $t_{3}$, because for every adversarial
manipulation $\vec{z}\in A_{1,2}(\vec{x})$ we have $z_{1}\in[x_{1}-2,x_{1}+2]$
and the distance between the thresholds in the trees ($17-12=5>4$) is large
enough to ensure that the problem of incompatible attacks cannot exist,
because the feature 1 can be attacked just in one of the two trees. For
example, if $x_{1}=14$, then only $t_{2}$ can be attacked, while if $x_{1}=16$
only $t_{3}$ can be attacked; if $x_{1}=15$, instead, neither $t_{2}$ nor
$t_{3}$ can be attacked.

####  3.2.2. Large-Spread Ensembles

We formalize this intuition by defining the _$p$ -spread_ $\psi_{p}(T)$ of a
tree ensemble $T$ as the minimum distance between the thresholds of the same
feature across different trees, according to the $L_{p}$-norm. If
$\psi_{p}(T)>2k$, where $k$ is the maximum distance allowed for adversarial
manipulations, we say that $T$ is large-spread.

###### Definition 3.1 (Large-Spread Ensemble).

Given the ensemble $T=\\{t_{1},\dots,t_{m}\\}$, its $p$-spread $\psi_{p}(T)$
is:

$\psi_{p}(T)=\min\bigcup_{\begin{subarray}{c}1\leq f\leq d\\\ t,t^{\prime}\in
T,t\neq t^{\prime}\end{subarray}}\Big{\\{}||v-v^{\prime}||_{p}:\sigma(f,v)\in
t\wedge\sigma(f,v^{\prime})\in t^{\prime}\Big{\\}}.$

We say that $T$ is _large-spread_ for the attacker $A_{p,k}$ iff
$\psi_{p}(T)>2k$.

A large-spread ensemble $T$ allows one to compose attacks working against
individual trees to produce an attack against the ensemble as follows.
Assuming $\vec{z}_{i}=\vec{x}+\vec{\delta}_{i}$ is an attack against a tree
$t_{i}\in T$ and $\vec{z}_{j}=\vec{x}+\vec{\delta}_{j}$ is an attack against a
different tree $t_{j}\in T$, then the large-spread condition guarantees that
$\vec{\delta}_{i}$ and $\vec{\delta}_{j}$ target disjoint sets of features,
i.e., they are orthogonal ($\vec{\delta}_{i}\cdot\vec{\delta}_{j}=0$). Indeed,
each feature can be corrupted of $k$ at most, however the same feature can be
reused in different trees only if the corresponding thresholds are more than
$2k$ away, hence it is impossible for any feature value to traverse more than
one threshold as the result of an evasion attack (we formalize and prove this
result in Appendix A). The disjointness condition of attacks implies that
$\vec{z}=\vec{x}+\vec{\delta}_{i}+\vec{\delta}_{j}$ is an attack working
against both $t_{i}$ and $t_{j}$ (assuming
$||\vec{\delta}_{i}+\vec{\delta}_{j}||_{p}\leq k$), because $t_{i}(\vec{z})$
and $t_{j}(\vec{z})$ take the same prediction paths of $t_{i}(\vec{z}_{i})$
and $t_{j}(\vec{z}_{j})$ respectively, which are successful attacks against
the two trees. Note that this does not hold for arbitrary tree ensembles, like
the one in Fig. 2. Indeed, for that ensemble and an instance $\vec{x}$ such
that $x_{1}=11$ the attack against $t_{1}$ subtracts 2 from the feature 1 and
the attack against $t_{2}$ adds 2 to the feature 1, hence the sum of the two
attacks would leave the instance $\vec{x}$ unchanged.

####  3.2.3. Robustness Verification of Large-Spread Ensembles

This compositionality result is powerful, because it allows the efficient
robustness verification of large-spread ensembles. The intuition is that –
since the ensemble $T$ is large-spread – the minimal perturbations
$\\{\vec{\delta}_{i}\\}_{i}$ enabling attacks against the individual trees
$\\{t_{i}\\}_{i}$ can be summed up together to obtain a perturbation
$\vec{\delta}$ enabling an attack against the whole ensemble. More precisely,
let $T^{\prime}\subseteq T$ be the set of trees in $T$ which may suffer from a
successful attack, then:

  * •

If $|T^{\prime}|<\frac{m-1}{2}+1$, then the number of trees performing a wrong
prediction under attack is too low to identify a successful attack against the
whole ensemble.

  * •

If $|T^{\prime}|\geq\frac{m-1}{2}+1$, instead, we consider the
$\frac{m-1}{2}+1$ attacks $\\{\vec{\delta}_{i}\\}_{i}$ with the _smallest_
$L_{p}$-norm. An attack against $T$ is then possible iff
$||\vec{\delta}||_{p}\leq k$, where:

(5) $\vec{\delta}=\sum_{i=1}^{\frac{m-1}{2}+1}\vec{\delta}_{i}.$

However, note that the complexity of this algorithm is $O(Nd+m\log m)$ because
we annotate each of the $N$ nodes in the ensemble with a hyper-rectangle of
size $d$ and we compute the minimum perturbations along with their norms, as
explained in Section 3.1. Moreover, to find the perturbations with the
smallest norms, we have to sort the pairs
$(\vec{\delta_{i}},||\vec{\delta_{i}}||_{p})$ in non-decreasing order of
$L_{p}$-norm in $O(m\log m)$ time. We now show that the large-spread condition
enables a more efficient algorithm, running in $O(N+m\log m)$ time.

####  3.2.4. Optimization

If the minimal perturbations $\\{\vec{\delta}_{i}\\}_{i}$ are pairwise
orthogonal vectors, then the following facts hold.

###### Fact 1.

$||\sum_{i=1}^{q}\vec{\delta}_{i}||_{0}=\sum_{i=1}^{q}||\vec{\delta}_{i}||_{0}$,
if $\vec{\delta}_{i}\cdot\vec{\delta}_{j}=0$, $\forall(i,j)$.

###### Fact 2.

$||\sum_{i=1}^{q}\vec{\delta}_{i}||_{\infty}=\underset{1\leq i\leq
q}{\max}\\{||\vec{\delta}_{i}||_{\infty}\\}$, if
$\vec{\delta}_{i}\cdot\vec{\delta}_{j}=0$, $\forall(i,j)$.

###### Fact 3.

$||\sum_{i=1}^{q}\vec{\delta}_{i}||_{p}=(\sum_{i=1}^{q}||\vec{\delta}_{i}||_{p}^{p})^{1/p}$,
if $\vec{\delta}_{i}\cdot\vec{\delta}_{j}=0$, $\forall(i,j)$.

Note that the proof of Fact 1 and Fact 2 is immediate, hence we just prove
Fact 3 for the $L_{p}$-norm, with $p\in\mathbb{N}$.

###### Proof.

We show the equivalence for $q=2$; the case for $q>2$ is a simple
generalization. By definition of $L_{p}$-norm,
$||\vec{\delta}_{1}+\vec{\delta}_{2}||_{p}=(\sum_{i=1}^{d}|\delta_{1,i}+\delta_{2,i}|^{p})^{1/p}$.
The quantity $|\delta_{1,i}+\delta_{2,i}|^{p}$ is $\sum_{j=0}^{p}{p\choose
j}|\delta_{1,i}^{p-j}\cdot\delta_{2,i}^{j}|$ for the binomial theorem. Note
that the latter sum can be rewritten as
$|\delta_{1,i}|^{p}+|\delta_{2,i}|^{p}+\sum_{j=1}^{p-1}{p\choose
j}|\delta_{1,i}^{p-j}\cdot\delta_{2,i}^{j}|$, where $\sum_{j=1}^{p-1}{p\choose
j}|\delta_{1,i}^{p-j}\delta_{2,i}^{j}|=0$ because
$\delta_{1,i}\cdot\delta_{2,i}=0$ for any $1\leq i\leq d$. Therefore,
$||\vec{\delta}_{1}+\vec{\delta}_{2}||_{p}=(\sum_{i=1}^{d}|\delta_{1,i}|^{p}+\sum_{i=1}^{d}|\delta_{2,i}|^{p})^{1/p}=(||\vec{\delta}_{1}||_{p}^{p}+||\vec{\delta}_{2}||_{p}^{p})^{1/p}$.

The generalization to an arbitrary number of vectors $q>2$ involves a
multinomial theorem instead of a binomial theorem. ∎

We introduce the following operator to have a suitable way of referring to the
result of the three facts above:

(6)
$\bigoplus_{i=0}^{q}||\vec{\delta_{i}}||_{p}=\begin{cases}\sum_{i=1}^{q}||\vec{\delta}_{i}||_{0},&\textnormal{if
}p=0\\\ \underset{1\leq i\leq
q}{\max}\\{||\vec{\delta}_{i}||_{\infty}\\}&\textnormal{if }p=\infty\\\
(\sum_{i=1}^{q}||\vec{\delta}_{i}||_{p}^{p})^{1/p}&\textnormal{if
}p\in\mathbb{N}.\end{cases}$

Fact 1, 2, and 3 imply that we do not actually need to explicitly compute the
vector $\vec{\delta}$ in Eq. 5 if we just want its $L_{p}$-norm, which is
exactly our case because we just need to check whether such norm does not
exceed $k$. Since $\vec{\delta}$ results from the sum of pairwise orthogonal
vectors, we can use Eq. 6 to compute the norm directly from the norms of the
orthogonal vectors, i.e., the verification algorithm can operate on scalars
rather than vectors, thus reducing its complexity by a $d$ factor.

In light of these considerations, we now revisit the tree traversal from
Section 3.1 to show that we can compute for each leaf of the tree just a
scalar $\Delta=||\vec{\delta}||_{p}$, where
$\vec{\delta}=\textit{dist}(\vec{x},H)$ and $H$ is the hyper-rectangle which
would normally annotate the leaf. Similarly to the linear-time tree visit
described in (ChenZS0BH19, ) for the $L_{\infty}$-norm, the idea is to
maintain one _global_ hyper-rectangle during the visit instead of one hyper-
rectangle _per node_. Ultimately, this reduces the time complexity from
$O(nd)$ to the optimal $O(n)$, since the hyper-rectangle is not copied from
parent to children. The optimized variant of the algorithm is described in the
Reachable procedure of Algorithm 1. This $O(n)$-time algorithm for arbitrary
$L_{p}$-norm is, in fact, a combination of the $O(n)$-time algorithm of
(ChenZS0BH19, ) (which works only for the $L_{\infty}$-norm) with the
generalization to any $L_{p}$-norm of (WangZCBH20, ) (which however runs in
$O(nd)$ time).

Algorithm 1 Optimized robustness verification algorithm for decision trees.

1:function Reachable($t,p,k,\vec{x},y$)

2: $H\leftarrow(-\infty,+\infty]^{d}$

3: $\Delta\leftarrow 0$

4: return $\textsc{Traverse}(t,p,k,\vec{x},y,H,\Delta)$

5:

6:function Traverse($t,p,k,\vec{x},y,H,\Delta$)

7: if $t=\lambda(y^{\prime})$ then

8: if $\Delta\leq k$ and $y^{\prime}\neq y$ then

9: return $\\{\Delta\\}$

10: return $\varnothing$

11: Let $t=\sigma(f,v,t_{l},t_{r})$

12: $D\leftarrow\varnothing$

13: $H_{f}^{*}\leftarrow H_{f}$ $\triangleright$ copy

14: $\Delta^{*}\leftarrow\Delta$ $\triangleright$ copy

15: $\delta_{f}=\textit{dist}(\vec{x},H_{f})$ $\triangleright$ Eq. 3

16: $H_{f}\leftarrow H_{f}^{*}\cap(-\infty,v]$ $\triangleright$ Eq. 1

17: $\delta^{\prime}_{f}=\textit{dist}(\vec{x},H_{f})$ $\triangleright$ Eq. 3

18: $\Delta\leftarrow\textsc{Update-
Norm}(p,\Delta,\delta_{f},\delta^{\prime}_{f})$ $\triangleright$ Eq. 7

19: $D\leftarrow D\cup\textsc{Traverse}(t_{l},p,k,\vec{x},y,H,\Delta)$

20: $H_{f}\leftarrow H_{f}^{*}\cap(v,+\infty)$ $\triangleright$ Eq. 2

21: $\delta^{\prime}_{f}=\textit{dist}(\vec{x},H_{f})$ $\triangleright$ Eq. 3

22: $\Delta\leftarrow\textsc{Update-
Norm}(p,\Delta,\delta_{f},\delta^{\prime}_{f})$ $\triangleright$ Eq. 7

23: $D\leftarrow D\cup\textsc{Traverse}(t_{r},p,k,\vec{x},y,H,\Delta)$

24: $H_{f}\leftarrow H_{f}^{*}$ $\triangleright$ Restore hyper-rectangle

25: $\Delta\leftarrow\Delta^{*}$ $\triangleright$ Restore norm

26: return $D$

27:

28:function Robust-Tree($t,p,k,\vec{x},y$)

29: if $t(\vec{x})=y$ then

30: $D\leftarrow\textsc{Reachable}(t,p,k,\vec{x},y)$

31: if $D=\varnothing$ then

32: return True

33: return False

We implement $H$ as an initially-empty map (e.g., using a hash table):
$H_{i}\in\mathbb{R}^{2}$ is the entry associated to the $i$-th feature. If the
map does not contain an entry for the $i$-th feature, then it is implicitly
assumed $H_{i}=(-\infty,+\infty]$. Let
$H=(l_{1},r_{1}]\times\ldots\times(l_{d},r_{d}]$ be the state of the hyper-
rectangle when visiting node $t=\sigma(f,v,t_{1},t_{2})$. When moving to a
child $t_{j}$ of $t$, with $j\in\\{1,2\\}$, note that the distance vector
$\vec{\delta}$ changes only in its $f$-th component $\delta_{f}$, since only
the $f$-th component $(l_{f},r_{f}]$ of the hyper-rectangle $H$ changes. We
can therefore update $\Delta$ efficiently as follows. Let $\Delta^{\prime}$
and
$H^{\prime}=(l^{\prime}_{1},r^{\prime}_{1}]\times\ldots\times(l^{\prime}_{d},r^{\prime}_{d}]$
be the perturbation distance and hyper-rectangle associated to any of $t$’s
children. Let $\delta^{\prime}_{f}$ be the quantity defined in Eq. 3. We
extend the linear-time algorithm of (ChenZS0BH19, ) to an arbitrary
$L_{p}$-norm by noting that the following is implied by Facts 1, 2, and 3:

(7) $\small\textsc{Update-
Norm}(p,\Delta,\delta_{f},\delta^{\prime}_{f})=\begin{cases}\Delta-||\delta_{f}||_{0}+||\delta^{\prime}_{f}||_{0}&\textnormal{if
}p=0\\\ \max\big{(}\Delta,|\delta^{\prime}_{f}|\big{)}&\textnormal{if
}p=\infty\\\
\big{(}\Delta^{p}-|\delta_{f}|^{p}+|\delta^{\prime}_{f}|^{p}\big{)}^{1/p}&\textnormal{if
}p\in\mathbb{N}.\end{cases}$

By definition, it is clear that Update-Norm is computed in $O(1)$ time. The
correctness of the case $p=\infty$ (as also discussed in (ChenZS0BH19, ))
follows from the fact that it must be $|\delta^{\prime}_{f}|\geq|\delta_{f}|$,
since $(l^{\prime}_{i},r^{\prime}_{i}]\subseteq(l_{i},r_{i}]$. In conclusion,
we spend $O(1)$ time per node and the time complexity of the whole visit is
therefore $O(n)$. Hence, the set $D$ in Eq. 3.1.2 is computed in $O(n)$ time
rather than $O(nd)$ time as we previously described in Section 3.1. This also
lowers the time complexity of the robustness verification for decision trees
shown in the Robust procedure of Algorithm 1 to just $O(n)$ rather than
$O(nd)$. Since robustness verification for large-spread ensembles builds on
the verification algorithm of the individual trees therein, this optimization
reduces the complexity of our final algorithm.

####  3.2.5. Final Algorithm

We conclude this section with Algorithm 2, our robustness verification
algorithm for large-spread ensembles, whose correctness is stated in the
following theorem and formally proved in Appendix A. It follows the
description in Section 3.2.3, revised to operate with norms (scalars) rather
than vectors.

###### Theorem 3.2.

Let $\vec{x}$ be an instance with label $y$. A tree ensemble $T$ such that
$\psi_{p}(T)>2k$ is robust on $\vec{x}$ against the attacker $A_{p,k}$ iff
$\textsc{Robust}(T,p,k,\vec{x},y)$ returns True.

Observe that the complexity of Algorithm 2 is $O(N+m\log m)$, where $N$ and
$m$ are, respectively, the total number of nodes and trees in the ensemble.
Verifying the robustness of the $m$ individual trees in the ensemble and
updating vector $\vec{\Delta}$ takes $O(N)$ time thanks to the linear-time
Algorithm 1. Afterwards, the algorithm sorts $\vec{\Delta}$ in $O(m\log m)$
time and computes the minimum norm required to attack at least
$\frac{m-1}{2}+1$ trees in $O(m)$ time.

Algorithm 2 Robustness verification algorithm for large-spread tree ensembles.

1:function Robust($T,p,k,\vec{x},y$)

2: if $T(\vec{x})=y$ then

3: return $\textsc{Stable}(T,p,k,\vec{x},y)$

4: return False

5:

6:function Stable($T,p,k,\vec{x},y$)

7: $\textit{num\\_unstable\\_trees}\leftarrow 0$

8: $\vec{\Delta}\leftarrow[+\infty,\ldots,+\infty]$ $\triangleright$ Vector of
size $m$

9: for $i\leftarrow 1$ to $m$ do

10: $D\leftarrow\textsc{Reachable}(t_{i},p,k,\vec{x},y)$

11: if $D\neq\varnothing$ then

12: $\Delta_{i}\leftarrow\min D$

13:
$\textit{num\\_unstable\\_trees}\leftarrow\textit{num\\_unstable\\_trees}+1$

14: if $\textit{num\\_unstable\\_trees}\geq(m-1)/2+1$ then

15: Sort $\vec{\Delta}$ in non-decreasing order

16: $\Delta=\bigoplus_{i=0}^{(m-1)/2+1}\Delta_{i}$ $\triangleright$ Eq. 6

17: if $\Delta\leq k$ then

18: return False

19: return True

##  4\. Training Large-Spread Ensembles

We have described an efficient robustness verification algorithm for large-
spread ensembles in Section 3. However, traditional decision tree ensembles
trained using, e.g., sklearn, do not necessarily enjoy the large-spread
condition. Here we discuss possible ideas for training algorithms designed to
enforce the large-spread condition and we present a specific solution from the
design space.

###  4.1. Design Space

While reasoning about the design of a training algorithm for large-spread
ensembles, we considered different approaches falling in three broad classes:

  1. (1)

_Custom ensemble learning algorithms_. Develop new learning algorithms in the
spirit of Random Forest (Breiman01, ) or Gradient Boosting (KeMFWCMYL17, ),
designed to constrain the ensemble shape so as to satisfy the large-spread
condition. For example, one might train each tree while taking into account
the thresholds already present in the previously trained trees, to then remove
the training data which might lead to learning thresholds which are too close
to the existing ones. Indeed, recall that thresholds are learned from the
training data, hence all the possible thresholds are known a priori.

  2. (2)

_Training set partitioning_. Pre-compute a partition of the training data so
that each decision tree in the ensemble is trained over highly separated
instances, thus leading to an ensemble of trees satisfying the large-spread
condition. The simplest instantiation of this idea would be partitioning the
set of features and train different trees over different subsets of features,
so that the large-spread condition is trivially satisfied, but more fine-
grained strategies based on instance partitioning would also be feasible.

  3. (3)

_Pruning techniques_. Train a standard decision tree ensemble, e.g., using the
Random Forest algorithm, and prune it so as to keep only trees satisfying the
large-spread condition. A variant of this technique might perform different
types of mutations of the available trees to improve the effectiveness of
pruning.

Although we consider all these routes to be viable and worth investigating, in
this work we decide to prioritize the third class of solutions. Compared to
the first class, pruning leads to a range of simple and intuitive solutions,
which take advantage of state-of-the-art implementations of existing training
algorithms, e.g., those available in sklearn. This simplifies the deployment
of an efficient and robust implementation. Moreover, pruning does not
necessarily require a massive amount of training data and features, as needed
for an effective training set partitioning (second class). In the last part of
this section, we also discuss how to leverage feature partitioning to improve
the effectiveness of our pruning-based learning algorithm in those settings
where a high number of features is available (_hierarchical training_).

###  4.2. Proposed Training Algorithm

Here we present our training algorithm. We motivate its design, describe how
it works and discuss a few relevant aspects of the proposed solution.

####  4.2.1. Preliminaries

Our problem of interest can be formulated as follows: given a decision tree
ensemble $T$ and a size $0<s\leq|T|$, determine whether there exists an
ensemble $T^{\prime}\subseteq T$ such that $T^{\prime}$ is large-spread and
$|T^{\prime}|=s$. We refer to this problem as the _large-spread subset_
problem for decision tree ensembles. Unfortunately, we can prove that this
problem is NP-hard. The proof is provided in Appendix B.

###### Theorem 4.1.

The large-spread subset problem is NP-hard.

The theorem implies that it is computationally hard to train large-spread
ensembles by pruning when the desired number of trees therein is enforced a
priori, which is normally the case because the number of trees is a standard
hyper-parameter of ensemble methods. One might argue that this negative result
is not a showstopper, because training is performed just once and one might
devise efficient heuristic approaches to approximate the large-spread subset
problem, however preliminary experiments on public datasets suggest that any
training approach which is _purely_ based on pruning is likely ineffective in
practice. Indeed, we empirically observed on our datasets that traditional
random forests trained using sklearn are not directly amenable for pruning,
because any two trees in the ensemble already violate the large-spread
condition when joined into an ensemble of size two. Our understanding of this
phenomenon is that there exist some important features which are pervasively
reused across different trees, which often learn the same thresholds, thus
making the identification of a large-spread ensemble unfeasible. Our training
algorithm thus integrates a greedy heuristic approach to pruning with a
mutation operation, which perturbs thresholds so as to actively enforce the
large-spread condition even when it would not be possible by pruning alone.

####  4.2.2. Training Algorithm

The proposed training algorithm takes as input a training set
$\mathcal{D}_{\textit{train}}$, a number of trees $m$, a norm $p$, a maximum
perturbation $k$ and a maximum number of iterations $MAX\\_ITER$ (for
readability, we omit additional hyper-parameters such as maximum tree depth).
From a high level point of view, the algorithm operates by training a standard
random forest $T$ including $2m$ trees to then select a set of $m$ trees
constituting a large-spread ensemble $T^{*}$. This is done by a combination of
pruning and mutation of the trees in $T$. After picking a random tree of $T$
to begin with, the algorithm iteratively tries to identify the other $m-1$
trees by means of a greedy approach. The candidate tree $t$ to be inserted in
$T^{*}$ is always the tree in $T$ minimizing the number of _feature overlaps_
with $T^{*}$, i.e., the number of features violating the large-spread
condition in $T^{*}\cup\\{t\\}$. If the number of feature overlaps is greater
than zero, the ensemble is fixed to enforce the large-spread condition by
iteratively removing the overlaps. In particular, let $\sigma(f,v)$ and
$\sigma(f,v^{\prime})$ be two nodes from different trees such that
$||v-v^{\prime}||_{p}\leq 2k$. We sample a perturbation $\delta\in[k,2k]$, we
subtract $\delta$ from $\min(v,v^{\prime})$ and we sum $\delta$ to
$\max(v,v^{\prime})$. The original overlap is therefore fixed because the new
thresholds are at least $2k$ away from each other. Since this change might
introduce new overlaps, we then iterate through the ensemble until all the
overlaps have been fixed (i.e., the ensemble is large-spread) or a maximum
number of iterations has been reached. If all the overlaps of
$T^{*}\cup\\{t\\}$ have been fixed, i.e., the resulting tree-based ensemble is
large-spread, then the extended large-spread ensemble becomes the new large-
spread ensemble $T^{*}$, otherwise $T^{*}$ is not extended and the tree $t$ is
discarded. Then the algorithm tries to extend $T^{*}$ with another tree in
$T$, unless $T^{*}$ has reached the desired number of trees or all the trees
in $T$ have been selected for extending the large-spread ensemble. The
pseudocode of the training algorithm is presented in Algorithm 3.

Algorithm 3 Training algorithm for large-spread ensembles

1:function TrainLargeSpread($\mathcal{D}_{\textit{train}},m,p,k,MAX\\_ITER$)

2: $T\leftarrow\textsc{TrainRandomForest}(\mathcal{D}_{\textit{train}},2m)$

3: $t\leftarrow\textsc{SampleTree}(T)$ $\triangleright$ Choose a random tree
from $T$

4: $T\leftarrow T\setminus\\{t\\}$

5: $T^{*}\leftarrow\\{t\\}$

6: $i\leftarrow 1$

7: while $i<2m$ and $|T^{*}|<m$ do

8: $i\leftarrow i+1$

9: $t\leftarrow\textsc{GetBestTree}(T,T^{*},p,k)$

10: $T\leftarrow T\setminus\\{t\\}$

11: $\overline{T^{*}}\leftarrow T^{*}\cup\\{t\\}$

12: $\overline{T^{*}}\leftarrow\textsc{FixForest}(\overline{T^{*}},p,k)$

13: if $\overline{T^{*}}\neq\bot$ then $\triangleright$ FixForest succeded

14: $T^{*}\leftarrow\overline{T^{*}}$

15: if $|T^{*}|=m$ then $\triangleright$ TrainLargeSpread succeded

16: return $T^{*}$

17: else

18: return $\bot$

19:

20:function GetBestTree($T,T^{*},p,k$)

21: $t^{*}\leftarrow\bot$

22: $min\\_f\\_overlaps\leftarrow+\infty$

23: for $t\in T$ do

24: $overlaps\leftarrow\\{\sigma(f,v)\in
t~{}|~{}\exists\sigma(f,v^{\prime})\in T^{*}:||v-v^{\prime}||_{p}\leq 2k\\}$

25: $f\\_ov\leftarrow|\\{f~{}|~{}\exists\sigma(f,v)\in overlaps\\}|$

26: if $f\\_ov<min\\_f\\_overlaps$ then

27: $min\\_f\\_overlaps\leftarrow f\\_ov$

28: $t^{*}\leftarrow t$

29: return $t^{*}$

30:

31:function FixForest($T^{*},p,k,MAX\\_ITER$)

32: $iter\leftarrow 0$

33: while $T^{*}$ is not large-spread and $iter<MAX\\_ITER$ do

34: $iter\leftarrow iter+1$

35: for $t,t^{\prime}\in T^{*},\ \sigma(f,v)\in t,\
\sigma(f^{\prime},v^{\prime})\in t^{\prime}$ do

36: if $f=f^{\prime}$ and $||v-v^{\prime}||_{p}\leq 2k$ then

37: $\delta\leftarrow\textsc{Random}(k,2k)$ $\triangleright$ Pick a float in
$[k,2k]$

38: if $v\leq v^{\prime}$ then

39: $\sigma(f,v)\leftarrow\sigma(f,v-\delta)$

40:
$\sigma(f^{\prime},v^{\prime})\leftarrow\sigma(f^{\prime},v^{\prime}+\delta)$

41: else

42: $\sigma(f,v)\leftarrow\sigma(f,v+\delta)$

43:
$\sigma(f^{\prime},v^{\prime})\leftarrow\sigma(f^{\prime},v^{\prime}-\delta)$

44: if $T^{*}$ is not large-spread then

45: return $\bot$

46: return $T^{*}$

####  4.2.3. Complexity

In our analysis we assume that each of the $m$ trees in the trained forest has
at most $n$ nodes. TrainLargeSpread calls $O(m)$ times GetBestTree and
FixForest. The former function GetBestTree iterates at most $|T|\in O(m)$
times ($t\in T$, line 23) the construction of set _overlaps_. A naive way of
building this set is to iterate over all nodes of $t$ (at most $n$ nodes) and
compare their thresholds with all the thresholds appearing in the nodes of
$T^{*}$ (at most $mn$ nodes), leading to time $O(mn^{2})$ to build one
instance of _overlaps_. We observe that it is easy to speed up this step using
balanced search trees, but we leave optimizations to further extensions of
this work. To sum up, the $O(m)$ calls to GetBestTree cost overall time
$O(m^{3}n^{2})$. Function FixForest iterates $MAX\\_ITER$ times the for loop
at line 35, which iterates over all possible combinations of $\sigma(f,v)$ and
$\sigma(f^{\prime},v^{\prime})$ belonging to two distinct trees of $T^{*}$.
Since there are at most $mn$ nodes in $T^{*}$, the for loop at line 35
iterates at most $O(m^{2}n^{2})$ times. The operations inside the for loop
cost $O(1)$ time. To this cost, we have to add the $MAX\\_ITER$ evaluations of
”$T^{*}$ is not large-spread” (line 33); this predicate can be evaluated in
$O(|T^{*}|^{2})=O(m^{2}n^{2})$ time by comparing all pairs of thresholds
appearing in $T^{*}$. We conclude that the running time of the $O(m)$
iterations of FixForest is in total $O(MAX\\_ITER\cdot m^{3}n^{2})$. This
dominates the running time of the $O(m)$ iterations of GetBestTree, so we
conclude that $O(MAX\\_ITER\cdot m^{3}n^{2})$ is also the running time of
TrainLargeSpread. This cost is paid in addition to the cost of training the
standard random forest at line 2.

As noted above, although it is feasible to reduce this complexity using
appropriate data structures, we observe that $(i)$ training is often performed
only once, so any optimization just offers limited benefits and is left to
future work, and $(ii)$ the number of trees and nodes is often small enough to
make a cubic complexity acceptable.

####  4.2.4. Hierarchical Training

We observe that our training algorithm can fail, in particular when it is not
possible to add one tree to the current large-spread ensemble and reduce to
zero the overlaps by our mutation routine, i.e., the number of overlaps
resulting from adding a tree to the large-spread ensemble is too high.
However, we show in our experimental evaluation (see Section 5) that it is
possible to train large-spread ensembles of different dimensions after some
parameter tuning. In particular, we propose an intuitive and effective
technique to mitigate the risks of failures during training. A key insight is
that the larger the ensemble is, the more difficult it becomes to avoid
violations of the large-spread requirement, because ensembles including many
trees also have many thresholds, hence overlaps become harder to avoid. We
thus propose a _hierarchical_ training approach as follows:

  1. (1)

We first partition the set of features in $l$ disjoint subsets and we build
$l$ different projections of the training set $\mathcal{D}_{\textit{train}}$,
based on such feature sets.

  2. (2)

We train a large-spread ensemble of size $\frac{m}{l}$ on each of the $l$
different training sets using Algorithm 3 and we finally merge all the trained
ensembles into an ensemble of $m$ trees.

Note that the final ensemble is indeed large-spread, because each of the
merged ensembles ensures the large-spread condition on the trees therein, and
trees from different ensembles cannot violate the large-spread condition
because they are built on disjoint sets of features. For example, an ensemble
of 100 trees can be trained by building 4 disjoint projections of the training
data (based on feature partitioning) and training an ensemble of 25 trees on
each of them. We empirically observed that this approach may improve the
effectiveness of the training process, by enabling the construction of larger
ensembles in practice. We report on experiments confirming this observation in
the next section.

##  5\. Experimental Evaluation

###  5.1. Experimental Setup

To show the practical relevance of our theory, we develop two tools on top of
it and we prove their effectiveness on public datasets.

####  5.1.1. Tools

Our first tool CARVE222CARVE - CompositionAl Robustness Verifier for tree
Ensembles is a C++ implementation of the proposed robustness verification
algorithm for large-spread ensembles (Algorithm 2). It takes as input a random
forest classifier $T$, a norm $p$, a maximum perturbation $k$ and a test set
$\mathcal{D}_{\textit{test}}$ to return as output the robustness score
$r_{A_{p,k}}(T,\mathcal{D}_{\textit{test}})$. CARVE assumes that $T$ is large-
spread and implements majority voting as the aggregation scheme of individual
tree predictions.

Our second tool LSE is a sequential Python implementation of the proposed
training algorithm for large-spread ensembles (Algorithm 3). Starting from a
training set $\mathcal{D}_{\textit{train}}$, a number of trees $m$, a norm $p$
and a maximum perturbation $k$, it returns a large-spread ensemble $T^{*}$ of
$m$ trees (unless the training algorithm fails by returning $\bot$). The
random forest trained before pruning is created using the traditional
implementation of sklearn.

Table 2. Dataset statistics Dataset | Instances | Features | Distribution
---|---|---|---
FashionMNIST clothes | 13866 | 784 | 50%
MNIST26 | 14000 | 784 | 51%
REWEMA | 6271 | 630 | 50%
Table 3. Accuracy and robustness measures for traditional and large-spread ensembles. Robustness is computed against $A_{\infty,k}$. We highlight in bold the cases in which the gap between the accuracy and the robustness of the traditional tree-based ensemble and large-spread ensemble is at least of $0.05$. Dataset | $k$ | Trees | Depth | Accuracy | Robustness
---|---|---|---|---|---
Traditional | Large-Spread | Traditional | Large-Spread
Fashion-MNIST clothes | $0.005$ | 25 | 4 | 0.93 | 0.91 | 0.90 | 0.90
101 | 6 | 0.96 | 0.95 | 0.91 | 0.92
$0.01$ | 25 | 4 | 0.93 | 0.91 | 0.86 | 0.86
101 | 6 | 0.96 | 0.93 | 0.79 | 0.90
$0.015$ | 25 | 4 | 0.93 | 0.91 | 0.60 | 0.81
101 | 6 | 0.96 | 0.91 | 0.51 $\pm$ 0.01 | 0.85
MNIST2-6 | $0.005$ | 25 | 4 | 0.97 | 0.98 | 0.90 | 0.91
101 | 6 | 0.99 | 0.99 | 0.94 | 0.97
$0.01$ | 25 | 4 | 0.97 | 0.98 | 0.72 | 0.89
101 | 6 | 0.99 | 0.99 | 0.77 $\pm$ 0.02 | 0.93
$0.015$ | 25 | 4 | 0.97 | 0.98 | 0.64 | 0.80
101 | 6 | 0.99 | 0.99 | 0.67 $\pm$ 0.05 | 0.89
REWEMA | $0.005$ | 25 | 4 | 0.88 | 0.87 | 0.85 | 0.85
101 | 6 | 0.98 | 0.89 | 0.88 | 0.89
$0.01$ | 25 | 4 | 0.88 | 0.87 | 0.83 | 0.86
101 | 6 | 0.98 | 0.88 | 0.86 | 0.87
$0.015$ | 25 | 4 | 0.88 | 0.88 | 0.83 | 0.84
101 | 6 | 0.98 | 0.87 | 0.78 | 0.84

####  5.1.2. Methodology

Our experimental evaluation is performed on three publicly available datasets:
MNIST333https://www.openml.org/search?type=data&sort=runs&id=554, Fashion-
MNIST444https://www.openml.org/search?type=data&sort=runs&id=40996&status=active
and REWEMA555https://www.kaggle.com/code/kerneler/starter-
rewema-c5ce57b7-e/input. Since MNIST and Fashion-MNIST are datasets associated
to multiclass classification tasks and we focus on binary classification tasks
in this work, we consider two subsets of them, MNIST26 and Fashion-MNIST
clothes. The former dataset contains all the instances of MNIST representing
the digits 2 and 6; the latter uses the instances of classes 0 (T-shirt/top)
and 3 (Dress) of Fashion-MNIST. The key characteristics of the chosen datasets
are reported in Table 2. The first two datasets are extensively used in the
robustness verification literature (Andriushchenko019, ; ChenZS0BH19, ;
RanzatoZ20, ; WangZCBH20, ), while the third dataset is associated with a
security relevant classification task (malware detection), for which the
robustness verification of the employed classifier is critically important. In
general, we choose datasets with a high number of features, where it may be
useful to train large tree ensembles to reach the best performance. Each
dataset is partitioned into a training set and a test set, using 70/30
stratified random sampling.

In our experimental evaluation we make use of two training algorithms to learn
different types of classifiers: $(i)$ a majority-voting classifier based on a
traditional random forest trained using sklearn, and $(ii)$ a majority-voting
classifier based on a large-spread tree ensemble trained using LSE. Moreover,
we consider tree-based classifiers of different sizes: $(i)$ small ensembles
with $25$ trees of maximum depth $4$; $(ii)$ large ensembles with $101$ trees
with maximum depth $6$. We only consider ensembles with an odd number of trees
in order to avoid ties in classification.

Robustness verification is then performed using CARVE and SILVA, a state-of-
the-art verifier for traditional decision tree ensembles based on abstract
interpretation (RanzatoZ20, ). Note that SILVA can be applied to arbitrary
ensembles, while CARVE can only be used on large-spread ensembles. Since SILVA
leverages the hyper-rectangle abstract domain for verification, which does not
introduce any loss of precision for $L_{\infty}$-norm attackers but might lead
to an over-approximation for generic $L_{p}$-norm attackers, we only focus on
$L_{\infty}$-attackers in our experiments to carry out a fair comparison. We
consider three different perturbations $k\in\\{0.005,0.01,0.015\\}$.

####  5.1.3. LSE Setup

Our tool LSE requires the user to specify the value of some additional
parameters (described in Section 4.2) with respect to the traditional
implementation of the training algorithm for random forests by sklearn. The
norm $p$ and the perturbation $k$ depend on the assumed attacker’s
capabilities, so they do not require a particular tuning. Still, the number of
partitions $l$ for the hierarchical training and the maximum number of
iterations $MAX\\_ITER$ of the FixForest procedure require some tuning.
Indeed, although partitioning the features may enable the training of larger
ensembles, a too high number of partitions might negatively affect the
accuracy of the resulting large-spread ensemble, because each sub-forest has
only a partial view on the set of available features and some patterns may not
be learned. In the same way, the maximum number of rounds $MAX\\_ITER$ has an
impact on the success of the training procedure, since a minimum number of
rounds is required to adjust the thresholds of the ensemble, but a too high
number of rounds may modify the thresholds too much and downgrade the
predictive power of the model. We perform some experiments in order to assess
the influence of the two parameters on the success of training a large-spread
ensemble and on the accuracy of the resulting model. For space reasons, we
discuss the results in Appendix C. In the next experiments, we let the value
of $l$ range from one to four, while we take the value of $MAX\\_ITER$ from
the set $\\{100,500,1000\\}$. We choose the best values by using grid-search,
looking for the values that give the large-spread ensemble with the best
accuracy on each test set.

###  5.2. Accuracy and Robustness Results

In our first experiment, we assess whether large-spread ensembles are
effective at classification and we analyze their robustness properties.
Indeed, the large-spread condition enforced on the ensemble limits the model
shape, thus potentially reducing its predictive power with respect to
traditional, unconstrained tree ensembles. At the same time, since we are not
just concerned about accuracy but we target robustness, we also analyze how
large-spread ensembles fare against evasion attacks. We compare accuracy and
robustness against a traditional random forest of the same size. The
robustness of the models is computed using SILVA, since CARVE can only be used
for verifying large-spread ensembles. We set a limit on the verification time
per instance of one second, as in (RanzatoZ20, ).

Table 3 shows the experimental results of our evaluation. Note that the value
of robustness may be approximate, since SILVA may not be able to verify
robustness on some instances within the time limit; for these cases, we
provide lower and upper bounds of robustness, using the $\pm$ notation. The
results highlight that the large-spread ensembles are reasonably accurate and
more robust than the random forests of the same size. In particular, the
accuracy of the large-spread ensembles is at most $0.03$ lower than the
accuracy of the corresponding traditional model in the majority of the cases,
while the improvement in robustness is at least of $0.03$ points in around
half of the cases. This is reassuring, because accuracy was at stake, since
the large-spread condition restricts the shape of the ensemble and might be
associated to a reduction of predictive power. The increase of robustness is
an interesting byproduct of the large-spread condition: since thresholds in
different trees are far way, evasion attacks are empirically harder to craft.
Observe that the accuracy and robustness values of the large-spread ensembles
on the MNIST26 and Fashion-MNIST clothes test sets show that large-spread
models present better performance overall than the traditional ensembles. The
accuracy of the large-spread ensembles on these two test sets is usually equal
to the one of the traditional ensembles, while the robustness value improves
of at least $0.05$ in half of the cases, in particular when the biggest
considered perturbation $k$ is used as the attacker’s capability. For example,
the robustness of the large-spread ensemble with $101$ trees of maximum depth
$6$ and perturbation $0.015$ is at least $0.16$ points higher than the
robustness of the corresponding random forest, while the accuracy decreases
only by $0.05$ points at most. When the value of the perturbation $k$ is the
lowest considered, i.e., $0.005$, the results are still positive, since the
large-spread ensembles preserve around the same accuracy and robustness of the
traditional ensemble.

We see a slightly different trend in the results for the REWEMA dataset: the
robustness of large-spread ensembles is always equal to or greater than the
robustness of the traditional ensembles, but the gap in accuracy with respect
to the traditional ensembles may increase. For example, the large spread
ensemble of $101$ trees with maximum depth $6$ presents $0.84$ robustness with
perturbation $0.015$ ($+0.06$ w.r.t the robustness of the corresponding
traditional tree ensemble) and its accuracy is $0.87$ ($-0.11$ w.r.t. the
accuracy of the traditional tree ensemble). This confirms that an improvement
in robustness often occurs at the price of a decrease in accuracy, because of
the classic trade-off between accuracy and robustness (TsiprasSETM19, ). Even
in these cases though, adopting large-spread ensembles continues to be
beneficial: the accuracy is always way above the majority class distribution,
so the model is usable in the non-adversarial setting, while being more robust
than the traditional counterpart and amenable for efficient security
verification.

###  5.3. Efficiency of Robustness Verification

We now compare the SILVA and CARVE robustness verification tools along two
different dimensions: verification time and memory consumption. For
simplicity, we only focus on the verification of large ensembles with $101$
trees and maximum depth $6$ on the MNIST26 dataset with $k=0.015$. As emerged
from the results in Section 5.2, this is a setting where a state-of-the-art
approach like SILVA clearly shows its limits: indeed, SILVA could not provide
a precise estimate of the robustness of this model ($\pm$ 0.05). In order to
measure the verification time per instance and setting timeouts in the same
way for both the tools, we use the GNU commands time and timeout that measure
the elapsed wall clock time. The former command is also used to compute the
maximum amount of physical memory allocated to the verifier. When it is
required to set a maximum amount of physical memory that the process can use,
we use the Linux kernel feature cgroup. All the experiments are performed on a
virtual machine with 103 GB of RAM and Ubuntu 20.04.4 LTS, running on a server
with an Intel Xeon Gold 6148 2.40GHz.

(a) Number of verified instances of the test set when varying the time limit
in seconds for the verification. (b) Number of verified instances of the test
set when varying the maximum memory consumption limit during the verification.

Figure 3. Comparison of the time and memory efficiency of SILVA and CARVE on
the MNIST26 dataset (we consider ensembles with 101 trees of maximum depth 6).

####  5.3.1. Time Efficiency

In our first experiment we compare the robustness verification times for
traditional tree ensembles using SILVA and the robustness verification times
for large-spread ensembles using CARVE. This way, we compare a state-of-the-
approach for adversarial machine learning models (i.e., what we would do
today) against our custom algorithm designed to take advantage of the large-
spread condition (i.e., what we put forward in this paper). In the experiments
of Section 5.2, we set the maximum verification time per instance of SILVA to
one second. However, SILVA may complete the verification also on more
difficult instances if more time is granted, e.g., 60 seconds (RanzatoZ20, ).
In order to perform a fair comparison, we compare how many instances of the
MNIST26 test set can be verified under growing time limits per instance, i.e.,
from one second to 10 minutes. This methodology allows us to figure out on how
many instances the verification is really difficult. Note that the timeout of
10 minutes per instance is already extremely large, since test sets normally
include thousands of instances.

Figure 3a shows the results of our experiment. The plot shows that SILVA is
not able to verify the robustness of the traditional tree ensemble on 434
instances in less than one second and on 190 instances in less than one
minute, providing just approximate robustness estimates with an uncertainty of
0.10 ($\pm 0.05$) and 0.05 ($\pm 0.025$) respectively. On the other hand, our
tool CARVE requires _less than one second_ per instance to verify the
robustness of the large-spread ensemble on all the instances of the test set,
providing an exact estimate of the robustness of the model. As the maximum
amount of verification time per instance increases, the number of instances on
which SILVA is not able to verify the robustness of the model further
decreases, e.g., 168 instances with a timeout of 120 seconds and 166 instances
with a timeout of 180 seconds. Even though the robustness estimate of SILVA
becomes more precise as the timeout per instance increases, i.e., the
uncertainty on robustness decreases to 0.04 ($\pm 0.02$) with a timeout per
instance of 180 seconds, this process eventually hits a wall: the remaining
166 instances cannot be verified even when the timeout increases to 10 minutes
per instance. Moreover, the improved precision comes at the cost of an higher
total verification time: with a timeout of 120 seconds, SILVA requires in
total 22220 seconds to verify the traditional tree ensemble on the entire
MNIST26 test set, while CARVE requires just 129 seconds in total, i.e., a
reduction of two orders of magnitude. As expected, the results show the
pitfalls of the complete robustness verification on traditional tree-ensembles
and the improvements in the verification time enabled by the large-spread
condition. Since the verification problem is NP-complete, there may be
instances on which the verification time increases exponentially, while the
large-spread condition allows one to train tree ensembles whose robustness can
be verified in polynomial time on all the possible instances of the feature
space.

####  5.3.2. Memory Efficiency

Our first experiment provides only a partial picture of the efficiency of the
robustness verification and the reasons for the potential inefficiency of
SILVA. Indeed, memory constraints should also be taken into account during
robustness verification, since a high memory consumption may make the
verification unfeasible on standard commercial systems.

In our second experiment, we compare the memory efficiency of SILVA and CARVE.
In particular, we compare how many instances can be verified given a growing
maximum memory consumption limit per instance, setting the maximum amount of
verification time per instance to 10 minutes. The results of our experiment
are shown in Figure 3b. The results highlight that SILVA may consume a lot of
memory in order to provide precise robustness estimates. In the best scenario,
with 100 GB of memory available, SILVA is still unable to verify the
robustness of the model on 168 instances, providing just an approximate
estimate of the robustness of the traditional tree-based ensemble with an
uncertainty of 0.04 ($\pm 0.02$). Even though the interval on which the
robustness approximation is not so large in this setting, the plot shows that
the number of instances that SILVA can not verify increases as the memory
consumption limit decreases, expanding also the uncertainty of SILVA in the
robustness estimation. For example, SILVA is not able to verify the robustness
of the model on 216 and 342 instances with the memory consumption limit of 32
GB and 4 GB respectively, providing an uncertainty in the robustness estimates
of 0.05 ($\pm 0.025$) and 0.08 ($\pm 0.04$). Instead, CARVE manages to verify
the robustness of the large-spread ensemble on all the MNIST26 test set using
_less than 4GB of memory_ per instance, providing an exact value of
robustness. More precisely, the maximum memory consumption by CARVE is less
than 1 GB in practice. The results confirm the efficiency in terms of memory
consumption of our proposal and the unfeasibility of obtaining an exact value
of robustness on traditional tree ensembles using a state-of-the-art verifier
like SILVA when memory consumption constraints are imposed.

####  5.3.3. Efficiency Under Time and Memory Constraints

We finally perform a comparison between CARVE and SILVA when enforcing both a
maximum verification time limit and a maximum memory consumption limit. In
particular, we compare the total verification time, the maximum memory
consumption and the number of instances on which the tool is not able to
return an answer given a maximum verification time of 60 seconds per instance
and a maximum memory consumption limit of 64 GB.

Table 4. Comparison of total verification time and maximum memory consumption of SILVA and CARVE on the MNIST26 test set. The last column reports the number of instances on which the verifier was not able to provide an answer because it exceeded the time or memory limits. Tool | Total Time (s) | Memory (GB) | # Failures
---|---|---|---
SILVA | 14448 | 64 | 190
CARVE | 129 | 0.03 | 0

Table 4 shows the results of our experiment. The results confirm the
observations from the previous sections: CARVE is far more efficient of SILVA
in terms of both verification time and memory consumption. In particular,
CARVE outperforms SILVA on the total verification time on the MNIST26 test
set, verifying the large-spread ensemble on all the instances in just 129
seconds, thus being 112 times faster than SILVA (that requires 14448 seconds).
Moreover, the memory consumption of CARVE is more than 2000 times lower than
the one of SILVA, using just 0.03 GB of memory capacity, thus CARVE is usable
on commodity hardware. Finally, SILVA is not able to provide an answer on 190
instances of the test set, providing an approximated robustness estimate with
an uncertainty of 0.05 ($\pm 0.025$), while CARVE is able to provide the exact
robustness value.

###  5.4. Take-Away Messages

Our experimental evaluation shows that:

  * •

Large-spread ensembles do not sacrifice too much predictive power with respect
to traditional tree ensembles. In particular, the accuracy of large-spread
ensembles is often equal to the accuracy of traditional tree ensembles of the
same size. Even in the few cases where accuracy decreases, it still remains
way higher than the majority class of the test set.

  * •

Large-spread ensembles are generally more robust than traditional tree
ensembles. This empirical observation is a useful byproduct of the large-
spread condition, which makes it harder to craft evasion attacks which are
effective against multiple trees in the ensemble.

  * •

Our verification tool for large-spread ensemble CARVE is much more efficient
than SILVA, a state-of-the-art verifier for traditional tree ensembles.
Improvements are due to both verification time and memory consumption.

Concretely, we showed that SILVA can provide just approximate robustness
estimates in some experimental settings, even when provided with extremely
high time and memory bounds (10 minutes per instance, 100 GB of RAM).
Conversely, CARVE can compute the exact value of robustness using just limited
time and memory (1 second per instance, 1 GB of RAM). This shows the
effectiveness of the verifiable learning paradigm: models trained with formal
verification in mind can be verified in a matter of seconds even on
traditional commercial hardware, contrary to traditional machine learning
models which cannot be accurately verified even when extremely powerful
servers are available.

##  6\. Related Work

We already mentioned that prior work studied the complexity of the robustness
verification problem for decision tree ensembles (KantchelianTJ16, ;
WangZCBH20, ). This problem was proved to be NP-complete for arbitrary
$L_{p}$-norm attackers, even when restricting the model shape to decision
stump ensembles (Andriushchenko019, ; WangZCBH20, ). To the best of our
knowledge, we are the first to identify a specific class of decision tree
ensembles enabling robustness verification in polynomial time. Prior work on
robustness verification for decision tree ensembles proposed different
techniques, such as exploiting equivalence classes extracted from the tree
ensemble (TornblomN20, ), integer linear programming (KantchelianTJ16, ), a
reduction to the max clique problem (ChenZS0BH19, ), abstract interpretation
(RanzatoZ20, ; CalzavaraFL20, ) and satisfiability modulo theory (SMT) solving
(DevosMD21, ; EinzigerGSS19, ; SatoKNO20, ). Though effective in many cases,
these techniques still have to deal with the exponential complexity of the
robustness verification problem, so they are bound to fail for large ensembles
and complex datasets. We experimentally showed that a state-of-the-art
verifier like SILVA (RanzatoZ20, ) is much less efficient than our verifiable
learning approach, supporting verification in polynomial time, and can only
compute approximate robustness estimates in practical cases. Moreover, our LSE
training algorithm produces tree ensembles that are in general more robust
than the traditional counterparts as a side-effect of imposing that the
thresholds of different trees are sufficiently far away. Several papers in the
literature discussed new algorithms for training tree ensembles that are
robust to evasion attacks (CalzavaraLTAO20, ; CalzavaraLT19, ; ChenZBH19, ;
KantchelianTJ16, ; Andriushchenko019, ; VosV21, ; RanzatoZ21, ), but our work
is complementary to them. Indeed, our primary goal is not enforcing
robustness, which is a byproduct of our training algorithm, but supporting
efficient robustness verification of the trained models.

It is worth mentioning that a lot of work has been done on the robustness
verification of deep neural networks (DNNs), that was also proved to be a NP-
complete problem (KatzBDJK17, ). Typical approaches for exact verification
often do not scale to large DNNs, as for tree ensembles, and they are
typically based on SMT solvers (KatzBDJK17, ; KatzHIJLLSTWZDK19, ; HuangKWW17,
) and integer linear programming solvers (BastaniILVNC16, ; LomuscioM17, ;
TjengXT19, ; DuttaJST18, ). To mitigate the scalability problems of robustness
verification, different proposals have been done, such as shrinking the
original DNN through pruning (GuidottiLPT20, ) and finding specific classes of
DNNs that empirically enable more efficient robustness verification (JiaR20,
). Xiao et. al. (XiaoTSM19, ) proposed the idea of co-designing model training
and verification, i.e., training models that show reasonable accuracy and
robustness, while better enabling exact verification. In particular, their
work proposes a training algorithm for DNNs that encourages weight sparsity
and ReLU stability, two properties that improve the efficiency of verification
through SMT solving. There are significant differences between these lines of
work and ours. First, prior techniques only provide empirical efficiency
guarantees, while our proposal leads to a formal complexity reduction of the
robustness verification problem. This enables the design of a polynomial time
algorithm for robustness verification, which is crucial when the size and the
complexity of the verified model increase. Moreover, our research deals with
tree ensembles rather than DNNs.

Finally, we observe that recent work explored the adversarial robustness of
model ensembles (YangLXK0L22, ). The main result of this work proved that the
combination of “diversified gradient” and “large confidence margin” are
sufficient and necessary conditions for certifiably robust ensemble models.
While this result cannot be directly applied to non-differentiable models such
as decision tree ensembles, the intuition of diversifying models is similarly
captured by our large-spread condition. We plan to explore any intriguing
connections with this proposal as future work.

##  7\. Conclusion

We introduced the general idea of _verifiable learning_ , i.e., the adoption
of training algorithms designed to learn restricted model classes amenable for
efficient security verification. We applied this idea to decision tree
ensembles, identifying the class of _large-spread_ ensembles. We showed that
this class of ensembles admits robustness verification in polynomial time,
whereas the problem is NP-hard for general decision tree models. We then
proposed a pruning-based training algorithm to learn large-spread ensembles
from traditional decision tree ensembles. Our experiments on public datasets
show that large-spread ensembles largely preserve the predictive power of
traditional tree ensembles, yet their robustness is normally higher and much
more efficient to verify. This makes large-spread ensembles particularly
appealing in the adversarial setting.

As future work, we plan to investigate the use of verifiable learning also for
other popular model classes, e.g., neural networks. Moreover, we want to
explore different training algorithms for large-spread ensembles and compare
their effectiveness against the pruning-based approach proposed in this paper.

## References

  * (1) Andriushchenko, M., Hein, M.: Provably robust boosted decision stumps and trees against adversarial attacks. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d’Alché-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 12997–13008 (2019), https://proceedings.neurips.cc/paper/2019/hash/4206e38996fae4028a26d43b24f68d32-Abstract.html
  * (2) Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V., Criminisi, A.: Measuring neural net robustness with constraints. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain. pp. 2613–2621 (2016), https://proceedings.neurips.cc/paper/2016/hash/980ecd059122ce2e50136bda65c25e07-Abstract.html
  * (3) Biggio, B., Corona, I., Maiorca, D., Nelson, B., Srndic, N., Laskov, P., Giacinto, G., Roli, F.: Evasion attacks against machine learning at test time. In: Blockeel, H., Kersting, K., Nijssen, S., Zelezný, F. (eds.) Machine Learning and Knowledge Discovery in Databases - European Conference, ECML PKDD 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part III. Lecture Notes in Computer Science, vol. 8190, pp. 387–402. Springer (2013). https://doi.org/10.1007/978-3-642-40994-3_25, https://doi.org/10.1007/978-3-642-40994-3_25
  * (4) Breiman, L.: Random forests. Mach. Learn. 45(1), 5–32 (2001). https://doi.org/10.1023/A:1010933404324, https://doi.org/10.1023/A:1010933404324
  * (5) Breiman, L., Friedman, J.H., Olshen, R.A., Stone, C.J.: Classification and Regression Trees. Wadsworth (1984)
  * (6) Calzavara, S., Ferrara, P., Lucchese, C.: Certifying decision trees against evasion attacks by program analysis. In: Chen, L., Li, N., Liang, K., Schneider, S.A. (eds.) Computer Security - ESORICS 2020 - 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12309, pp. 421–438. Springer (2020). https://doi.org/10.1007/978-3-030-59013-0_21, https://doi.org/10.1007/978-3-030-59013-0_21
  * (7) Calzavara, S., Lucchese, C., Tolomei, G.: Adversarial training of gradient-boosted decision trees. In: Zhu, W., Tao, D., Cheng, X., Cui, P., Rundensteiner, E.A., Carmel, D., He, Q., Yu, J.X. (eds.) Proceedings of the 28th ACM International Conference on Information and Knowledge Management, CIKM 2019, Beijing, China, November 3-7, 2019. pp. 2429–2432. ACM (2019). https://doi.org/10.1145/3357384.3358149, https://doi.org/10.1145/3357384.3358149
  * (8) Calzavara, S., Lucchese, C., Tolomei, G., Abebe, S.A., Orlando, S.: Treant: training evasion-aware decision trees. Data Min. Knowl. Discov. 34(5), 1390–1420 (2020). https://doi.org/10.1007/s10618-020-00694-9, https://doi.org/10.1007/s10618-020-00694-9
  * (9) Chen, H., Zhang, H., Boning, D.S., Hsieh, C.: Robust decision trees against adversarial examples. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA. Proceedings of Machine Learning Research, vol. 97, pp. 1122–1131. PMLR (2019), http://proceedings.mlr.press/v97/chen19m.html
  * (10) Chen, H., Zhang, H., Si, S., Li, Y., Boning, D.S., Hsieh, C.: Robustness verification of tree-based models. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d’Alché-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada. pp. 12317–12328 (2019), https://proceedings.neurips.cc/paper/2019/hash/cd9508fdaa5c1390e9cc329001cf1459-Abstract.html
  * (11) Demetrio, L., Coull, S.E., Biggio, B., Lagorio, G., Armando, A., Roli, F.: Adversarial exemples: A survey and experimental evaluation of practical attacks on machine learning for windows malware detection. ACM Trans. Priv. Secur. 24(4), 27:1–27:31 (2021). https://doi.org/10.1145/3473039, https://doi.org/10.1145/3473039
  * (12) Devos, L., Meert, W., Davis, J.: Verifying tree ensembles by reasoning about potential instances. In: Demeniconi, C., Davidson, I. (eds.) Proceedings of the 2021 SIAM International Conference on Data Mining, SDM 2021, Virtual Event, April 29 - May 1, 2021. pp. 450–458. SIAM (2021). https://doi.org/10.1137/1.9781611976700.51, https://doi.org/10.1137/1.9781611976700.51
  * (13) Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Muñoz, C.A., Narkawicz, A. (eds.) NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10811, pp. 121–138. Springer (2018). https://doi.org/10.1007/978-3-319-77935-5_9, https://doi.org/10.1007/978-3-319-77935-5_9
  * (14) Einziger, G., Goldstein, M., Sa’ar, Y., Segall, I.: Verifying robustness of gradient boosted models. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019. pp. 2446–2453. AAAI Press (2019). https://doi.org/10.1609/aaai.v33i01.33012446, https://doi.org/10.1609/aaai.v33i01.33012446
  * (15) Guidotti, D., Leofante, F., Pulina, L., Tacchella, A.: Verification of neural networks: Enhancing scalability through pruning. In: Giacomo, G.D., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J. (eds.) ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 2505–2512. IOS Press (2020). https://doi.org/10.3233/FAIA200384, https://doi.org/10.3233/FAIA200384
  * (16) Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 3–29. Springer (2017). https://doi.org/10.1007/978-3-319-63387-9_1, https://doi.org/10.1007/978-3-319-63387-9_1
  * (17) Jia, K., Rinard, M.C.: Efficient exact verification of binarized neural networks. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020), https://proceedings.neurips.cc/paper/2020/hash/1385974ed5904a438616ff7bdb3f7439-Abstract.html
  * (18) Kantchelian, A., Tygar, J.D., Joseph, A.D.: Evasion and hardening of tree ensemble classifiers. In: Balcan, M., Weinberger, K.Q. (eds.) Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016. JMLR Workshop and Conference Proceedings, vol. 48, pp. 2387–2396. JMLR.org (2016), http://proceedings.mlr.press/v48/kantchelian16.html
  * (19) Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 97–117. Springer (2017). https://doi.org/10.1007/978-3-319-63387-9_5, https://doi.org/10.1007/978-3-319-63387-9_5
  * (20) Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 443–452. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_26, https://doi.org/10.1007/978-3-030-25540-4_26
  * (21) Ke, G., Meng, Q., Finley, T., Wang, T., Chen, W., Ma, W., Ye, Q., Liu, T.: Lightgbm: A highly efficient gradient boosting decision tree. In: Guyon, I., von Luxburg, U., Bengio, S., Wallach, H.M., Fergus, R., Vishwanathan, S.V.N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA. pp. 3146–3154 (2017), https://proceedings.neurips.cc/paper/2017/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html
  * (22) Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRR abs/1706.07351 (2017), http://arxiv.org/abs/1706.07351
  * (23) Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings. OpenReview.net (2018), https://openreview.net/forum?id=rJzIBfZAb
  * (24) Ranzato, F., Zanella, M.: Abstract interpretation of decision tree ensemble classifiers. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. pp. 5478–5486. AAAI Press (2020), https://ojs.aaai.org/index.php/AAAI/article/view/5998
  * (25) Ranzato, F., Zanella, M.: Genetic adversarial training of decision trees. In: Chicano, F., Krawiec, K. (eds.) GECCO ’21: Genetic and Evolutionary Computation Conference, Lille, France, July 10-14, 2021. pp. 358–367. ACM (2021). https://doi.org/10.1145/3449639.3459286, https://doi.org/10.1145/3449639.3459286
  * (26) Sato, N., Kuruma, H., Nakagawa, Y., Ogawa, H.: Formal verification of a decision-tree ensemble model and detection of its violation ranges. IEICE Trans. Inf. Syst. 103-D(2), 363–378 (2020). https://doi.org/10.1587/transinf.2019EDP7120, http://search.ieice.org/bin/summary.php?id=e103-d_2_363
  * (27) Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: Bengio, Y., LeCun, Y. (eds.) 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings (2014), http://arxiv.org/abs/1312.6199
  * (28) Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net (2019), https://openreview.net/forum?id=HyGIdiRqtm
  * (29) Törnblom, J., Nadjm-Tehrani, S.: Formal verification of input-output mappings of tree ensembles. Sci. Comput. Program. 194, 102450 (2020). https://doi.org/10.1016/j.scico.2020.102450, https://doi.org/10.1016/j.scico.2020.102450
  * (30) Tsipras, D., Santurkar, S., Engstrom, L., Turner, A., Madry, A.: Robustness may be at odds with accuracy. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net (2019), https://openreview.net/forum?id=SyxAb30cY7
  * (31) Vos, D., Verwer, S.: Efficient training of robust decision trees against adversarial examples. In: Meila, M., Zhang, T. (eds.) Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event. Proceedings of Machine Learning Research, vol. 139, pp. 10586–10595. PMLR (2021), http://proceedings.mlr.press/v139/vos21a.html
  * (32) Wang, Y., Zhang, H., Chen, H., Boning, D.S., Hsieh, C.: On lp-norm robustness of ensemble decision stumps and trees. In: Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event. Proceedings of Machine Learning Research, vol. 119, pp. 10104–10114. PMLR (2020), http://proceedings.mlr.press/v119/wang20aa.html
  * (33) Xiao, K.Y., Tjeng, V., Shafiullah, N.M.M., Madry, A.: Training for faster adversarial robustness verification via inducing relu stability. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net (2019), https://openreview.net/forum?id=BJfIVjAcKm
  * (34) Yang, Z., Li, L., Xu, X., Kailkhura, B., Xie, T., Li, B.: On the certified robustness for ensemble models and beyond. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net (2022), https://openreview.net/forum?id=tUa4REjGjTf

##  Appendix A Proof of Theorem 3.2

We introduce the following auxiliary notation:
$\textit{opt}(t,p,k,\vec{x},y)=\operatorname*{arg\,min}_{\vec{\delta}\in
S}||\vec{\delta}||_{p}$ where
$S=\\{\vec{\delta}\,|\,||\vec{\delta}||_{p}\in\textsc{Reachable}(t,p,k,\vec{x},y)\\}$.

Note that $\textsc{Reachable}(t,p,k,\vec{x},y)$ visits every leaf of $t$.
Therefore, $\textit{opt}(t,p,k,\vec{x},y)$ is undefined iff
$\textsc{Reachable}(t,p,k,\vec{x},y)=\varnothing$, i.e., Reachable does not
visit any leaf with label different from $y$.

###### Lemma A.1.

Let $\vec{\delta}=\textit{opt}(t,p,k,\vec{x},y)$. Then the following
properties hold:

  1. (1)

If $\vec{\delta}$ is undefined, then there does not exist any $\vec{z}\in
A_{p,k}(\vec{x})$ such that $t(\vec{z})\neq y$.

  2. (2)

If $\vec{\delta}$ is defined, then $\vec{z}_{o}=\vec{x}+\vec{\delta}\in
A_{p,k}(\vec{x})$ and $t(\vec{z}_{o})\neq y$. Moreover, for every $\vec{z}\in
A_{p,k}(\vec{x})$ such that $t(\vec{z})\neq y$ we have
$||\vec{z}_{o}||_{p}\leq||\vec{z}||_{p}$.

###### Proof.

(1) If $\vec{\delta}$ is undefined then
$\textsc{Reachable}(t,p,k,\vec{x},y)=\varnothing$. This means there is no
perturbation $\vec{\delta^{\prime}}=\vec{z}-\vec{x}$ computed during a call to
Reachable such that $||\vec{\delta^{\prime}}||\leq k$ and is able to push
$\vec{z}$ into a leaf with label different from $y$. That is, $t(\vec{z})\neq
y$. (2) If $\vec{\delta}$ is defined, then
$||\vec{z_{o}}-\vec{x}||=||\vec{\delta}||\leq k$, hence $\vec{z_{o}}\in
A_{p,k}(\vec{x})$. In particular, $\vec{z}_{o}=\vec{x}+\vec{\delta}$ is the
attack of minimum cost since $\vec{\delta}$ is the minimum perturbation, hence
it must be $t(\vec{z_{o}})\neq y$ and
$||\vec{\delta}||_{p}\leq||\vec{\delta^{\prime}}||_{p}$ for any other
$\vec{\delta^{\prime}}$ such that $\vec{z}=\vec{x}+\vec{\delta^{\prime}}\in
A_{p,k}(\vec{x})$. But
$||\vec{\delta}||_{p}\leq||\vec{\delta^{\prime}}||_{p}\iff||\vec{z_{o}}-\vec{x}||_{p}\leq||\vec{z}-\vec{x}||_{p}\iff||\vec{z_{o}}||_{p}\leq||\vec{z}||_{p}$.
∎

###### Lemma A.2.

Assume $\psi_{p}(T)>2k$ and consider two distinct trees $t,t^{\prime}\in T$.
Let $\vec{\delta}=\textit{opt}(t,p,k,\vec{x},y)$ and
$\vec{\delta}^{\prime}=\textit{opt}(t^{\prime},p,k,\vec{x},y)$ be defined,
then we have
$\textit{supp}(\vec{\delta})\cap\textit{supp}(\vec{\delta}^{\prime})=\varnothing$.

###### Proof.

By contradiction. Assume that there exists a feature $f$ such that
$\delta_{f}\neq 0$ and $\delta_{f}^{\prime}\neq 0$. Since
$\vec{\delta},\vec{\delta}^{\prime}$ are the minimal attacks with respect to
$||\cdot||_{p}$ by Lemma A.1, the feature $f$ must be tested when performing
the predictions $t(\vec{x}+\vec{\delta})$ and
$t^{\prime}(\vec{x}+\vec{\delta}^{\prime})$ respectively, i.e., the prediction
$t(\vec{x}+\vec{\delta})$ must perform a test $x_{f}\leq v$ and the prediction
$t^{\prime}(\vec{x}+\vec{\delta}^{\prime})$ must perform a test $x_{f}\leq
v^{\prime}$ for some thresholds $v,v^{\prime}$. Since
$||v^{\prime}-x_{f}||_{p}=||x_{f}-v^{\prime}||_{p}$, we get
$||v-v^{\prime}||\leq||v-x_{f}||_{p}+||x_{f}-v^{\prime}||_{p}$ by triangle
inequality. Since $||v-x_{f}||_{p}\leq k$ and $||v^{\prime}-x_{f}||_{p}\leq k$
because both $\vec{\delta},\vec{\delta^{\prime}}$ are valid minimal attacks,
this implies $||v-v^{\prime}||\leq 2k$ which contradicts the hypothesis
$\psi_{p}(T)>2k$. ∎

###### Lemma A.3.

Assume $\psi_{p}(T)>2k$ and consider two distinct trees $t,t^{\prime}\in T$.
Let $\vec{x}$ be an instance with label $y$ and let $\vec{z}\in
A_{p,k}(\vec{x})$ be such that $t(\vec{z})\neq y$ and $t^{\prime}(\vec{z})\neq
y$. Then there exist $\vec{\delta}$ and $\vec{\delta}^{\prime}$ such:

  1. (1)

$\vec{z}=\vec{x}+\vec{\delta}+\vec{\delta}^{\prime}$ with
$\textit{supp}(\vec{\delta})\cap\textit{supp}(\vec{\delta}^{\prime})=\varnothing$;

  2. (2)

$t(\vec{x}+\vec{\delta})\neq y$;

  3. (3)

$t^{\prime}(\vec{x}+\vec{\delta}^{\prime})\neq y$.

###### Proof.

Let $\vec{z}=\vec{x}+\vec{\delta}^{*}$. We show an algorithm that constructs
$\vec{\delta}$ and $\vec{\delta}^{\prime}$ with the desired properties (1) –
(3). In particular, the algorithm identifies how to split $\vec{\delta}^{*}$
into $\vec{\delta}$ and $\vec{\delta}^{\prime}$ by partitioning the set of
features. The algorithm takes as input the decision tree $t$, $\vec{x}$ and
$\vec{z}$, and operates as follows:

  * •

Initialize the set $F$ to $\varnothing$;

  * •

Let the root of the tree be $\sigma(f,v,t_{l},t_{r})$;

  * •

If $x_{f}\leq v$ and $z_{f}>v$: let $F=F\cup\\{f\\}$ and recursively visit
$t_{r}$;

  * •

If $x_{f}>v$ and $z_{f}\leq v$: let $F=F\cup\\{f\\}$ and recursively visit
$t_{l}$;

  * •

If $x_{f}\leq v$ and $z_{f}\leq v$: recursively visit $t_{l}$;

  * •

If $x_{f}>v$ and $z_{f}>v$: recursively visit $t_{r}$.

The algorithm terminates by returning $F$ when the visit reaches a leaf. We
then construct $\vec{\delta}$ by setting the features in $F$ to their
corresponding value in $\vec{\delta}^{*}$ and setting the other features to 0;
conversely, we construct $\vec{\delta^{\prime}}$ by setting all the features
not in $F$ to their corresponding value in $\vec{\delta}^{*}$ and setting the
other features to 0. We can show that $\vec{\delta}$ and
$\vec{\delta}^{\prime}$ have the desired properties as follows:

  1. (1)

We have
$\textit{supp}(\vec{\delta})\cap\textit{supp}(\vec{\delta^{\prime}})=\varnothing$
by construction. The fact that
$\vec{\delta}^{*}=\vec{\delta}+\vec{\delta}^{\prime}$ follows by definition of
$\vec{\delta}$ and $\vec{\delta^{\prime}}$, observing that
$\\{\textit{supp}(\vec{\delta}),\textit{supp}(\vec{\delta^{\prime}})\\}$ is a
partition of the set of features;

  2. (2)

We have $t(\vec{x}+\vec{\delta})\neq y$, because $t(\vec{x}+\vec{\delta})$
follows the same prediction path of $t(\vec{z})$ by construction;

  3. (3)

This property follows from the large-spread assumption. In particular, we
define $\vec{z}^{\prime}$ such that $\forall i\in F:z_{i}^{\prime}=x_{i}$ and
$\forall j\not\in F:z_{j}^{\prime}=z_{j}$. We have
$t^{\prime}(\vec{z}^{\prime})\neq y$, because $t^{\prime}(\vec{z}^{\prime})$
follows the same prediction path of $t(\vec{z})$ by construction. Indeed,
features in $F$ cannot affect the prediction path of $t^{\prime}(\vec{z})$
w.r.t. $t^{\prime}(\vec{x})$, since such features already affect the
prediction path of $t(\vec{z})$ w.r.t. $t(\vec{x})$ and $T$ is large-spread.
The property $t^{\prime}(\vec{x}+\vec{\delta}^{\prime})\neq y$ follows by
observing that $\vec{x}+\vec{\delta}^{\prime}=\vec{z}^{\prime}$.

∎

###### Lemma A.4.

Assume $\psi_{p}(T)>2k$ and pick any $T^{\prime}\subseteq T$. Let
$\vec{\delta}_{i}=\textit{opt}(t_{i},p,k,\vec{x},y)$ be defined for every
$t_{i}\in T^{\prime}$. Then for every $\vec{z}\in A_{p,k}(\vec{x})$ such that
$\forall t_{i}\in T^{\prime}:t_{i}(\vec{z})\neq y$ we have
$||\vec{x}+\sum_{i}\vec{\delta}_{i}||_{p}\leq||\vec{z}||_{p}$.

###### Proof.

Let $\vec{\delta}=\vec{z}-\vec{x}$. We want to show that
$||\sum_{i}\vec{\delta}_{i}||_{p}\leq||\vec{\delta}||_{p}$, which yields the
conclusion. Since $\vec{\delta}$ is a perturbation inducing an attack against
all trees in $T^{\prime}$ and $T^{\prime}$ is large-spread, then
$\vec{\delta}$ can be written as the sum of $|T^{\prime}|$ pairwise-orthogonal
perturbations $\\{\vec{\delta^{\prime}_{i}}\\}_{i}$ by Lemma A.3, each
inducing an attack against $t_{i}\in T^{\prime}$, i.e.,
$\vec{\delta}=\sum_{i}\vec{\delta^{\prime}_{i}}$. Hence
$||\vec{\delta}||_{p}=||\sum_{i}\vec{\delta^{\prime}_{i}}||_{p}$. By Lemma
A.1, it must be
$||\vec{\delta^{\prime}_{i}}||_{p}\geq||\vec{\delta_{i}}||_{p}$ because
$\vec{\delta_{i}}=\textit{opt}(t_{i},p,k,\vec{x},y)$. Since
$\\{\vec{\delta_{i}}\\}_{i}$ are also pairwise-orthogonal by Lemma A.2, we
conclude
$||\sum_{i}\vec{\delta^{\prime}_{i}}||_{p}\geq||\sum_{i}\vec{\delta}||_{p}$. ∎

###### Lemma A.5.

If $\textsc{Stable}(T,p,k,\vec{x},y)$ returns True and $\psi_{p}(T)>2k$, then
$T$ is stable on $\vec{x}$ against $A_{p,k}$.

###### Proof.

We perform a case analysis:

  * •

_The number of unstable trees is at least $\frac{m-1}{2}+1$_. This means that
there exist at least $\frac{m-1}{2}+1$ trees $t_{i}\in T$ such that
$\Delta_{i}\in\textsc{Reachable}(t_{i},p,k,\vec{x},y)$. The quantity $\Delta$
calculated by the algorithm is the $L_{p}$ norm of the vector
$||\vec{\delta}||_{p}=\sum_{i=1}^{(m-1)/2+1}\vec{\delta}_{i}$ as in Eq. 5,
with $\Delta_{i}=||\vec{\delta_{i}}||_{p}$. Note that it must be $\Delta>k$
because the algorithm returns True. Assume now by contradiction that there
exists $T^{\prime}\subseteq T$ with $|T^{\prime}|\geq\frac{m-1}{2}+1$ such
that there exists $\vec{z}\in A_{p,k}(\vec{x})$ such that $\forall
t^{\prime}\in T^{\prime}:t^{\prime}(\vec{z})\neq y$, i.e., $T$ is not stable
on $\vec{x}$. Lemma A.4 ensures that $\Delta\leq||\vec{z}-\vec{x}||_{p}$,
hence $||\vec{z}-\vec{x}||_{p}>k$ by transitivity. This is a contradiction,
because $\vec{z}\in A_{p,k}(\vec{x})$, i.e., we conclude that $T$ is stable on
$\vec{x}$.

  * •

_The number of unstable trees is less than $\frac{m-1}{2}+1$_. This means that
there are less than $\frac{m-1}{2}+1$ trees $t_{i}\in T$ such that
$\Delta_{i}\in\textsc{Reachable}(t_{i},p,k,\vec{x},y)$. For Lemma A.1 there
exist at least $\frac{m-1}{2}+1$ trees $t_{i}\in T$ such that
$\forall\vec{z}\in A_{p,k}(\vec{x}):t_{i}(\vec{z})=y$. This implies that
$\forall\vec{z}\in A_{p,k}(\vec{x}):T(\vec{z})=y$, i.e., $T$ is stable on
$\vec{x}$.

∎

###### Lemma A.6.

If $T$ is stable on $\vec{x}$ against $A_{p,k}$ and $\psi_{p}(T)>2k$, then
$\textsc{Stable}(T,p,k,\vec{x},y)$ returns True.

###### Proof.

Assume that $\psi_{p}(T)>2k$. We show that if
$\textsc{Stable}(T,p,k,\vec{x},y)$ returns False, then $T$ is not stable on
$\vec{x}$ against $A_{p,k}$. If the algorithm returns False, it must be
$\Delta\leq k$, i.e., there are at least $\frac{m-1}{2}+1$ trees whose minimal
perturbations $\vec{\delta}_{i}$ are such that $||\vec{\delta}_{i}||_{p}\leq
k$. Hence there exist at least $\frac{m-1}{2}+1$ trees $t_{i}\in T$ such that
$\exists\,\vec{z}\in A_{p,k}(\vec{x}):t_{i}(\vec{z})\neq y$. This implies that
$T$ is not stable on $\vec{x}$. ∎

See 3.2

###### Proof.

Since $\psi_{p}(T)>2k$, Lemma A.5 and Lemma A.6 ensure that
$\textsc{Stable}(T,p,k,\vec{x},y)$ returns True if and only if $T$ is stable
on $\vec{x}$ against the attacker $A_{p,k}(\vec{x})$. The conclusion follows
by observing that $T$ is robust on $\vec{x}$ if and only if $T(\vec{x})=y$ and
$T$ is stable on $\vec{x}$. ∎

##  Appendix B Proof of Theorem 4.1

We here prove the NP-hardness of the large-spread subset problem.

See 4.1

###### Proof.

We show how to reduce an instance of the max-clique problem to the large-
spread subset problem. Let $G=(V,E)$ be an undirected graph, we construct an
ensemble $T$ such that $G$ contains a clique of size $s$ if and only if there
exists $T^{\prime}\subseteq T$ of size $s$ such that $T^{\prime}$ is large-
spread for the attacker $A_{0,0}$ (who does not perturb any feature). In
particular, the construction operates as follows:

  1. (1)

We construct the complementary graph $\overline{G}=(V,\overline{E})$, where
$\\{u,v\\}\in\overline{E}$ if and only if $\\{u,v\\}\not\in E$.

  2. (2)

We introduce a feature $\pi_{E}(e)$ for each $e\in\overline{E}$, i.e., the
dimensionality of the feature space is $|\overline{E}|$. We assume features
are totally ordered, using any ordering convention.

  3. (3)

We construct a decision tree $\pi_{V}(v)$ for each $v\in V$ as follows:

     * •

If $\deg(v)=0$, we let $\pi_{V}(v)$ be a leaf with label +1.

     * •

If $\deg(v)>0$, we let $\pi_{V}(v)$ be a decision tree of depth $\deg(v)$
built on top of the feature set $\\{\pi_{E}(e)~{}|~{}\exists u\in
V:e=\\{u,v\\}\in\overline{E}\\}$. Each level of the tree tests a single
feature from this set with threshold arbitrarily set to 1, following the total
order assumed on features. Leaves are arbitrarily set so that the left child
has label -1 and the right child has label +1.

By construction, decision trees $\pi_{V}(u),\pi_{V}(v)\in T$ share a feature
if and only if $\\{u,v\\}\not\in E$, i.e., $\pi_{V}(u),\pi_{V}(v)\in T$ do not
share any feature if and only if $\\{u,v\\}\in E$. Given that all thresholds
are set to the same value 1 and the attacker does not perturb any feature, any
$T^{\prime}\subseteq T$ is large-spread if and only if the trees in
$T^{\prime}$ do not share any feature. This implies that $G$ has a clique of
size $s$ if and only if there exists $T^{\prime}\subseteq T$ of size $s$ such
that $T^{\prime}$ is large-spread. ∎

##  Appendix C Parameter Tuning for LSE Training

In this section, we present the results of our analysis of the impact of the
number of subsets of features $l$ of hierarchical training and the maximum
number of iterations $MAX\\_ITER$ on our training algorithm LSE. We trained
both small and large large-spread ensembles on the three datasets, varying
also the value of the perturbation $k$ (see the details of the methodology of
our experiments in Section 5.1.2). Table 5 shows the results of our
evaluation, in which we report the accuracy of the trained large-spread
ensembles in case the training is performed successfully, otherwise we
indicate the failure with the dash symbol (-).

#### Training the large-spread ensemble

The results highlight that LSE is able to successfully train the large-spread
ensembles in the majority of the cases. In particular, training always
succeeded for the small models and only occasionally failed for larger model.
Most importantly, though, for each dataset and model size we were able to
identify values of $l$ and $MAX\\_ITER$ leading to a successful training.

When training a large large-spread ensemble, the two parameters have an impact
on the success of LSE. In particular, on the MNIST26 and Fashion-MNIST clothes
datasets, the two parameters may interact to determine the success or the
failure of the training. Given a small perturbation $k$, i.e., $k=0.005$, LSE
very often fails to train an LSE with $100$ iterations at maximum, while it
always succeeds when the maximum number of iterations is equal or above $500$.
Even when the perturbation is low, a minimum number of iterations is indeed
required to enforce the large-spread condition. When the perturbation $k$ is
high, a combination of a higher number of partitions and higher maximum number
of iterations is required to successfully train the large-spread ensemble. For
example, the training of a large large-spread ensemble on the MNIST dataset
succeeds if a number of partitions above $3$ and a maximum number of
iterations equal to $500$ is considered, while it fails without exploiting
hierarchical training for every value of $MAX\\_ITER$, i.e., when the chosen
number of subsets of features is $1$. This result highlights the benefits of
hierarchical training: training smaller large-spread ensembles on subsets of
features and then merging them can enable the training of large large-spread
ensembles, even when improving the maximum number of iterations is not
sufficient for training a large-spread ensemble without hierarchical
partitioning.

To sum up, this first analysis allowed us to catch some insights about the
influence of the value of the two parameters in the success of LSE. When the
chosen perturbation $k$ is high, the value of two parameters may need to be
sufficiently high in order to determine the success of a large large-spread
ensemble training. On the other hand, the two parameters does not seem to
significantly influence the success of training a small large-spread ensemble
or when the chosen perturbation is small.

#### Accuracy of the large-spread ensembles

In addition to the impact on the success of the LSE in training the large-
spread ensemble, it is relevant to evaluate the impact of the two parameters
on the accuracy of the trained large-spread ensemble. In the previous
analysis, we have seen that many combinations of values of the two parameters
allow LSE to successfully train a large-spread ensemble, thus the accuracy of
the large-spread ensemble may be used to select the best model to deploy in
practice.

The results in Table 5 show that only the number of subsets of partitions may
impact negatively the accuracy of the large-spread models only on the REWEMA
dataset, while it does not influence the accuracy of the large-spread
ensembles on the MNIST26 and Fashion-MNIST clothes dataset. For example, the
accuracy of a large large-spread ensemble trained on MNIST26 dataset with
perturbation $k=0.01$ and $MAX\\_ITER=100$ does not decrease as the number of
subsets of features increases, while the gap between the accuracy of the same
large-spread ensemble trained on the REWEMA with one and four subsets of
features is 0.88 and 0.81(-0.07) respectively. These results highlight that
increasing the number of subsets of features may not be a good option for
training a large-spread ensemble on some datasets, because each sub-forest has
only a partial view of the set of available features and some patterns may not
be learned. The experimental results suggest that using only one subset of
features, i.e., all the available features when training the large-spread
ensemble is the best option if it is possible.

Instead, surprisingly, the experimental results show that the maximum number
of rounds does not have an impact on the accuracy of the accuracy of the
resulting large-spread ensemble. This observation may allow us to simplify the
tuning of this parameter: if it is necessary, it is possible to consider a
higher number of iterations of the FixForest procedure (see Algorithm 3)
without harming the accuracy of the resulting large-spread ensemble.

#### Summary

The values of the number of subsets $l$ considered in hierarchical training
and the maximum number of iterations $MAX\\_ITER$ may have an impact on the
success of the LSE tool and in the accuracy of the resulting large-spread
ensemble. A combination of high values of the two parameters may be needed for
training large large-spread ensembles, but choosing a high number of subsets
of features may harm the accuracy of the large-spread ensemble. However, the
impact of the value of the two parameters is not the same for every dataset
(as with the parameters of standard training algorithms), for example, the
accuracy of the large-spread ensembles decreases by increasing the number of
subsets of features only on the REWEMA dataset. For this reason, we suggest to
perform the parameter tuning of these two parameters by using grid-search and
selecting the large-spread ensemble that shows the highest value for the
performance metric of interest, e.g., the accuracy on the test set.

Table 5. Accuracy of the large-spread ensembles trained using the LSE tool for different values of the parameters $l$ and $MAX\\_ITER$. The failure in training a large-spread ensemble of the LSE tool for a configuration of the parameters is indicated with dash (-). The large-spread ensembles are trained with norm $p=\infty$. Dataset | Trees | Depth | $k$ | $MAX\\_ITER$ | $l$
---|---|---|---|---|---
$1$ | $2$ | $3$ | $4$
FashionMNIST clothes | 25 | 4 | 0.005 | 100 | 0.91 | 0.91 | 0.91 | 0.91
500 | 0.91 | 0.91 | 0.91 | 0.91
1000 | 0.91 | 0.91 | 0.91 | 0.91
0.01 | 100 | 0.91 | 0.91 | 0.91 | 0.90
500 | 0.91 | 0.91 | 0.91 | 0.90
1000 | 0.91 | 0.91 | 0.91 | 0.90
0.015 | 100 | 0.91 | 0.91 | 0.91 | 0.90
500 | 0.91 | 0.91 | 0.91 | 0.90
1000 | 0.91 | 0.91 | 0.91 | 0.90
101 | 6 | 0.05 | 100 | - | - | - | 0.93
500 | 0.95 | 0.94 | 0.94 | 0.92
1000 | 0.95 | 0.94 | 0.94 | 0.92
0.01 | 100 | - | - | - | -
500 | 0.93 | 0.93 | 0.93 | 0.92
1000 | 0.93 | 0.93 | 0.93 | 0.92
0.015 | 100 | - | - | - | -
500 | - | - | 0.90 | 0.91
1000 | - | - | 0.90 | 0.91
MNIST26 | 25 | 4 | 0.005 | 100 | 0.98 | 0.97 | 0.97 | 0.97
500 | 0.98 | 0.97 | 0.97 | 0.97
1000 | 0.98 | 0.97 | 0.97 | 0.97
0.01 | 100 | 0.98 | 0.97 | 0.97 | 0.97
500 | 0.98 | 0.97 | 0.97 | 0.97
1000 | 0.98 | 0.97 | 0.97 | 0.97
0.015 | 100 | 0.98 | 0.97 | 0.97 | 0.97
500 | 0.98 | 0.97 | 0.97 | 0.97
1000 | 0.98 | 0.97 | 0.97 | 0.97
101 | 6 | 0.05 | 100 | - | - | - | -
500 | 0.99 | 0.99 | 0.99 | 0.99
1000 | 0.99 | 0.99 | 0.99 | 0.99
0.01 | 100 | - | - | - | 0.99
500 | - | 0.99 | 0.99 | 0.99
1000 | - | 0.99 | 0.99 | 0.99
0.015 | 100 | - | - | - | -
500 | - | - | - | 0.91
1000 | - | - | - | 0.90
REWEMA | 25 | 4 | 0.005 | 100 | 0.87 | 0.8 | 0.8 | 0.79
500 | 0.87 | 0.8 | 0.8 | 0.79
1000 | 0.87 | 0.8 | 0.8 | 0.79
0.01 | 100 | 0.89 | 0.79 | 0.79 | 0.81
500 | 0.89 | 0.79 | 0.79 | 0.81
1000 | 0.89 | 0.79 | 0.79 | 0.81
0.015 | 100 | 0.88 | 0.82 | 0.79 | 0.81
500 | 0.88 | 0.82 | 0.79 | 0.81
1000 | 0.88 | 0.82 | 0.79 | 0.81
101 | 6 | 0.05 | 100 | 0.88 | 0.89 | 0.88 | 0.84
500 | 0.89 | 0.88 | 0.88 | 0.85
1000 | 0.89 | 0.88 | 0.88 | 0.86
0.01 | 100 | 0.88 | 0.88 | 0.87 | 0.81
500 | 0.88 | 0.87 | 0.87 | 0.81
1000 | 0.88 | 0.87 | 0.87 | 0.80
0.015 | 100 | 0.86 | 0.87 | 0.86 | 0.80
500 | 0.86 | 0.86 | 0.86 | 0.80
1000 | 0.86 | 0.87 | 0.86 | 0.80