一种用于合成二值化神经网络的自动机理论方法
机器学习
2023-08-01 v1 形式语言与自动机理论
摘要
深度神经网络（DNNs，亦称 NNs）已广泛应用于各类任务并被证明十分成功。然而，伴随而来的高昂计算与存储成本使其在资源受限设备上的部署成为重要关切。为解决此问题，量化作为一种有效手段应运而生，通过将浮点数量化为低比特定点表示，以极小的精度损失降低 DNNs 的成本。量化神经网络（QNNs）由此发展起来，其中限制为二值化的二值化神经网络（BNNs）为其特例。关于神经网络的另一关切是其脆弱性与缺乏可解释性。尽管针对 DNNs 可信性的研究活跃，面向 QNNs 的方法却寥寥无几。为此，本文提出一种自动机理论方法，用于合成满足指定属性的 BNNs。具体而言，我们定义一种称为 BLTL 的时序逻辑作为规约语言。我们证明每个 BLTL 公式均可转化为有限字上的自动机。为应对状态爆炸问题，我们在实际实现中给出了一种基于 tableau 的方法。在合成过程中，我们利用 SMT 求解器来检测模型（即 BNN）的存在性。值得注意的是，合成提供了一种在训练前确定网络超参数的途径。此外，我们通过实验评估了该方法，并证明其在保持较高精度的同时，有效提升了 BNNs 的个体公平性与局部鲁棒性。
引用
@article{arxiv.2307.15907,
title = {An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks},
author = {Ye Tao and Wanwei Liu and Fu Song and Zhen Liang and Ji Wang and Hongxu Zhu},
journal= {arXiv preprint arXiv:2307.15907},
year = {2023}
}