Boosting-based Construction of BDDs for Linear Threshold Functions and
  Its Application to Verification of Neural Networks
Understanding the characteristics of neural networks is important but
difficult due to their complex structures and behaviors. Some previous work
proposes to transform neural networks into equivalent Boolean expressions and
apply verification techniques for characteristics of interest. This approach is
promising since rich results of verification techniques for circuits and other
Boolean expressions can be readily applied. The bottleneck is the time
complexity of the transformation. More precisely, (i) each neuron of the
network, i.e., a linear threshold function, is converted to a Binary Decision
Diagram (BDD), and (ii) they are further combined into some final form, such as
Boolean circuits. For a linear threshold function with $n$ variables, an
existing method takes $O(n2^{\frac{n}{2}})$ time to construct an ordered BDD of
size $O(2^{\frac{n}{2}})$ consistent with some variable ordering. However, it
is non-trivial to choose a variable ordering producing a small BDD among $n!$
candidates.
  We propose a method to convert a linear threshold function to a specific form
of a BDD based on the boosting approach in the machine learning literature. Our
method takes $O(2^n \text{poly}(1/\rho))$ time and outputs BDD of size
$O(\frac{n^2}{\rho^4}\ln{\frac{1}{\rho}})$, where $\rho$ is the margin of some
consistent linear threshold function. Our method does not need to search for
good variable orderings and produces a smaller expression when the margin of
the linear threshold function is large. More precisely, our method is based on
our new boosting algorithm, which is of independent interest. We also propose a
method to combine them into the final Boolean expression representing the
neural network.
Yiping Tang, Kohei Hatano, Eiji Takimoto
Boosting-based Construction of BDDs for Linear Threshold Functions and Its Application to Verification of Neural Networks

###### Abstract

Understanding the characteristics of neural networks is important but difficult due to their complex structures and behaviors. Some previous work proposes to transform neural networks into equivalent Boolean expressions and apply verification techniques for characteristics of interest. This approach is promising since rich results of verification techniques for circuits and other Boolean expressions can be readily applied. The bottleneck is the time complexity of the transformation. More precisely, (i) each neuron of the network, i.e., a linear threshold function, is converted to a Binary Decision Diagram (BDD), and (ii) they are further combined into some final form, such as Boolean circuits. For a linear threshold function with \(n\) variables, an existing method takes \(O(n2^{\frac{n}{2}})\) time to construct an ordered BDD of size \(O(2^{\frac{n}{2}})\) consistent with some variable ordering. However, it is non-trivial to choose a variable ordering producing a small BDD among \(n!\) candidates.

We propose a method to convert a linear threshold function to a specific form of a BDD based on the boosting approach in the machine learning literature. Our method takes \(O(2^{n}\text{poly}(1/\rho))\) time and outputs BDD of size \(O(\frac{n^{2}}{\rho^{4}}\ln\frac{1}{\rho})\), where \(\rho\) is the margin of some consistent linear threshold function. Our method does not need to search for good variable orderings and produces a smaller expression when the margin of the linear threshold function is large. More precisely, our method is based on our new boosting algorithm, which is of independent interest. We also propose a method to combine them into the final Boolean expression representing the neural network. In our experiments on verification tasks of neural networks, our methods produce smaller final Boolean expressions, on which the verification tasks are done more efficiently.

Convolutional Neural Network Binary decision diagram Boosting Verification.

## 1 Introduction

Interpretability of Neural Networks (NNs) has been relevant since their behaviors are complex to understand. Among many approaches to improve interpretability, some results apply verification techniques of Boolean functions to understand NNs, where NNs are represented as an equivalent Boolean function and then various verification methods are used to check criteria such as robustness [10]Liu, Malon, Xue, and Kruus, Mangal et al.(2019)Mangal, Nori, and Orso, [20]Weng, Zhang, Chen, Yi, Su, Gao, Hsieh, and Daniel, Yu et al.(2019)Yu, Qin, Liu, Zhao, Wang, and Chen, Zheng et al.(2016)Zheng, Song, Leung, and Goodfellow. This
approach is promising in that rich results of Boolean function verification can be readily applied. The bottleneck, however, is to transform a NN into some representation of the equivalent Boolean function.

A structured way of transforming NNs to Boolean function representations is proposed by [14, 15]. They proposed (i) to transform each neuron, i.e., a linear threshold function, into a Binary Decision Diagram (BDD) and then (ii) to combine BDDs into a final Boolean function representations such as Boolean circuits. In particular, the bottleneck is the transformation of a linear threshold function to a BDD. To do this, they use the transformation method of [14]. The method is based on dynamic programming, and its time complexity is \(O(n2^{\frac{n}{2}})\) and the size of resulting BDD is \(O(2^{\frac{n}{2}})\), where \(n\) is the number of the variables. In addition, the method requires a fixed order of \(n\) variables as an input and outputs the minimum BDD consistent with the order. Thus, to obtain the minimum BDD, it takes \(O(n!n2^{\frac{n}{2}})\) time by examining \(n!\) possible orderings. Even if we avoid the exhaustive search of orderings, it is non-trivial to choose a good ordering.

In this paper, we propose an alternative method to obtain a specific form of BDD representation (named Aligned Binary Decision Diagram, ABDD) of a linear threshold function. Our approach is based on _Boosting_, a framework of machine learning which combines base classifiers into a better one. More precisely, our method is a modification of the boosting algorithm of Mansour and McAllester [16]. Given a set of labeled instances of a linear threshold function, their algorithm constructs a BDD that is consistent with the instances in a top-down greedy way. The algorithm can be viewed as a combination of greedy decision tree learning and a process of merging nodes. Given a linear threshold function \(f(x)=\sigma(w\cdot x+b)\) where \(\sigma\) is the step function, we can apply the algorithm of Mansour and McAllester by feeding all \(2^{n}\) possible labeled instances of \(f\) and obtain a BDD representation of \(f\) of the size \(O(\frac{n^{2}}{\rho^{4}}\ln\frac{1}{\rho})\) in time \(O(2^{n}\text{poly}(1/\rho))\), where \(\rho\) is the margin of \(f\), defined as \(\rho=\min_{x\in\{-1,1\}^{n}}|w\cdot x+b|/\|w\|_{1}\). An advantage of the method is that the resulting BDD is small if the linear threshold function has a large margin. Another merit is that the method does not require a variable ordering as an input. However, in our initial investigation, we observe that the algorithm is not efficient enough in practice. Our algorithm, in fact, a boosting algorithm, is obtained by modifying their algorithm so that we only use one variable (base classifier) in each layer. We show that our modification still inherits the same theoretical guarantees as Mansour and McAllester's. Furthermore, surprisingly, the small change makes the merging process more effective and produces much smaller BDDs in practice. Our modification might look easy but is non-trivial in a theoretical sense. To achieve the same theoretical guarantee, we introduce a new information-theoretic criterion to choose variables that is different from the previous work. That is one of our technical contributions.

In our experiments on verification tasks of Convolutional Neural Networks (CNNs), by following the same procedures as [14, 15], we construct smaller BDDs and resulting Boolean representations of CNNs faster than in previous work, thus contributing to more efficient verification.

This paper is organized as follows: Section 2 overviews the preliminaries of binary NN (BNN), BDD, Ordered BDD (OBDD), and Aligned BDD (ABDD). Section 3 and 4 detail our proposed method to construct ABDD. Section 5 details the construction of the Boolean circuit and SDD. Section 6 handles the experimental results with analysis, followed by the conclusion in Section 7.

Related workThe work in [16]Narodytska, Kasiviswanathan, Ryzhyk, Sagiv, and Walsh] proposed a precise Boolean encoding of BNNs that allows easy network verification. However, it only works with small-sized networks. [14]Shih, Darwiche, and Choi] leveraged the Angluin-style learning algorithm to convert the BNN (the weights and input are binarized as \(\{-1,1\}\)) and OBDD into Conjunctive Normal Form (CNF) and then used the Boolean Satisfiability (SAT) solver to verify the equivalence of its produced CNF. However, they modified the OBDD several times and utilized limited binary network weights. [14] suggested a method to convert a linear threshold classifier with real-valued weight into OBDD. However, their approach owns time complexity of \(O(n!n2^{\frac{n}{2}})\) and OBDD size complexity of \(O(2^{\frac{n}{2}})\) via searching the full ordering, which increases exponentially

\begin{table}
\begin{tabular}{|c|c|c|c|} \hline Method & DD type & Size & Time \\ \hline
[14] & OBDD & \(O(2^{\frac{n}{2}})\) & \(O(n!n2^{\frac{n}{2}})\) \\ \hline
[16] & BDD & \(O(\frac{n}{\rho^{4}}\ln\frac{1}{\rho})\) & \(O(2^{n}\text{poly}(1/\rho))\) \\ \hline Ours & ABDD & \(O(\frac{n}{\rho^{4}}\ln\frac{1}{\rho})\) & \(O(2^{n}\text{poly}(1/\rho))\) \\ \hline \hline (cf. [14, 15]Shih, Darwiche, and Choi]) & OBDD & \(O(nW)\) & \(O(nW)\) \\ \hline \end{tabular}
\end{table}
Table 1: Time and size for several methods to convert to DDs from a given linear threshold function (LTF, for short) of margin \(\rho\). The fourth result is only for LTFs with integer weights whose \(L2\)-norm is \(W\).
when \(n\) becomes larger. Still, [Narodytska et al.(2018)Narodytska, Kasiviswanathan, Ryzhyk, Sagiv, and Walsh, Shih et al.(2019)Shih, Darwiche, and Choi, Chan and Darwiche(2003)] can only handle small dimension NN weight, and the large Boolean expression was represented as Sentential Decision Diagram (SDD), which owns enormous time complexity. Moreover, [Chorowski and Zurada(2011)] proposed a rule extraction method inspired by the 'rule extraction as learning" approach to express NN into a Reduced Ordered DD (RODD), which has the time complexity of \(O(n2^{2n})\).

## 2 Preliminaries

### Binary Neural Network

A binary neural network (BNN) is a variant of the standard NN with binary inputs and outputs [Bshouty et al.(1998)Bshouty, Tamon, and Wilson]. In this paper, each neural unit, with a step activation function \(\sigma\), is formulated as follows:

\[\sigma(\sum_{i}x_{i}w_{i}+b)=\begin{cases}1,&\sum_{i}x_{i}w_{i}+b\geq 0\\ -1,&\text{otherwise}\end{cases} \tag{1}\]

where \(x\in\{-1,1\}^{n}\), \(w\in\mathbb{R}^{n}\) and \(b\in\mathbb{R}\) are the input, the weight vector and the bias of this neural unit, respectively.

### Definition of BDD, OBDD and ABDD

A binary decision diagram (BDD) \(T\) is defined as a tuple \(T=(V,E,l)\) with the following properties: (1) \((V,E)\) is a directed acyclic graph with a root and two leaves, where \(V\) is the set of nodes, \(E\) is the set of edges such that \(E=E_{-}\cup E_{+}\), \(E_{-}\cap E_{+}=\varnothing\). Elements of \(E_{+}\) and \(E_{-}\)'s are called \(+\)-edges, and \(--\)edges, respectively. Let \(L=\{\text{0-leaf, 1-leaf}\}\subset V\) be the set of leaves. For each \(v\in V\), there are two child nodes \(v^{-},v^{+}\in V\) such that \((v,v^{-})\in E_{-}\) and \((v,v^{+})\in E_{+}\). (2) \(l\) is a function from \(V\setminus L\) to \([n]\).

Given an instance \(x\in\{-1,1\}^{n}\) and a BDD \(T\), we define the corresponding path \(P(x)=(v_{0},v_{1},\ldots,v_{k-1},v_{k})\in V^{*}\) over \(T\) from the root to a leaf as follows: (1) \(v_{0}\) is the root. (2) for any \(j=0,\ldots k-1\), we have \((v_{j},v_{j+1})\in E_{+}\Leftrightarrow x_{l(v_{j})}=1\) and \((v_{j},v_{j+1})\in E_{-}\Leftrightarrow x_{l(v_{j})}=-1\). (3) \(v_{k}\) is a leaf node. We say that an instance \(x\in\{-1,1\}^{n}\) reaches node \(u\) in \(T\), if \(P(x)\) contains \(u\). Then, a BDD \(T\) naturally defines the following function \(h_{T}:\{-1,1\}^{n}\rightarrow\{-1,1\}\) such that

\[h_{T}(x)\triangleq\begin{cases}-1,&\text{$x$ reaches $0$-leaf}\\ 1,&\text{$x$ reaches $1$-leaf}.\end{cases} \tag{2}\]

Given a BDD \(T=(V,E,l)\), we define the depth of a node \(u\in V\) as the length of the longest path from the root to \(u\). An ordered BDD (OBDD) \(T=(V,E,l)\) is a BDD satisfying an additional property: There is a strict total order \(<_{[n]}\) on \([n]\) such that for any path \(P=(v_{0},\ldots,v_{k})\) on from the root to a leaf, and any nodes \(v_{i}\) and \(v_{j}\)\((i<j<k)\), \(l(v_{i})<_{[n]}l(v_{j})\). An Aligned BDD (ABDD) \(T=(V,E,l)\) is defined as a BDD satisfying that for any nodes \(u,v\in V\setminus L\) with the same depth, \(l(u)=l(v)\). We employ \(v_{i,j}\) to appear the positional information of a node in the BDD, where \(j\) represents the depth of the node, and \(i\) represents the position of the node at depth \(j\).

BDD, OBDD and ABDD are illustrated in Figure 1.

### Instance-based Robustness (IR), Model-based Robustness (MR) and Sample-based Robustness (SR)

Robustness is a fundamental property of the neural network, which represents the tolerance of the network to noise or white attacks. For binary input images, the robustness \(k\) represents that as long as at least \(k\) pixels are flipped from 0 to 1 or 1 to 0, and the neural network's output will be changed.

We define the IR and MR of a network as follows.

**Definition 1**.: _(Instance-based Robustness) [Shi et al.(2020)Shi, Shih, Darwiche, and Choi] Consider a classification function \(f:\{-1,1\}^{n}\rightarrow\{-1,1\}\) and a given instance \(x\). The robustness of the classification of \(x\) by \(f\), denoted by \(r_{f}(x)\). If \(f\) is not a trivial function (always \(True\) or \(False\)),_

\[r_{f}(x)=\min_{x^{\prime};f(x)\neq f(x^{\prime})}dis(x,x^{\prime}) \tag{3}\]

_where \(dis(x,x^{\prime})\) denotes the Hamming distance between \(x\) and \(x^{\prime}\)._
**Definition 2**.: _(Model-based Robustness) [20][21, 22]. The Model-based Robustness of \(f\) is defined as:_

\[MR(f)=\frac{1}{2^{n}}\sum_{x}r_{f}(x). \tag{4}\]

However, we consider that computing MR on full-size data is not practically meaningful. In practical applications, robustness validation based on sample data is common. Here, we regard the samples in the dataset as instances randomly extracted from the full-size data under the uniform distribution. Then, we have the following definition.

**Definition 3**.: _(Sample-based Robustness, SR) Consider a classification function \(f:\left\{-1,1\right\}^{n}\rightarrow\left\{-1,1\right\}\). Given a sample \(S\) under uniform distribution from \(\{-1,1\}^{n}\). The Sample-based Robustness of \(f\) is defined as:_

\[SR(f)=\frac{1}{|S|}\sum_{x\in S}r_{f}(x). \tag{5}\]

### Overview of our method

In Section 3, we propose an algorithm that constructs an ABDD whose training error is small with respect to a given sample of some target Boolean function. Our algorithm is based on boosting, which is an effective approach in machine learning that constructs a more accurate classifier by combining "slightly accurate" classifiers. In Section 4, we apply our boosting algorithm for finding an equivalent ABDD with a given linear threshold function. Under a natural assumption that the linear threshold function has a large "margin", we show the size of the resulting ABDD is small. In Section 5, we show how to convert a given BNN to an equivalent Boolean expression suitable for verification tasks. More precisely, (i) Each neural unit is converted to an equivalent ABDD by applying our boosting algorithm, (ii) each ABDD is further converted to a Boolean circuit, and (iii) all circuits are combined into the final circuit, which is equivalent to the given BNN. Furthermore, for a particular verification task, we convert the final circuit to an equivalent sentential decision diagram (SDD).

## 3 Boosting

### Problem Setting

Boosting is an approach to constructing a strongly accurate classifier by combining weakly accurate classifiers. We assume some unknown target function \(f:\left\{-1,1\right\}^{n}\rightarrow\left\{-1,1\right\}\). Given a sample \(S=((x_{1},f(x_{1})),\ldots,(x_{m},f(x_{m})))\in(\{-1,1\}^{n}\times\{-1,1\})^ {m}\) of \(m\) instances labeled by \(f\) and a precision parameter \(\varepsilon\), we want to find a classifier \(g:\left\{-1,1\right\}^{n}\rightarrow\left\{-1,1\right\}\) such that its training error \(\Pr_{U}\{g(x)\neq f(x)\}\leq\varepsilon\), where

Figure 1: Examples of BDD (A), OBDD (B) and ABDD (C). To express the same linear threshold function in BDD form: nodes at the same depth can be labeled by different variables, which means that the number of variables does not limit the depth of BDD; in OBDD form: the nodes at the same depth are all labeled by the same variables, which results in the depth of OBDD is smaller than the number of variables; in ABDD form: nodes at the same depth are labeled by the same variables, and the depth of ABDD only depends on the reduction of entropy to 0 in our algorithm.
is the uniform distribution over \(S\). We are also given a set \(\mathcal{H}\) of base classifiers from \(\{-1,1\}^{n}\) to \(\{-1,1\}\). We assume the following assumption which is standard in the boosting literature [Mansour and McAllester(2002)].

**Definition 4**.: _(Weak Hypotheses Assumption (WHA)) A hypothesis set \(\mathcal{H}\) satisfies \(\gamma\)-Weak Hypothesis Assumption (WHA) for the target function \(f:\{-1,1\}^{n}\to\{-1,1\}\) if for any distribution \(d\) over \(\{-1,1\}^{n}\), there exists \(h\in\mathcal{H}\) such that \(edge_{d,f}(h)\triangleq\sum_{x\in\{-1,1\}^{n}}d_{x}f(x)h(x)\geq\gamma\)._

Intuitively, WHA ensures the set of \(\mathcal{H}\) of hypotheses and \(f\) are "weakly" related to each other. The edge function \(edge_{d,f}(h)\) takes values in \([-1,1]\) and equals to \(1\) if \(f=h\). Under WHA, we combine hypotheses of \(\mathcal{H}\) into a final hypothesis \(h_{T}\) represented by an ABDD \(T\).

Our analysis is based on a generalized version of entropy [Kearns and Mansour(1999)]. A pseudo-entropy \(G:[0,1]\to[0,1]\) is defined as \(G(q)\triangleq 2\sqrt{q(1-q)}\). Like the Shannon entropy, \(G\) is concave and \(G(1/2)=1\), and \(G(0)=G(1)=0\). In particular, \(\min(q,1-q)\leq G(q)\). Then we will introduce the conditional entropy of \(f\) given a sample \(S\) and an ABDD \(T\). For each node \(u\) in \(T\), let \(p_{u}\triangleq\Pr_{U}\{x\text{ reaches }u\}\) and \(q_{u}\triangleq\Pr_{U}\{f(x)=1\mid x\text{ reaches }u\}\), respectively. Let \(N(T)\) be the set of nodes in \(V\setminus L\) whose depth is the maximum. We further assume that for each node \(u\) in \(N(T)\), the \(x\) in \(u\) is assigned to \(1\)-leaf if \(q_{u}\geq 1/2\), and is assigned to \(0\)-leaf, otherwise. Then, observe that \(\Pr_{U}\{f(x)\neq h_{T}(x)\}=\sum_{u\in N(T)}p_{u}\min(q_{u},1-q_{u})\). The conditional entropy of \(f\) given an ABDD \(T\) with respect to the distribution \(U\) is defined as

\[H_{U}(f|T)=\sum_{u\in N(T)}p_{u}G(q_{u}). \tag{6}\]

Then the conditional entropy gives an upper bound of the training error as follows.

**Proposition 1**.: \(\Pr_{U}\{h_{T}(x)\neq f(x)\}\leqslant H_{U}(f|T)\)_._

Therefore, it is sufficient to find an ABDD \(T\) whose conditional entropy \(H_{U}(f|T)\) is less than \(\varepsilon\).

We will further use the following notations and definitions. Given an ABDD \(T\), \(S\) and \(u\in N(T)\), let \(S_{u}=\{(x,y)\in S\mid x\text{ reaches }u\}\). The entropy \(H_{d}(f)\) of \(f:\{-1,1\}^{n}\to\{-1,1\}\) with respect to a distribution \(d\) over \(\{-1,1\}^{n}\) is defined as \(H_{d}(f)\triangleq G(q)\), where \(q=\Pr_{d}\{f(x)=1\}\). The conditional entropy \(H_{d}(f|h)\) of \(f\) given \(h:\{-1,1\}^{n}\to\{-1,1\}\) with respect to \(d\) is defined as \(H_{d}(f|h)=\Pr_{d}\{h(x)=1\}G(q^{+})+\Pr_{d}\{h(x)=-1\}G(q^{-})\), where \(q^{\pm}=\Pr_{d}\{f(x)=1\mid h(x)=\pm 1\}\), repectively.

### Our Boosting Algorithm

Our algorithm is a modification of the boosting algorithm proposed by Mansour and McAllester [Mansour and McAllester(2002)]. Both algorithms learn Boolean functions in the form of BDDs in a top-down manner. The difference between our algorithm and Mansour and McAllester's algorithm lies in the construction of the final Boolean function, where ours utilizes ABDDs, while Mansour and McAllester's algorithm does not. Although this change may appear subtle, it necessitates a new criterion for selecting hypotheses in \(\mathcal{H}\) and demonstrates improved results in our experiments.

Our boosting algorithm iteratively grows an ABDD by adding a new layer at the bottom. More precisely, at each iteration \(k\), given the current ABDD \(T_{k}\), the algorithm performs the following two consecutive processes (as illustrated in Figure 2).

**Split:**: It chooses a hypothesis \(h_{k}\in\mathcal{H}\) using some criterion and adds two child nodes for each node in \(N(T_{k})\) in the next layer, where each child corresponds to \(\pm 1\) values of \(h_{k}\). Let \(T_{k}^{\prime}\) be the resulting DD.
**Merge:**: It merges nodes in \(N(T_{k}^{\prime})\) according to some rule and let \(T_{k+1}\) be the ABDD after the merge process.

The full description of the algorithm is given in Algorithm 1 and 2, respectively. For the split process, it chooses the hypothesis \(h_{k}\) maximizing the edge \(edge_{\hat{d},f}(h)\) with respect to the distribution \(\hat{d}\) specified in (9). For the merge process, we use the same way in the algorithm of Mansour and McAllester [Mansour and McAllester(2002)].

**Definition 5**.: _[_Mansour and McAllester(2002)_]_ _For \(\delta\) and \(\lambda\) (\(0<\delta,\lambda<1\)), a (\(\delta,\lambda\))-net \(\mathcal{I}\) is defined as a set of intervals \([v_{0},v_{1}],[v_{1},v_{2}],\ldots,[v_{w-1},v_{w}]\) such that (i) \(v_{0}=0\), \(v_{w}=1\), (ii) for any \(I_{k}=[v_{k-1},v_{k}]\) and \(q\in I_{k}\), \(\max_{q^{\prime}\in I_{k}}G(q^{\prime})\leq\max\{\delta,(1+\lambda)G(q)\}\)._

Mansour and McAllester showed a simple construction of \((\delta,\lambda)\)-net with length \(w=O((1/\lambda)\ln(1/\delta))\)[Mansour and McAllester(2002)] and we omit the details. Our algorithm uses particular \((\delta,\lambda)\)-nets for merging nodes.
### Analyses

\[H_{d}(Y|T,h)=\sum_{u\in N(T)}(p_{u^{+}}G(q_{u^{+}})+p_{u^{-}}G(q_{u^{-}})) \tag{7}\]

where \(p_{u^{+}}=Pr_{d}\{x\text{ reaches }u|h(x)=1\}\) and \(q_{u^{+}}=Pr_{d}(f(x)=1|x\text{ reaches }u\), \(h(x)=1)\). \(p_{u^{-}}\) and \(q_{u^{-}}\) are defined similarly.

The following lemmas prove an effective weak learning algorithm under a variant balanced distribution \(\bar{d}\), and it also can be achieved under any distribution. For \((x,y)\in S\):

\[\bar{d}_{(x,y)}=\frac{d_{(x,y)}}{2\sum_{(x^{\prime},y)\in S}d_{(x^{\prime},y)}} \tag{8}\]

**Lemma 1**.: _[_7_]_ _Let \(d\) and \(\bar{d}\) be any distribution over \(\{-1,1\}^{n}\) and its balanced distribution with respect to some \(f:\{-1,1\}^{n}\rightarrow\{-1,1\}\), respectively. Then, for any hypothesis with \(edge_{\bar{d},f}(h)\geq\gamma\), \(H_{d}(f|h)\leqslant(1-\gamma^{2}/2)H_{d}(f)\)._

Based on Lemma 1, we establish the connection between \(\gamma\) and entropy function, and have a \(\gamma^{*}\in(0,1)\) at each depth to reflect the entropy change under our algorithm.

**Lemma 2**.: _Let \(\hat{d}\) be the distribution over \(S\) specified in (9) when \(T_{k}\), \(\mathcal{H}\) and \(S\) is given by Algorithm 2 and let \(h_{k}\) be the output. If \(\mathcal{H}\) satisfies \(\gamma\)-WHA, then the conditional entropy of \(f\) with respect to the distribution \(U\) over \(S\) given \(T_{k}\) and \(h_{k}\) is bounded as \(H_{U}(f|h_{k},T_{k})\leqslant(1-\gamma^{2}/2)H_{U}(f|T_{k})\)._

**Lemma 3**.: _([11]) Assume that, before the merge process in Algorithm 1, \(H_{U}(f|h_{k},T_{k})\leq(1-\gamma)H_{U}(f|T_{k})\) for some \(\lambda\) (\(0<\lambda<1\)). Then, by merging based on the \((\delta,\eta)\)-net with \(\delta=(\lambda/6)H_{U}(f|T_{k})\) and \(\eta=\lambda/3\), the conditional entropy of \(f\) with respect to the distribution \(U\) over \(S\) given \(T_{k+1}\) is bounded as \(H_{U}(f|T_{k+1})\leqslant(1-\lambda/2)H_{U}(f|T_{k})\), where the width of \(T_{k+1}\) is \(O((1/\lambda)(\ln(1/\lambda)+\ln(1/\varepsilon)))\), provided that \(H_{U}(f|T_{k})>\varepsilon\)._

```
0: a sample \(S\in(\{-1,1\}^{n}\times(-1,1))^{m}\) of \(m\) instances by \(f\), and a set \(\mathcal{H}\) of of hypotheses, and precision parameter \(\varepsilon\) (\(0<\varepsilon<1\));
0: ABDD \(T\);
1: initialization: \(T_{1}\) is the ABDD with a root and \(0,1\)-leaves, \(k=1\).
2:repeat
3: (Split) Let \(h_{k}=Split(T,\mathcal{H},S)\) and add child nodes with each node in \(N(T_{k})\). Let \(T_{k}^{\prime}\) be the resulting ABDD.
4:for\(u\in N(T_{k}^{\prime})\)do
5: merge \(u\) to the \(0\)-leaf (the \(1\) leaf) if \(q_{u}=0\) (\(q_{u}=1\), resp.).
6:endfor
7: (Merge) Construct a \((\hat{\delta},\hat{\lambda}/3)\)-net \(\mathcal{I}_{k}\) with
8:\(\hat{\lambda}=1-\frac{H_{U}(f|T_{k},h_{k})}{H_{U}(f|T_{k})}\), and \(\hat{\delta}=\frac{\hat{\lambda}H_{U}(f|T_{k})}{6}\).
9:for\(I\in\mathcal{I}_{k}\)do
10: merge all nodes \(u\in N(T_{k}^{\prime})\) such that \(q_{u}\in I\).
11:endfor
12: Let \(T_{k+1}\) be the resulting ABDD and update \(k\gets k+1\).
13:until\(H_{U}(f|T_{k})<\varepsilon\)
14: Output \(T=T_{k}\).
```

**Algorithm 1** ABDD Boosting

Now we are ready to show our main theorem.

**Theorem 4**.: _Given a sample \(S\) of \(m\) instances labeled by \(f\), and a set \(\mathcal{H}\) of hypotheses satisfying \(\gamma\)-WHA, Algorithm 1 outputs an ABDD \(T\) such that \(\Pr_{U}\{h_{T}(x)\neq f(x)\}\leq\varepsilon\). The size of \(T\) is \(O((\ln(1/\varepsilon)/\gamma^{4})(\ln(1/\varepsilon)+\ln(1/\gamma)))\) and the running time of the algorithm is \(poly(1/\gamma,n)m\)._

## 4 ABDD Construction

We now apply the ABDD Boosting algorithm developed in the previous section to a given linear threshold function \(f\) to obtain an ABDD representation \(\bar{T}\) for \(f\). In particular, we show that the size of \(T\) is small when \(f\) has a large margin.
To be more specific, assume that we are given a linear threshold function \(f:\{-1,1\}^{n}\rightarrow\{-1,1\}\) of the form

\[f(x)=\sigma(w\cdot x+b)\]

for some weight vector \(w\in\mathbb{R}^{n}\) and bias \(b\in\mathbb{R}\), where \(\sigma\) is the step function, i.e., \(\sigma(z)\) is \(1\) if \(z\geq 0\) and \(-1\) otherwise. Note that there are infinitely many \((w,b)\) inducing the same function \(f\). We define the margin \(\rho\) of \(f\) as the maximum margin \(f(x)(w\cdot x+b)/\|w\|_{1}\) over all \((w,b)\). We let our hypothesis set \(\mathcal{H}\) consist of projection functions, namely, \(\mathcal{H}=\{h_{1},h_{2},\ldots,h_{n},h_{n+1},h_{n+2},\ldots,h_{2n}\}\), where \(h_{i}:x\mapsto x_{i}\) if \(i\leq n\) and \(h_{i}:x\mapsto-x_{i}\) otherwise, so that we can represent \(f\) as \(f(x)=\sigma(\sum_{i=1}^{2n}w_{i}h_{i}(x)+b)\) for some non-negative \(2n\)-dimensional weight vector \(w\geq 0\) and bias \(b\). Then, we can represent the margin \(\rho\) of \(f\) as the solution of the optimal solution for the following LP problem:

\[\max_{w,b,\rho}\rho\] (10) s.t. \[f(x)(\sum_{i=1}^{2n}w_{i}h_{i}(x)+b)\geq\rho\text{ for any }x\in\{-1,1 \}^{n},\] \[w\geq 0,\] \[\sum_{i}w_{i}=1.\]

Now we show that \(\mathcal{H}\) actually satisfies \(\rho\)-WHA for \(f\).

Figure 2: Illustration of our boosting algorithm. The blue dotted line part represents the process of merging the split temporary nodes into new nodes by searching the equivalence space that does not appear in the ABDD. Following algorithm 1, we find some hypothesis \(h\) to construct child nodes in the new layer and then merge nodes afterward.
**Lemma 5**.: _Let \(f\) be a linear threshold function with margin \(\rho\). Then \(\mathcal{H}\) satisfies \(\rho\)-WHA._

By the lemma and Theorem 4, we immediately have the following corollary.

**Corollary 1**.: _Let \(f\) be a linear threshold function with margin \(\rho\). Applying the ABDD Boosting algorithm with the sample \(S=\{(x,f(x))\mid x\in\{-1,1\}^{n}\}\) of all (2\({}^{n}\)) instances, our hypothesis set \(\mathcal{H}\), and the precision parameter \(\varepsilon=1/2^{n}\), we obtain an ABDD \(T\), which is equivalent to \(f\) of size \(O\left(\frac{n}{\rho^{1}}(n+\ln(1/\rho))\right)\)._

## 5 Circuit and SDD Construction

Since we have a method to convert linear threshold functions into a DD representation, the next step is to connect them according to the structure of the NN to form an equivalent \((\vee,\wedge,\neg)\)-circuit, which is used to verify SR. Subsequently, we can convert the circuit into an SDD, which is used to verify robustness.

The conversion process from a DD to a circuit is performed in a top-down manner. As shown in Figure 3, the region enclosed by the red dashed box represents a conversion unit. This unit converts a node \(x_{1}\) and its two edges in the DD into four gates and a variable in the circuit. As the next node \(x_{2}\) is connected to a different edge of node \(x_{1}\), we generate a new circuit beginning with an 'or'-gate and connect it to the 'and'-gate obtained from the conversion of an edge associated with \(x_{1}\). This process is repeated until all edges of the nodes reach either the 0-leaf or the 1-leaf. The resulting circuit is equivalent to the DD and its corresponding neural unit. To construct the NN's equivalent circuit, we utilize Algorithm 1 to generate DDs for each neuron in the NN. These DDs are then converted into circuit form. We combine these equivalent circuits based on the structure of the NN, specifically establishing a one-to-one correspondence between the inputs and outputs of each neuron in the NN and the inputs and outputs of the circuit. This completes the construction of the NN's equivalent circuit. Such a method is also described in [14, 15].

Once we have the equivalent circuit of a neural network (NN), the subsequent step is to convert it into an SDD. SDD is a subclass of deterministic Decomposable Negation Normal Form (d-DNNF) circuits that assert a stronger decomposability and a more robust form of determinism [1]. The class of SDDs generalizes that of OBDDs in that, every OBDD can be turned into an SDD in linear time. In contrast, some Boolean functions have polynomial-size SDD representations but only exponential-size OBDD representations [1]. In SDD, Boolean functions are represented through the introduction of "decision (\(\vee\)) nodes" and "conjunction (\(\wedge\)) nodes."

Indeed, the size complexity of each \(apply\) operation between two SDD nodes is proportional to the product of their internal nodes. Consequently, as the complexity of the circuit increases, the construction of the corresponding SDD requires more space. Considering the conversion process according to ABDD, if the resulting circuit is smaller, it follows that the corresponding SDD constructed from it will also be smaller in size. The size reduction in the circuit conversion directly influences the size of the resulting SDD. Therefore, by optimizing the BDD/circuit representation, we can achieve a more compact SDD.

Figure 3: Example of converting BDD/OBDD/ABDD (Left) to the circuit (Right).
## 6 Experiments

### Experimental Setup

We use the USPS digits dataset of hand-written digits, consisting of \(16\times 16\) binary pixel images. We use the data with labels 0 and 1 for verification of SR.The NN design we used is similar to [21], which has two convolution layers and a full-connected layer. In training, we use two real-valued-weight convolutional layers (kernel size 3, stride 2; kernel size 2, stride 2) with a sigmoid function and a real-valued-weight fully-connected layer in the NN. In testing, the sigmoid function is replaced with the step activation function mentioned before. The experiments are conducted using a CPU of Intel(R) Xeon(R) Gold 2.60GHz. The batch size equals 32 and the utilized learning rate is 0.01 decaying to 10% at half and three-quarters of all learning epochs. Here, the Stochastic Gradient Descent (SGD) optimizer with a momentum of 0.9 and a weight decay of 0.0001 is used.

### Sample-based Robustness (SR) validation

The SR of a standard NN whose output is real-valued is achieved simply by querying the pixels that affect the recognition the most and flipping them until the recognition result changes. Nevertheless, on the standard methods, for a BNN that has input size \(h\times w\), the time cost to compute robustness \(k\) is \(O((hw)^{k})\), which is difficult to use in BNNs.

Since BDD, OBDD, and ABDD are easily represented as a circuit, as shown in Figure 3. The circuits of several neural units are linked into a circuit \(f\) that represents the entire NN according to its network structure. Note that we separately verify the SR of the OBDDs generated by the methods based on Theorem 1 and Theorem 2 in [21], Shih, Darwiche, and Choi] using a circuit representation. The integration of weights and bias in Theorem 2 is performed as follows.

For each \(w\) in weight \(W\) and bias \(b\), We set \(\alpha=\max\{|w_{1}|,\ldots,|w_{n}|,|b|\}\), then we turn them to integer weight \(\hat{w}_{i}=\lfloor\frac{10^{p}}{\alpha}w_{i}\rfloor\) and bias \(\hat{b}=\lfloor\frac{10^{p}}{\alpha}b\rfloor\) where \(p\) is the number of digits of precision.

As for \(dis()\) in Definition 1, it's easy to express the \(k\leq dis(x,x^{\prime})\) between \(x\) and \(x^{\prime}\) in a circuit form and likewise convert it to circuit \(g_{k,x}\) denoted as follows:

\[g_{k,x}(x^{\prime})=\begin{cases}1,&if\mid x\oplus x^{\prime}\mid\leq k\\ -1,&otherwise\end{cases} \tag{11}\]

We calculate the SR of \(f\) on (positive and negative) instance \(x\), where have \(f(x)=1\) and \(f(x)=-1\), by running Algorithm 3 of BDD, OBDD and ABDD on 10 CNNs, the results as shown in Table 2.Note that the SR of negative instances can be computed by invoking Algorithm 3 on function \(\neg f\).

```
1:circuit \(f\), (positive) instance \(x\in\{-1,1\}^{n}\);
2:\(r_{f}(x)\);
3:initial: \(r_{f}=0\);
4:for\(k=1\) to n do
5:if\(g_{k,x}\wedge\overline{f}\) is satisfiable then
6: break
7:endif
8:endfor
9:return\(k\)
```

**Algorithm 3**\(SR\)

In table 2, (Shi.1) circuits are generated using the Theorem 1 proposed in [21, 22], while (MM.) circuits are generated using the method described in [21], and (Shi.2 \(p\)) circuits are generated using the Theorem 2 proposed in [21], Shih, Darwiche, and Choi] under the number of digits of precision \(p=2,3,4\). As observed, the number of gates of (Shi.2 \(2,3,4\)) are significantly larger than the others, it also consumes more time during SR validation (over 10 hours).
### Analysis

We train a standard CNN and show 99.73% accuracy on the test set. Then we replace the sigmoid function with the step activation function, and the accuracy of the CNN dropped to 99.22%. To represent BCNN, compare to BDD and OBDD, our algorithm can generate smaller ABDD while keeping the same recognition accuracy. It provides certain advantages in later work. Note that since [21]Shi et al.(2020)Shi et al.
same variable labels the nodes at the same depth, and the depth is not limited to the number of dimensions of the variable. Experimental results show that ABDD can be connected in various forms to express NN and can be used to implement various verification tasks efficiently. Since our method can be used to generate a smaller equivalent circuit of the NN, it can be applied in tasks such as hardware-based transformations of NNs. In the future, we aim to extend our method to more complex NNs.
