具有保证精度的浮点数神经网络分类的量化技术

《Proceedings of the ACM on Programming Languages》：Quantization with Guaranteed Floating-Point Neural Network Classifications

量化神经网络推理时可能因分类不一致导致误差，本文提出基于验证的校正系统CoMPAQt，通过混合整数线性规划编码量化过程并定制松弛降低复杂度，计算不一致输入的最大置信度。设计两种校正机制：一通过递增位精度网络确保100%一致性且加速3.8倍，二通过量化网络集合实现近似完美一致性并加速4.1倍。首次为量化网络分类一致性提供形式化保证。

　　

摘要

尽管神经网络取得了巨大的成功，但其计算成本仍然非常高。量化技术可以降低这一成本，但可能会导致原始浮点网络的分类结果发生变化，即使训练过程已经考虑了量化的因素。在这项工作中，我们依靠验证机制来设计修正系统，以便在推理时检测并消除分类不一致的问题。关键思想是用最大分类置信度来过度近似不一致输入的空间。计算这种置信度的主要挑战在于需要分析量化的网络，而这会引入极高的非线性。我们提出了CoMPAQt算法来计算这种置信度。CoMPAQt利用混合整数线性规划（MILP）中对量化的新颖编码方式，并结合定制的线性松弛技术来降低计算复杂性。为了缩小搜索空间，该算法将量化网络与其浮点对应网络的计算结果联系起来。基于这种置信度，我们提出了两种修正机制：第一种机制保证返回浮点网络的分类结果，并依赖于具有逐渐增加位精度的网络；第二种机制通过组合多个量化网络来减轻分类不一致的问题。我们在MNIST、ACAS-Xu和表格数据集上对全连接网络及卷积网络进行了实验验证。结果表明，第一种修正机制能够保证与浮点网络分类结果100%一致，同时平均降低计算成本3.8倍；第二种机制在实验中实现了几乎完美的分类一致性，同时计算成本降低了4.1倍。我们的工作是首个对量化网络的分类一致性提供正式保证的研究。