← All papers
First page of Towards Verifying Neural Networks Against Multi-Parameter Bit-Flip Perturbations

Towards Verifying Neural Networks Against Multi-Parameter Bit-Flip Perturbations

Hai Duong, Thanh Le, Ho Nguyen, ThanhVu Nguyen

cs.CR Oct 6, 2026 · v1
Soundness propositions of the bit-flip verifier (top-m bound, LP relaxation exactness, branch-and-bound correctness, propagation counting) are mechanized in Lean 4 with Mathlib.
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.

Hardware bit flips in the stored weights of quantized neural networks can change their predictions. Such faults usually affect several parameters at once, but existing verifiers handle only single-parameter perturbations because the number of flip-location combinations explodes.

mBFV extends CROWN bound propagation by recording each parameter's worst-case contribution and aggregating the m largest contributions, which avoids enumerating combinations. A branch-and-bound search over groups of neurons restricts where flips can occur, tightening the bounds. Key soundness results are mechanized in Lean 4 with Mathlib, including the top-m relaxation proposition (Proof/TopM.lean), branch-and-bound correctness, and the bound on the number of propagations.

On 625 instances, mBFV verifies 293, compared with 38 for BFAVerifier and 0 for an exact MILP baseline. It scales to networks with 1.15M parameters under up to four simultaneous parameter flips.

MethodVerified
mBFV293
BFAVerifier (single-parameter)38
MILP baseline0
Verified instances out of 625