基于提升的线性阈值函数 BDD 构造及其在神经网络验证中的应用
机器学习
2023-06-09 v1
摘要
理解神经网络的特征十分重要，但因其复杂结构与行为而困难。一些先前工作提出将神经网络转换为等价的布尔表达式，并对感兴趣的特征应用验证技术。该方法有前景，因为电路及其他布尔表达式验证技术的丰富成果可直接应用。瓶颈在于转换的时间复杂度。更确切地说，(i) 网络的每个神经元（即线性阈值函数）被转换为二叉决策图 (BDD)，且 (ii) 它们被进一步组合为某种最终形式，如布尔电路。对于含 n 个变量的线性阈值函数，已有方法耗时 O(n2^{n/2}) 构造与某变量序一致、大小为 O(2^{n/2}) 的有序 BDD。然而，在 n! 个候选中选取产生小 BDD 的变量序并非易事。我们提出一种基于机器学习文献中提升方法将线性阈值函数转换为特定形式 BDD 的方法。我们的方法耗时 O(2^n poly(1/ρ)) 并输出大小为 O(n^2/ρ^4 ln(1/ρ)) 的 BDD，其中 ρ 为某一致线性阈值函数的间隔。我们的方法无需搜索良好变量序，且当线性阈值函数间隔较大时产生更小表达式。更确切地说，我们的方法基于我们新的提升算法，其本身具有独立意义。我们还提出将其组合为表示神经网络的最终布尔表达式的方法。
引用
@article{arxiv.2306.05211,
title = {Boosting-based Construction of BDDs for Linear Threshold Functions and Its Application to Verification of Neural Networks},
author = {Yiping Tang and Kohei Hatano and Eiji Takimoto},
journal= {arXiv preprint arXiv:2306.05211},
year = {2023}
}