研究量化神经网络的验证复杂度，揭示其计算难度与传统网络相当。
The Complexity of Verifying Feedforward Neural Networks in Quantised Settings
- 区分三类前馈网络：有理数、固定量化、动态量化网络
- 固定精度下，两类规格验证均为NP完全，与未量化情况同阶
- 动态量化结合位级规格时，给出上界，补充已知PSPACE难结果
我们研究了在量化设置下前馈神经网络（FNNs）的验证计算复杂度。将FNN分为三类：权重为精确有理数的有理数FNN、权重来自有限精度算术的量化FNN，以及以有限精度算术评估有理数网络的动态量化FNN。考虑文献中两种规格：线性规划（LP）规格为线性约束合取，位向量（BV）规格支持位级推理，可表达非线性约束。研究结果构建了这些验证问题的复杂度图景。对于具有固定算术精度的量化FNN，无论在LP或BV规格下，验证均保持为NP完全，与有理数情形复杂度一致。对于动态量化FNN在BV规格下，我们建立了上界，补全了先前已知的PSPACE难性结果。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。