We investigate the computational complexity of neural network verification in quantised settings. We distinguish three classes of Feedforward Neural Networks (FNNs): rational FNNs with exact rational weights, quantised FNNs whose weights come from a finite-width arithmetic, and dynamically quantised FNNs in which rational networks are evaluated with respect to a given finite-width arithmetic. We consider two types of specifications used in the literature. Linear programming (LP) specifications are conjunctions of linear constraints, while bit-vector (BV) specifications allow reasoning at the bit level and can express non-linear constraints. Our results give a complexity landscape of these verification problems. For quantised FNNs with fixed arithmetic precision, we show that verification under both LP and BV specifications remains NP-complete, matching the complexity of the rational case. For dynamically quantised FNNs with BV specifications, we establish upper bounds, complementing a previously known PSPACE-hardness result.

翻译：我们研究了量化设置下神经网络验证的计算复杂性。我们区分了三类前馈神经网络（FNN）：具有精确有理权重的有理FNN、权重来自有限宽算术系统的量化FNN，以及基于给定有限宽算术系统对有理网络进行评估的动态量化FNN。我们考虑了文献中使用的两类规范。线性规划（LP）规范是线性约束的合取，而位向量（BV）规范允许在位级推理，并可表达非线性约束。我们的研究结果描绘了这些验证问题的复杂性全貌。对于具有固定算术精度的量化FNN，我们证明在LP和BV规范下的验证仍然属于NP完全问题，与有理情况下的复杂性相匹配。对于具有BV规范的动态量化FNN，我们建立了上界，补充了先前已知的PSPACE-硬度结果。