Exact and Cost-Effective Automated Transformation of Neural Network
  Controllers to Decision Tree Controllers
Over the past decade, neural network (NN)-based controllers have demonstrated
remarkable efficacy in a variety of decision-making tasks. However, their
black-box nature and the risk of unexpected behaviors and surprising results
pose a challenge to their deployment in real-world systems with strong
guarantees of correctness and safety. We address these limitations by
investigating the transformation of NN-based controllers into equivalent soft
decision tree (SDT)-based controllers and its impact on verifiability.
Differently from previous approaches, we focus on discrete-output NN
controllers including rectified linear unit (ReLU) activation functions as well
as argmax operations. We then devise an exact but cost-effective transformation
algorithm, in that it can automatically prune redundant branches. We evaluate
our approach using two benchmarks from the OpenAI Gym environment. Our results
indicate that the SDT transformation can benefit formal verification, showing
runtime improvements of up to 21x and 2x for MountainCar-v0 and CartPole-v0,
respectively.
Kevin Chang, Nathan Dahlin, Rahul Jain, Pierluigi Nuzzo
Exact and Cost-Effective Automated Transformation of Neural Network Controllers to Decision Tree Controllers

###### Abstract

Over the past decade, neural network (NN)-based controllers have demonstrated remarkable efficacy in a variety of decision-making tasks. However, their black-box nature and the risk of unexpected behaviors and surprising results pose a challenge to their deployment in real-world systems with strong guarantees of correctness and safety. We address these limitations by investigating the transformation of NN-based controllers into equivalent soft decision tree (SDT)-based controllers and its impact on verifiability. Differently from previous approaches, we focus on discrete-output NN controllers including rectified linear unit (ReLU) activation functions as well as argmax operations. We then devise an exact but cost-effective transformation algorithm, in that it can automatically prune redundant branches. We evaluate our approach using two benchmarks from the OpenAI Gym environment. Our results indicate that the SDT transformation can benefit formal verification, showing runtime improvements of up to \(21\times\) and \(2\times\) for MountainCar-v0 and CartPole-v0, respectively.

## I Introduction

Over the last decade, neural network (NN)-based techniques [1] have exhibited outstanding efficacy in a variety of decision-making tasks, surpassing human-level performance in some of the most challenging control problems. They even lead the leaderboard in almost all benchmark problems in control and robotics. However, their deployment in safety-critical applications, such as autonomous driving and flight control, raises concerns [2, 3] due to the black-box nature of NNs and the risk of unexpected behaviors.

To overcome the limitations of NN-based controllers, researchers have proposed distillation [4], which transfers the learned knowledge and behaviors of NN controllers to alternative models, such as decision trees, which are easier to interpret. In fact, the efficacy of NN controllers versus other models is not necessarily due to their richer representative capacity, but rather to the many regularization techniques available to facilitate training [5, 6]. By compressing NN controllers into simpler and more compact models, distillation can also facilitate formal verification. However, the distilled models typically fall short of the real-time performance of their full counterparts. In fact, identification of effective metrics to characterize the approximation quality of a distilled model versus the original NN is itself an open problem.

In this paper, we focus instead on the _exact, systematic transformation_ of NN-based controllers into equivalent soft decision tree (SDT)-based controllers and the empirical evaluation of the impact of this transformation on the verifiability of the controllers. The equivalent SDT models can be used for verification, while the NN models are used at runtime. Moreover, unlike prior work, we consider discrete-output NN controllers with rectified linear unit (ReLU) activation functions and argmax operations. These discrete-action NNs are particularly challenging from a verification standpoint, in that they tend to amplify the approximation errors generated by reachability analysis of the closed-loop control system. Our contributions can be stated as follows:

* We first prove that any discrete-output argmax-based NN controller has an _equivalent_ SDT. This is done by presenting a constructive procedure to transform any NN controller into an equivalent SDT controller that has the same properties.
* We show that our constructive procedure for creating an equivalent SDT controller can also be computationally practical, in that the number of nodes in the SDT scales polynomially with the maximum width of the hidden layers in the NN. To the best of our knowledge, this is the first such computationally practical transformation algorithm.
* We empirically validate the computational efficiency of formally verifying the SDT controller over the original NN controller on two benchmark OpenAI Gym environments [7], showing that verifying the SDT controller is 21 times as fast on the MountainCar-v0 environment and twice as fast on the CartPole-v0 environment.

Our results suggest that SDT transformation can be used to accelerate the verification of NN controllers in feedback control loops, with potential impact on applications where performance guarantees are critical but deep learning methods are the primary choice for control design.

Related Work. Distillation [4] has been used to transfer the knowledge and behavior of NN-based controllers to other models in an approximate, e.g., data-driven, or exact manner. _Approximate distillation_ can be performed by training shallow NNs to mimic the behavior of state-of-the-art NNs using a teacher-student paradigm [5]. Distilling SDTs from expert NNs was shown to lead to better performance than directly training SDTs [4]. Furthermore, distillation has demonstrated success in reinforcement learning (RL) problems, where the DAGGER algorithm is used to transfer knowledge from Q-value NN models via simulation episodes [8]. Finally, distilling to SDTs has also been suggested to interpret the internal workings of black-box NNs [9].

In contrast, _exact distillation_ has been proposed to transform feedforward NNs into simpler models while preserving equivalence [10, 11, 12]. Locally constant networks [10] and linear networks [11] have been introduced as intermediate representations to establish the equivalence between NNs and SDTs whose worst-case size scales exponentially in the maximum width of the NN hidden layers. Nguyen et al. [12] proposed transforming NNs with ReLUs into decision trees and then compressing the trees via a learning-based approach. As in previous approaches, our algorithm preserves equivalence with the SDTs. However, it also guarantees, without the need for compression, that the size of the tree scales polynomially in the width of the maximum hidden
layer of the NN. Finally, we also provide quantitative evidence about the impact of the proposed transformations on the verifiability of the controllers.

## II Preliminaries

We review key definitions for both neural networks (NN) and soft decision trees (SDT), using Fig. 1 as an illustrative example. Throughout the paper, we use \(A_{i,j}\) to denote the element in the \(i\)-th row and \(j\)-th column of matrix \(A\), and \(a_{i}\) or \((a)_{i}\) to denote the \(i\)-th element of vector \(a\).

#### Ii-1 Neural Networks

Let \(L\) denote the total number of layers in a NN, \(N^{l}\) denote the _width_, or number of neurons in the \(l\)-th layer, and define \(N:=(N_{1},\ldots,N_{L})\). In Fig. (a)a, we have \(L=3\), with a two-neuron input layer (\(N^{1}=2\)), a single-neuron hidden layer (\(N^{2}=1\)), and a three-neuron output layer (\(N^{3}=3\)), so that \(N=(2,1,3)\). The nodes in layer \(l\), with \(l>1\), are fully connected to the previous layer. Edges and nodes are associated with weights and biases, denoted by \(W^{l}\) and \(B^{l}\), respectively, for \(l\geq 2\). The output at each neuron is determined by its inputs using a _feedforward function_, defined below, and then passed through a rectified linear unit (ReLU) _activation function_.

**Definition 1**: _(NN Layer Feedforward Function). Given input \(x\in\mathbb{R}^{N^{l-1}}\), the feedforward function \(f_{F}^{l}:\mathbb{R}^{N^{l-1}}\rightarrow\mathbb{R}^{N^{l}}\) maps \(x\) to the output of layer \(l\geq 2\), where the output of the \(i\)-th neuron in layer \(l\) is defined as_

\[(f_{F}^{l}(x))_{i}:=\sum_{i=1}^{N^{l-1}}W_{i,j}^{l}x_{j}+B_{i}^{l}.\]

We also recall the definition of _characteristic function_. Let \(\alpha\) be the element-wise ReLU activation function, i.e., \(\alpha(x)_{i}=\max\{x_{i},0\}\).

**Definition 2**: _(NN Layer-Characteristic Function). The characteristic function for layer \(l\) of NN \(\mathcal{N}\), \(f_{\mathcal{N}}^{l}:\mathbb{R}^{N^{1}}\rightarrow\mathbb{R}^{N^{l}}\), is defined as_

\[f_{\mathcal{N}}^{l}(x):=f_{F}^{l}\circ\alpha\circ f_{F}^{l-1}\circ\cdots\circ f _{F}^{3}\circ\alpha\circ f_{F}^{2}(x).\]

**Definition 3**: _(NN Characteristic Function). The characteristic function of NN \(\mathcal{N}\), \(f_{\mathcal{N}}:\mathbb{R}^{N^{1}}\rightarrow\mathbb{N}\), is defined as_

\[f_{\mathcal{N}}(x):=\operatorname*{arg\,max}_{i\in\{1,\ldots,N^{L}\}}\{(f_{ \mathcal{N}}^{L})_{i}:i\in\{1,\ldots,N^{L}\}\}. \tag{1}\]

In Definition 3, we assume that when \(\operatorname*{arg\,max}(.)\) is not a singleton, a deterministic tie-breaking procedure is used to select a single index.

#### Ii-2 Soft Decision Trees

We consider a binary SDT [9]. Let \(\mathcal{I}_{\mathcal{S}}\) and \(\mathcal{L}_{\mathcal{S}}\) denote the sets of inner and leaf nodes for an SDT \(\mathcal{S}\) with input dimension \(n\). Each inner node \(v\in\mathcal{I}\) is associated with weights \(w^{v}\in\mathbb{R}^{n}\) and a bias term \(b^{v}\in\mathbb{R}\). At node \(v\), \(w^{v}\) and \(b^{v}\) are applied to input \(x\). The resulting value is passed through an activation function \(\sigma\), producing a scalar, \(p_{v}(x)=\sigma(x^{\top}w^{v}+b^{v})\), which is compared to a threshold to determine whether to proceed to the left or right branch. In this paper, we consider SDTs using the sigmoid logistic activation function \(\sigma(y)=\frac{1}{1+e^{-y}}\) at all nodes.

Each leaf node \(v\in\mathcal{L}\) is associated with a vector \(Q^{v}\). In general, \(Q^{v}\) is a distribution over possible output selections. In our SDTs, the elements of \(Q^{v}\) will take values in \(\{0,1\}\). Rather than learning the parameters \((w^{v},b^{v})\) or \(Q^{v}\) for each node \(v\) from data as in the literature [9], we derive these parameters via transformation of a reference NN. We denote the left and right child of an inner node \(v\) as \(l(v)\) and \(r(v)\), respectively, and the parent of \(v\) as \(\rho(v)\). The root node of the SDT is \(v_{0}\). We now define the SDT characteristic functions.

**Definition 4**: _(SDT Node Characteristic Function). Let \(\mathcal{S}\) be an SDT with input dimension \(n\). Given input vectors \(x\in\mathbb{R}^{n}\), the characteristic function of node \(v\), \(f_{\mathcal{S}}^{v}:\mathbb{R}^{n}\rightarrow\mathbb{N}\), is defined recursively as_

\[f_{\mathcal{S}}^{v}(x)=\left\{\begin{array}{cl}\operatorname*{arg\,max}_{k }\{Q_{k}^{v}\},&\text{if }v\in\mathcal{L}_{\mathcal{S}},\\ f_{\mathcal{S}}^{l(v)}(x),&\text{if }v\in\mathcal{I}_{\mathcal{S}}\wedge p_{v}(x) \leq 0.5,\\ f_{\mathcal{S}}^{r(v)}(x),&\text{if }v\in\mathcal{I}_{\mathcal{S}}\wedge p_{v}(x) >0.5.\end{array}\right.\]

**Definition 5**: _(SDT Characteristic Function). The characteristic function of SDT \(\mathcal{S}\) with input dimension \(n\), \(f_{\mathcal{S}}:\mathbb{R}^{n}\rightarrow\mathbb{N}\), is defined as \(f_{\mathcal{S}}(x):=f_{\mathcal{S}}^{v_{0}}(x)\)._

Throughout this work, we assume that NNs and SDTs use the same deterministic argmax-based tie-breaking procedure.

We further introduce the notation \(\mathcal{D}(v)\) to represent the effective _domain_ of an SDT node \(v\), i.e., the set of all possible inputs arriving at \(v\). The set \(\mathcal{D}(v)\) is computed recursively in a top-down manner from the root node as follows

\[\mathcal{D}(v)=\left\{\begin{array}{ll}\mathbb{R}^{n},&\text{if }v=v_{0},\\ \mathcal{D}(\rho(v))\cap&\text{if }v\neq v_{0}\wedge\\ \{x|p_{\rho(v)}(x)\leq 0.5\},&\text{ }l(\rho(v))=v,\\ \mathcal{D}(\rho(v))\cap&\text{if }v\neq v_{0}\wedge\\ \{x|p_{\rho(v)}(x)>0.5\},&\text{ }r(\rho(v))=v,\end{array}\right. \tag{2}\]

where \(n\) is the input dimension of the SDT.

For example, for the SDT in Fig. (b)b, the inputs \(x=(x_{0},x_{1})^{\top}\in\mathbb{R}^{2}\) are processed starting from the root node

Fig. 1: Example NN to SDT Transformation.
\(v_{0}\), where \(\mathcal{D}(v_{0})=\mathbb{R}^{2}\). The input range related to node \(v_{1}\) is \(\mathcal{D}(v_{1})=\{x\in\mathbb{R}^{2}|x_{1}\leq 0\}\) and \(v_{1}\) is reached only if \(x_{1}\leq 0\). Similarly, node \(v_{2}\) is reached when \(x_{1}\geq 0\), i.e., \(\mathcal{D}(v_{2})=\{x\in\mathbb{R}^{2}|x_{1}\geq 0\}\). In the remainder of the paper, we omit the reference to the underlying state-space in the expressions for the node input domains, when it is clear from the context, and simply write, e.g., \(\mathcal{D}(v_{1})=\{x_{1}\leq 0\}\) and \(\mathcal{D}(v_{2})=\{x_{1}>0\}\).

## III Transformation from Neural Network to Decision Tree

We present an algorithm for constructing an SDT \(\mathcal{S}_{\mathcal{N}}\) which is equivalent to a reference NN \(\mathcal{N}\) in the sense that \(f_{\mathcal{N}}(x)=f_{\mathcal{S}_{\mathcal{N}}}(x)\) for all inputs \(x\in\mathbb{R}^{n}\). We outline the relation between fully connected NNs with ReLU activation and argmax output and SDTs based on our transformation in Fig. 1.

In the NN of Fig. (a)a, the output of the single neuron in layer 2 following the ReLU activation is

\[\alpha(f_{\mathcal{N}}^{2}(x))=\alpha\left(W^{2}x+B^{2}\right)=\alpha(x_{1})= \begin{cases}0,&\text{if }x_{1}\leq 0,\\ x_{1},&\text{if }x_{1}>0.\end{cases} \tag{3}\]

Carrying these two cases forward through the output layer \(L=3\), we have

\[f_{\mathcal{N}}^{L}(x)=\begin{cases}B^{L}&=(0.001,\,0,\,0)^{\top},\quad\text{ if }x_{1}\leq 0,\\ W^{L}x_{1}+B^{L}&=(0.001,\,0,\,x_{1})^{\top},\quad\text{if }x_{1}>0.\end{cases} \tag{4}\]

Thus, when \(x_{1}\leq 0\), we have

\[f_{\mathcal{N}}(x)=\operatorname*{arg\,max}_{i\in\{1,\ldots,N^{L}\}}\{(f_{ \mathcal{N}}^{L}(x))_{i}\}=1,\]

while when \(x_{1}>0\), we have

\[f_{\mathcal{N}}(x)=\begin{cases}1,&\text{if }x_{1}\leq 0.001,\\ 3,&\text{if }x_{1}>0.001,\end{cases} \tag{5}\]

assuming we take the lowest index to break ties.

Turning to the SDT in Fig. (b)b, we observe that (3) partitions the input space into two subsets based on the inner node's ReLU activation. This is precisely the split that occurs at the root node \(v_{0}\) of the SDT toward nodes \(v_{1}\) and \(v_{2}\). Then, (5) further splits one of these subsets based on the output layer values. This split occurs at \(v_{2}\) to provide nodes \(v_{3}\) and \(v_{4}\). Finally, we have three regions where \(f_{\mathcal{N}}(x)\) is constant, corresponding to leaf nodes \(v_{1}\), \(v_{3}\), and \(v_{4}\) in Fig. (b)b.

As shown in (3)-(5) for subsets of the NN input space, based on the sequence of ReLU activations, \(f_{\mathcal{N}}^{L}(x)\) is an affine function. Such subsets may be further partitioned based on the argmax operation. Therefore, the operation of fully connected NNs with ReLU activations and argmax output can be understood in terms of successive assignment of inputs to increasingly refined partitions of the state space, which can be shown to consist of convex polyhedra [10]. Identification of SDT splits and leaf node assignments based upon NN neuron activations and output layer outputs forms the core of our transformation technique, which we explain further in the remainder of this section. See Appendix A for an application of the transformation to the example in Fig. 1.

### _Pre and Post-Activation Formulas_

We establish the relationship between \(\mathcal{N}\) and \(\mathcal{S}_{\mathcal{N}}\) by first introducing, for each node \(v\), a _pre-activation function_\(\mathcal{F}_{i}^{l}\llbracket v\rrbracket:\,\mathcal{D}(v)\to\mathbb{R}\) and a _post-activation function_\(\overline{\mathcal{F}_{i}^{l}\llbracket v\rrbracket}:\mathcal{D}(v)\to \mathbb{R}\). The pre-activation function provides the output of the \(i\)-th neuron in the \(l\)-th layer of \(\mathcal{N}\) as a function of the input in \(\mathcal{D}(v)\) prior to the ReLU. The _post-activation function_ gives the neuron output after the ReLU. The pre-activation functions for node \(v\) are defined for \(l=2,\ldots,L\) and \(i=1,\ldots,N^{l}\) as

\[\mathcal{F}_{i}^{l}\llbracket v\rrbracket(x)=\\ \begin{cases}\sum_{j=1}^{N^{l}_{1}}W_{i,j}^{l}x_{j}+B_{i}^{l},&\text{if }l=2,\\ \sum_{j=1}^{N^{l-1}_{1}}W_{i,j}^{l}\overline{\mathcal{F}_{j}^{l-1}\llbracket v \rrbracket}(x)+B_{i}^{l},&\text{if }l>2\wedge\overline{\mathcal{F}_{j}^{l-1} \llbracket v\rrbracket}(x)\neq\bot\\ &\text{for }j=1,2,\ldots,N^{l-1},\\ \bot,&\text{otherwise}.\end{cases} \tag{6}\]

Here, \(\bot\) denotes an undefined value. The post-activation functions for node \(v\) are defined for \(l=2,\ldots,L-1\) and \(i=1,\ldots,N^{l}\) as

\[\overline{\mathcal{F}_{i}^{l}\llbracket v\rrbracket}(x)=\begin{cases}\mathcal{F} _{i}^{l}\llbracket v\rrbracket(x),&\text{if }\mathcal{F}_{i}^{l}\llbracket v\rrbracket\neq\bot\wedge\\ &\mathcal{D}(v)\cap\{\mathcal{F}_{i}^{l}\llbracket v\rrbracket(x)\leq 0\}=\emptyset,\\ 0,&\text{if }\mathcal{F}_{i}^{l}\llbracket v\rrbracket\neq\bot\wedge\\ &\mathcal{D}(v)\cap\{\mathcal{F}_{i}^{l}\llbracket v\rrbracket(x)>0\}=\emptyset,\\ \bot,&\text{otherwise}.\end{cases} \tag{7}\]

We define \(\mathcal{F}^{l}\llbracket v\rrbracket:=(\mathcal{F}_{1}^{l}\llbracket v \rrbracket,\ldots,\mathcal{F}_{N^{l}}^{l}\llbracket v\rrbracket)^{\top}\) and \(\overline{\mathcal{F}^{l}\llbracket v\rrbracket}\) similarly for all \(l=2,\ldots,L\). The pre-activation formulas play a crucial role in determining the pre-threshold branching functions \(p_{v}\) at each inner node \(v\) of \(\mathcal{S}\).

### _SDT Split and Leaf Formation Rules_

We construct the branches of \(\mathcal{S}_{\mathcal{N}}\) based on the rules in Table I. By starting with the root node \(v_{0}\), for each node

\begin{table}
\begin{tabular}{c|c|c}
**Rules** & **Conditions** & **Computation of \(p_{v}(x)\) or \(Q^{v}\)** \\ \hline
1. Split based on ReLU & \(\exists\;i,l<L\) s.t. \(\mathcal{D}(v)\cap\{\mathcal{F}_{i}^{l}\llbracket v\rrbracket(x)\leq 0\}\neq\emptyset\wedge\) & \(p_{v}(x)=\left\{\begin{array}{ll}\sigma(\mathcal{F}_{i}^{l}\llbracket v \rrbracket(x))\\ \text{for }\min\;i,l\text{ such that Rule 1 conditions hold }\\ \end{array}\right.\) \\ \hline
2. Split based on output layer & \(\begin{array}{l}\mathcal{D}(v)\cap\bigcap_{v^{\prime}\neq i_{1}}\{F_{i_{1}}^{L} \llbracket v\rrbracket(x)\geq\mathcal{F}_{i_{1}}^{L}\llbracket v\rrbracket(x)\} \neq\emptyset\wedge\\ \mathcal{D}(v)\cap\bigcap_{v^{\prime}\neq i_{2}}\{F_{i_{2}}^{L}\llbracket v \rrbracket(x)\geq\mathcal{F}_{i_{1}^{L}}^{L}\llbracket v\rrbracket(x)\} \neq\emptyset\end{array}\) & \(p_{v}(x)=\sigma(\mathcal{F}_{i_{1}}^{L}\llbracket v\rrbracket(x)-\mathcal{F}_{i_{2} }^{L}\llbracket v\rrbracket(x))\) \\ \hline
3. Form leaf node & Neither Rule 1 nor Rule 2 satisfied & \(Q_{i}^{v}=\left\{\begin{array}{ll}1&\text{if }i=\operatorname*{arg\,max}_{k}\{\mathcal{F}_{k}^{L} \llbracket v\rrbracket(x)\}\;\forall x\in\mathcal{D}(v)\\ 0&\text{otherwise}\end{array}\right.\) \\ \end{tabular}
\end{table} TABLE I: Rules for constructing an SDT node \(v\).
in \(\mathcal{S}_{\mathcal{N}}\), we use Table I to obtain \(p_{v}(x)\) or \(Q^{v}\) in a top-down fashion from the root to leaves, as further explained below.

**Rule 1.** If there exists a neuron \(i\) in layer \(l\) of \(\mathcal{N}\) such that \(D_{0}:=\mathcal{D}(v)\cap\{\alpha(\mathcal{F}_{i}^{l}[\![v]\!](x))=0\}\neq\emptyset\) and \(D_{1}:=\mathcal{D}(v)\cap\{\alpha(\mathcal{F}_{i}^{l}[\![v]\!](x))>0\}\neq\emptyset\) hold, we form a split at node \(v\) in \(\mathcal{S}_{\mathcal{N}}\). \(\mathcal{D}(v)\) is then partitioned along the hyperplane \(\mathcal{F}_{i}^{l}[\![v]\!](x)=0\), with \(\mathcal{D}(l(v))=D_{0}\) and \(\mathcal{D}(r(v))=D_{1}\). For example, for node \(v_{0}\) in Fig. 0(b), we create a split at \(v_{0}\) with \(p_{v_{0}}(x)=\sigma(\mathcal{F}_{1}^{l}[\![v_{0}]\!](x))\).

**Rule 2.** Suppose no partitions can be found for \(\mathcal{D}(v)\) based on the ReLUs according to Rule 1. Then, \(\mathcal{D}(v)\) may be further partitioned based on the output layer values. If there exist \(i_{1}\) and \(i_{2}\) and sets \(D_{i_{1}}:=\{x\in\mathcal{D}(v)\big{|}\arg\max_{i}\{\big{(}\mathcal{F}^{L}[\! [v]\!](x)\big{)}_{i}=i_{1}\}\neq\emptyset\) and \(D_{i_{2}}:=\{x\in\mathcal{D}(v)\big{|}\arg\max_{i}\{\big{(}\mathcal{F}^{L}[\! [v]\!](x)\big{)}_{i}\}=i_{2}\}\neq\emptyset\), we form a split at node \(v\). \(\mathcal{D}(v)\) is then partitioned along the hyperplane \(\mathcal{F}_{i_{2}}^{L}[\![v]\!](x)-\mathcal{F}_{i_{1}}^{L}[\![v]\!](x)=0\), giving \(D_{i_{1}}\subseteq\mathcal{D}(l(v))\) and \(D_{i_{2}}\subseteq\mathcal{D}(r(v))\). For example, for node \(v_{2}\) in Fig. 0(b), we create a split at \(v_{2}\) and set \(p_{v_{2}}(x)\) as \(\sigma(\mathcal{F}_{1}^{l}[\![v_{2}]\!](x)-\mathcal{F}_{3}^{l}[\![v_{2}]\!](x))\).

**Rule 3.** If neither Rule 1 nor Rule 2 can be applied to further partition \(\mathcal{D}(v)\), then the index of the neuron with the maximum output at layer \(L\), i.e., the outcome of the \(\arg\max\) operator remains constant over the entire set \(\mathcal{D}(v)\). We then declare \(v\) as a leaf node, setting \(Q_{i}^{v}=1\) for the neuron index corresponding to the largest output, and \(0\) otherwise. For example, for node \(v_{1}\) in Fig. 0(b) we set \(Q_{1}^{v_{1}}(x)=1\) and \(Q_{2}^{v_{1}}(x)=Q_{3}^{v_{1}}(x)=0\).

The conditions above, such as non-emptiness of \(\mathcal{D}(v)\cap\{\alpha(\mathcal{F}_{i}^{l}[\![v]\!](x))=0\}\) in Rule 1, can be formulated and efficiently solved in terms of feasibility problems for LPs.

### _Transformation Procedure_

We construct \(\mathcal{S}_{\mathcal{N}}\) by starting with the root node \(v_{0}\) and building the binary tree downwards. We first construct the left-hand branches until a leaf node is discovered, from which we backtrack the tree to define the unexplored right branches. A recursive method implementing this procedure is presented in Algorithm 1. The transformation procedure effectively identifies a partition of the input space according to the domains associated with the leaf nodes of the SDT. Within these sets, the neural network characteristic function \(f_{\mathcal{N}}\) is constant, and due to our choice of \(Q^{v}\) at each leaf node \(v\), we have that \(f_{\mathcal{N}}(x)=f_{\mathcal{S}_{\mathcal{N}}}(x)\) over \(\mathcal{D}(v)\). Taking a union over the SDT partitions, we establish the equivalence of \(\mathcal{N}\) and \(\mathcal{S}_{\mathcal{N}}\) in Theorem 1. As detailed in Appendix B, Theorem 1 can be proved by induction on layer \(l\) to show that \(\mathcal{F}^{L}[\![v]\!](x)=f_{\mathcal{N}}^{L}(x)\) for leaf nodes nodes \(v\in\mathcal{L}_{\mathcal{S}_{\mathcal{N}}}\).

**Theorem 1**: _For a given NN \(\mathcal{N}\) and its SDT transformation \(\mathcal{S}_{\mathcal{N}}\) using Algorithm 1 with input space \(\mathbb{R}^{n}\), the corresponding characteristic functions are pointwise equal, i.e., \(f_{\mathcal{N}}(x)=f_{\mathcal{S}_{\mathcal{N}}}(x)\) for all \(x\in\mathbb{R}^{n}\)._

Differently from previous algorithms in the literature [10, 11, 12], our algorithm only generates essential branches during the creation of the SDT. Given the NN input and output layer sizes and the number of hidden layers, the SDT size scales polynomially in the maximum hidden layer width. The size complexity of \(\mathcal{S}_{\mathcal{N}}\) in terms of the number of nodes is stated in Theorem 2, whose proof is provided in Appendix C.

**Theorem 2**: _Let \(\mathcal{N}\) be a NN and \(\mathcal{S}_{\mathcal{N}}\) the SDT resulting from the application of Algorithm 1 to \(\mathcal{N}\). Denote the number of nodes in \(\mathcal{S}_{\mathcal{N}}\) by \(|\mathcal{S}_{\mathcal{N}}|\). Then, we obtain_

\[|\mathcal{S}_{\mathcal{N}}|=O\left(\prod_{l=2}^{L-1}\frac{(N^{l})^{(N^{1})}}{(N ^{1})!}2^{N^{L}}\right)=O\left(\frac{2^{N^{L}}}{(N^{1}!)}\mathcal{I}^{N^{1}L }\right),\]

_where \(\mathcal{I}:=\max_{l\in\{2,\dots,L-1\}}N^{l}\)._

## IV Verification Formulation

We describe the verification problems that we solve to evaluate the impact of the proposed transformation. We consider closed-loop controlled dynamical systems with state and action spaces \(\mathcal{X}\) and \(\mathcal{U}\), respectively, and dynamics \(h:\mathcal{X}\times\mathcal{U}\rightarrow\mathcal{X}\). Let \(\pi:\mathcal{X}\rightarrow\mathcal{U}\) denote a time-invariant Markovian policy (controller) mapping states to actions. Given a system dynamics \(h\), an initial set \(\mathcal{X}_{i}\), and goal set \(\mathcal{X}_{g}\), we wish to determine whether \(\mathcal{X}_{g}\) is reachable in finite horizon \(T\) for all initial states \(x_{0}\in\mathcal{X}_{i}\), under \(h\) and policy \(\pi\). If so, we say that the specification \((\mathcal{X}_{i},\mathcal{X}_{g},T)\) is verified for \(\pi\). In this context, we consider two verification approaches.

**Problem 1**: _(One-Shot Verification)._ We "unroll" the system dynamics at time instant \(t\in\{0,\dots,T\}\) and encode the verification problem to a satisfiability modulo theory (SMT) problem [13] using the bounded model checking approach [14]. Verification of \((\mathcal{X}_{i},\mathcal{X}_{g},T)\) for a policy \(\pi\) is then equivalent to showing that the following formula is _not_ satisfiable:

\[\phi_{1}(\pi):=(\mathcal{X}_{i})\wedge(\overline{\mathcal{X}_{g}})\bigwedge_{t=0} ^{T-1}(x_{t+1}=h(x_{t},u_{t}))\wedge(u_{t}=\pi(x_{t})). \tag{8}\]

If \(\phi_{1}(\pi)\) is false, then \(\pi\) is guaranteed to drive the system from any \(x_{0}\in\mathcal{X}_{i}\) to \(\mathcal{X}_{g}\) within the finite horizon \(T\).

We observe that (8) requires encoding \(T\) replicas of the NN (policy \(\pi\)) in the control loop, which can make the SMT problem intractable due to its computational complexity. Therefore, we also consider an alternative verification approach via reachability analysis. In particular, we adopt a _recursive reachability analysis_[15], where we use the \(s\)-step unrolled dynamics, with \(s\ll T\), to compute an over-approximation of the \(s\)-step reachable set in terms of a rectangle.
**Problem 2**: _(Recursive Reachability Analysis (RRA)._ We fix a step parameter \(s\) and recursively compute reachable sets \(\mathcal{R}_{t}\), where \(t=ms\) for \(m\in\mathbb{N}\). Given a system dynamics \(h\), policy \(\pi\) and step parameter \(s\), we encode the reachable set at time \(t\) as the SMT formula

\[\begin{split}\mathcal{R}_{t}(\pi)&=\bigg{\{}x \bigg{|}x=x_{t}\wedge(\mathcal{R}_{t-s})\wedge\\ &\qquad\bigwedge_{k=t-s}^{t-1}(x_{k+1}=h(x_{k},u_{k}))\wedge(u_{k }=\pi(x_{k}))\bigg{\}}.\end{split} \tag{9}\]

By setting \(\mathcal{R}_{0}=\mathcal{X}_{i}\), we can verify the specification \((\mathcal{X}_{i},\mathcal{X}_{g},T)\) by checking satisfaction of the following SMT formula

\[\phi_{\text{RRA}}(\pi):=(\mathcal{X}_{i})\wedge(\overline{\mathcal{X}_{g}}) \wedge\bigcup_{m=1}^{[T/s]}\mathcal{R}_{ms}(\pi). \tag{10}\]

While RRA may yield overly conservative reachable sets due to error propagation, it is often more tractable than direct one-shot verification [15], since it decomposes the overall reachability problem into a set of smaller sub-problems, each having a finite horizon of \(s\) and encoding the NN policy only \(s\) times, with \(s\ll T\).

## V Case Studies

### _The Environments_

#### V-A1 MountainCar-v0

In the MountainCar control task [16], an underpowered car needs to reach the top of a hill starting from a valley within a fixed time horizon \(T\). The state vector \(x_{t}\in\mathbb{R}^{2}\) comprises the car's position \(x_{t,0}\) and horizontal velocity \(x_{t,1}\) at time step \(t\), while the input \(u_{t}\in\{-1,0,1\}\) represent the car's acceleration action, either left (L), idle (I), or right (R), respectively. The system dynamics are given in Appendix D.

While the reference NNs are trained to reach the top of the hill \((x\geq\mathfrak{g})\) in the minimum number of steps, we seek to verify whether a given controller will reach the goal state within \(T\) steps, starting from any point in an initial interval. Our specification \((\mathcal{X}_{i},\mathcal{X}_{g},T)\) is given by

\[\mathcal{X}_{i}=\{x_{0}\in[\text{i},\text{i}_{u}],x_{1}=0\},\ \mathcal{X}_{g}=\bigcup_{t=0}^{T}\{x_{t,0}\geq\mathfrak{g}\},\]

where \(\text{i}_{l}\), \(\text{i}_{u}\), and \(\mathfrak{g}\) are parameters.

#### V-A2 CartPole-v0

In the CartPole control task [17], a pole is attached to a cart moving along a frictionless track, to be balanced upright for as long as possible within a fixed horizon \(T\). The state vector \(x_{t}\in\mathbb{R}^{4}\) consists of the cart position \(x_{t,0}\), the cart velocity \(x_{t,1}\), the pole angle \(x_{t,2}=\theta_{t}\), and the pole angular velocity \(x_{t,3}\) at time step \(t\). The input \(u_{t}\in\{0,1\}\) denotes the acceleration of the cart to the left or right. The system dynamics are given in Appendix E.

We seek to verify that the pole is balanced upright within tolerance \(\mathfrak{g}\) at the end of horizon \(T\), starting from a range of initial cart positions and pole angles. With \(\text{i}_{l}\), \(\mathfrak{g}\) as parameters, our specification \((\mathcal{X}_{i},\mathcal{X}_{g},T)\) is given by

\[\begin{split}\mathcal{X}_{i}&=\{x_{0,0}\in[\text {i}_{l},0],x_{0,2}\in[\text{i}_{l},0],x_{0,1}=x_{0,3}=0\}\\ \mathcal{X}_{g}&=\{|x_{T,2}|\geq\mathfrak{g}\}. \end{split} \tag{11}\]

### _Evaluation Results_

We adopt the problem setups available in the open-source package OpenAI Gym [7] and the parameters in Table II. We start by training NN controllers for \(1e7\) steps and then apply our transformation to construct equivalent SDTs. Figure 2 illustrates the average score, transformation time, and number of leaves of the SDT for each NN controller. We also display the estimated number of leaves under a naive transformation method that generates a split at every node for every neuron in every layer, denoted by "w/o branch removal". This value signifies the percentage reduction in size achieved by our transformation. As shown in Fig. 2, the percentage of size reduction for the SDT increases with the number of NN layers. Furthermore, the size of the transformed SDT for the CartPole problem increases faster than for the MountainCar problem, which can be attributed to the difference in \(N^{1}=|x_{t}|\). Nevertheless, we were able to transform all NN controllers in less than \(60\) seconds.

\begin{table}
\begin{tabular}{|c|c|c|c|} \hline Environment & \(\text{i}_{l}\) & \(\text{i}_{u}\) & \(\mathfrak{g}\) \\ \hline MountainCar & \(-0.11\) & \(-0.1\) & \(0.5\) \\ \hline CartPole & \(-0.1\) & N/A & \(\pi/15\) \\ \hline \end{tabular}
\end{table} TABLE II: Hyperparameters in OpenAI Gym.

Fig. 4: Comparison of MountainCar NN and SDT controller one-shot verification runtimes.

Fig. 3: MountainCar NN policies, L (), I (), R ().

Fig. 2: Transformation time and size of the transformed SDT.
An advantage of SDT controllers is that the policy can be inferred from the tree structure. Fig. 3 plots the policies and SDT leaf node partitions for example MountainCar controllers. Note that constant action state-space regions become more complex as the depth of the NN increases.

All SMT problems in our experiments are solved using an in-house implementation of a satisfiability modulo convex programming (SMC) solver [18], which integrates the Z3 satisfiability (SAT) solver [19] with Gurobi [20]. For the one-shot verification approach, Fig. 4 shows a comparison of the verification times for \(\mathcal{N}\) with \(N=(2,1,3)\) and \(\mathcal{S}_{\mathcal{N}}\) with three leaf nodes in the MountainCar problem. The NN verification time increases significantly compared to the equivalent SDT. However, verification takes more than 60000 seconds for \(\mathcal{N}\) when \(T>38\) and for \(\mathcal{S}_{\mathcal{N}}\) when \(T>64\). For the CartPole problem, all controllers fail to solve the verification problem (8) within 60000 seconds for \(T>10\).

To assess the efficiency of RRA for NN and SDT controllers, we measured runtimes both for individual reachability set determination as well as overall verification time. Figure 4(a) plots reachable sets, along with overall verification and reachable set generation runtimes for an example MountainCar controller with \(s\in\{1,2\}\) in (9). Figure 4(b) plots verification and reachable set generation runtimes for a collection of CartPole controllers with \(s=1\) in (9). As shown, RRA verification becomes more efficient using the equivalent SDT controllers, rather than the reference NNs.

Figure 6 compares the average inference and overall RRA verification times for a collection of NN and equivalent SDT controllers. We set \(T=200\) for the MountainCar problem and \(T=25\) for the CartPole problem. While the inference time for the SDT increases with the number of layers in NN, our results show that the transformed SDT controller accelerates verification for the MountainCar problem by up to \(21\times\) and for the CartPole problem by up to \(2\times\). Moreover, the larger the number of layers in the NN, the larger the difference between runtime for NN verification and runtime for SDT verification.

## VI Conclusion

We proposed a cost-effective algorithm to construct equivalent SDT controllers from any discrete-output argmax-based NN controller. Empirical evaluation of formal verification tasks performed on two benchmark OpenAI Gym environments shows a significant reduction in verification times for SDT controllers. Future work includes experimenting with more sophisticated RL environments and investigating an inverse algorithm to transform soft decision tree controllers into neural network controllers.
