一句话：提出CoMPAQt用MILP验证量化网络分类不一致性，并给出保证或近似保证与浮点网络分类一致的纠正机制。
神经网络量化虽降低计算开销，但即使量化感知训练也可能改变原始浮点网络的分类结果。本文借助验证构建推理时纠正系统：以最大分类置信度过近似不一致输入空间，提出CoMPAQt，用混合整数线性规划编码量化、定制线性松弛，并联合量化与浮点网络计算以剪枝，计算该置信度。基于此提出两种纠正机制：逐级提高位精度以保证返回浮点网络分类，或用量化网络集成缓解不一致。在MNIST、ACAS-Xu、表格数据集及全连接和卷积网络上评估，第一种机制保证100%分类一致性且平均降低3.8倍计算开销，第二种近乎完美一致且降低4.1倍；这是首个为量化网络分类一致性提供形式化保证的工作。
Despite the wide success of neural networks, their computational cost is very high. Quantization techniques reduce this cost, but it can result in changing the classifications of the original floating-point network, even if the training is quantization-aware. In this work, we rely on verification to design correction systems that detect classification inconsistencies at inference time and eliminate them. The key idea is to overapproximate the space of inconsistent inputs with their maximal classification confidence. The main challenge in computing this confidence is that it involves analyzing a quantized network, which introduces a very high degree of nonlinearity, over all possible inputs. We propose CoMPAQt , an algorithm for computing this confidence. CoMPAQt relies on a novel encoding of quantization in mixed-integer linear programming (MILP), along with customized linear relaxations to reduce the high complexity. To prune the search space, it ties the computations of the quantized network and its floating-point counterpart. Given this confidence, we propose two correction mechanisms. The first mechanism guarantees to return the classification of the floating-point network and relies on networks with increasing bit precisions. The second mechanism mitigates classification inconsistencies by an ensemble of quantized networks. We evaluate our approach on MNIST, ACAS-Xu, and tabular datasets over fully connected and convolutional networks. Results show that our first correction mechanism guarantees 100% consistency with the floating-point network's classifications while reducing its computational cost by 3.8x, on average. Our second mechanism reaches an almost perfect consistency guarantee in our experiments while reducing the computational cost by 4.1x. Our work is the first to provide a formal guarantee on the classification consistency of a quantized network.
@article{paperbot2978,
title = {Quantization with Guaranteed Floating-Point Neural Network Classifications},
author = {Anan Kabaha and Dana Drachsler Cohen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763118}
}