发表机构
George Mason University（乔治梅森大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出mBFV验证框架，通过多参数边界传播与分支定界技术，高效证明神经网络对多参数位翻转扰动的鲁棒性，显著优于现有单参数验证器，可扩展到百万参数网络。
AI 中文摘要
硬件故障可能翻转量化神经网络中存储权重的比特位，从而可能损害其预测性能。尽管此类故障通常同时影响多个参数，但现有的验证器由于大型网络中可能的翻转位置存在组合爆炸，仅限于处理单参数扰动。我们提出了mBFV（多比特翻转验证器），一种高效的验证框架，能够证明针对多个参数同时发生比特翻转的鲁棒性，而无需显式枚举这些组合。mBFV通过一种新颖的多参数边界传播技术实现这一点，该技术直接聚合m个最坏情况贡献。为进一步收紧这些边界，mBFV采用了一种基于分支定界的机制来处理扰动位置，将潜在的翻转划分为更小的神经元组。在625个实例上的评估中，mBFV成功验证了293个，显著优于先前的单参数验证器（38个已验证实例）和精确混合整数线性规划基线（0个已验证实例）。值得注意的是，虽然这些基线仅限于小型网络（最多13k参数）上的单参数翻转，mBFV能够扩展到验证具有多达115万参数的网络，并应对多达四个同时发生的参数翻转。
英文摘要
Hardware faults can flip bits in the stored weights of a quantized neural network, potentially compromising its predictions. While such faults typically affect multiple parameters simultaneously, existing verifiers are limited to single-parameter perturbations due to the combinatorial explosion of possible flip locations in large networks. We present mBFV (m-BitFlip Verifier), an efficient verification framework that proves robustness against simultaneous bit flips across multiple parameters without explicitly enumerating these combinations. mBFV achieves this via a novel multi-parameter bound propagation technique that directly aggregates the m worst-case contributions. To further tighten these bounds, mBFV employs a branch-and-bound mechanism over perturbation locations, partitioning the potential flips to smaller groups of neurons. Evaluated on 625 instances, mBFV successfully verifies 293, significantly outperforming a prior single-parameter verifier (38 verified instances) and an exact mixed-integer linear programming baseline (0 verified instances). Notably, while these baselines are restricted to single-parameter flips on small networks (up to 13k parameters), mBFV scales to verify networks with up to 1.15M parameters against up to four simultaneous parameter flips.
