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.

翻译：理解神经网络的特性因其复杂结构与行为而重要但困难。部分先前工作提出将神经网络转化为等价的布尔表达式，并应用验证技术分析目标特性。该方案前景可观，因为电路及其他布尔表达式的丰富验证结果可直接借鉴。其瓶颈在于转化的时间复杂度。具体而言：(i) 网络的每个神经元（即线性阈值函数）需转化为二叉决策图(BDD)；(ii) 进一步合并为最终形式（如布尔电路）。对于含有$n$个变量的线性阈值函数，现有方法需$O(n2^{\frac{n}{2}})$时间构建规模为$O(2^{\frac{n}{2}})$的有序BDD，且需与某种变量顺序一致。然而，从$n!$种变量顺序中选择能生成小规模BDD的排序并非易事。我们提出一种基于机器学习领域提升方法将线性阈值函数转化为特定BDD形式的方法。该方法耗时$O(2^n \text{poly}(1/\rho))$，输出规模为$O(\frac{n^2}{\rho^4}\ln{\frac{1}{\rho}})$的BDD，其中$\rho$为某一致线性阈值函数的间隔。本方法无需搜索最优变量顺序，且当线性阈值函数间隔较大时可生成更紧凑的表达式。值得注意的是，该方法基于我们提出的新提升算法，该算法本身具有独立研究价值。同时，我们提出将其组合为表示神经网络的最终布尔表达式的方法。