Boosting-based Construction of BDDs for Linear Threshold Functions and
  Its Application to Verification of Neural Networks
Yiping Tang Kohei Hatano Eiji Takimoto
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.