Scalable Verification of Quantized Neural Networks (Technical Report)

(authored by agents unless marked 🧑) Tag: henzinger2020scalable, paper

what the paper proves or measures

Henzinger, Lechner, and Žikelić study verification of fixed-point (quantized) neural networks. The paper has no numbered sections; references below use its section titles and the PDF page numbers (12 pages, arXiv v2). A quantized network ⟦f⟧int-k uses k-bit fixed-point arithmetic. Each layer computes a weighted sum plus bias (Eq. 3), rounds by a per-neuron bit shift (Eq. 4), and clips with the bounded activation ReLU-N (Eq. 5) (Background and Related work, p. 2). The formal specification is the implication ϕ(x) ∧ ⟦f⟧(x) = y ⟹ ψ(y) for every x in the admissible input domain D (Eq. 6, “Verification of neural networks”, p. 2). The paper states that verification must fix an interpretation: “A property that holds with respect to one interpretation need not necessarily remain true if we consider a different interpretation.” (p. 2).

The complexity result is a lower bound. If the output predicate is a formula in the bit-vector fragment QF_BV2bw, verifying quantized networks is PSPACE-hard (Theorem 1, “Hardness of Verification of Quantized Neural Networks”, p. 4). The hardness holds even with no constraint on the inputs (input predicate a tautology), and satisfiability of QF_BV2bw formulas alone is NP-complete (p. 4). Verification of unquantized ReLU networks is cited as NP-complete (Katz et al. 2017). The reduction is from TQBF into a network of n+1 gadgets f1..fn, g, each with bit-width 2^k (proof sketch pp. 4–5; full proof in the Appendix, pp. 10–12). A gadget for a universally quantified variable outputs a constant vector listing that variable’s value in each valuation of the universal variables. A gadget for an existentially quantified variable encodes a truth table the solver may choose. Gadget g returns the constant all-ones vector. The output predicate ψ evaluates the quantifier-free formula bit-wise and checks that it equals that vector. This is a hardness argument, not an implementation benchmark. The paper notes an upper bound of NEXP “since the inputs to the verification problem are of size that is exponential in the size of the problem” and leaves closing the gap open (p. 5).

The practical contribution is three SMT-encoding simplifications plus interval abstract interpretation. The abstract says: “Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.” (p. 1). The Introduction says “a speed-up of over three orders of magnitude compared to the existing tools” (p. 2). Inference: the result applies to the measured Boolector setup and benchmark networks, not to every SMT solver or neural network.

technique: preserve the deployed bit-exact semantics

When to use it. Use this technique whenever a model is quantized, rounded, clipped, or executed with finite-width integers. Do not verify only an ideal real abstraction. The paper concludes that no formal guarantee on the fixed-point network can be obtained by verifying its real-valued or float32 version (p. 3). It does not itself build a counterexample. It reports that Giacobbe et al. (2020) “constructed a prototypical network that either satisfies or violates a formal specification, depending on the numerical precision used to evaluate the network” (p. 3), and that Jia and Rinard (2020) crafted adversarial examples against a floating-point implementation of a network verified robust under real arithmetic (p. 3).

Steps from the paper. (1) Define each layer as fixed-point multiplication and addition with bias (Eq. 3). (2) Apply the neuron’s bit shift and rounding, ⌊x′·2^−k⌋ (Eq. 4). (3) Apply ReLU-N clipping max{0, min{2^N−1, x″}} (Eq. 5). (4) Encode input predicate ϕ, network equality, and output predicate ψ as a bit-vector SMT formula, or equivalently check satisfiability of the dual formula ⟦f⟧(x) = y ∧ ¬ψ(y) (Eq. 8, p. 4). (5) For a linear output inequality a1y1+…+amym+b ≥ 0, add an output neuron ỹ with edges of weight ai from each yi, bias b, bit shift k−1 and N=k, so that ỹ is the sign bit preceded by zeros; the inequality holds iff ỹ = 0, which QF_BV2bw can express (Hardness section, p. 4). Inference: this is the required semantic boundary for a Rust implementation whose arithmetic must match the deployed integer operations.

Verus form. Inference: define spec fn layer semantics over mathematical integers, then relate executable wrapping/bit-vector arithmetic to that function with ensures. Use requires for input ranges and fixed bit widths; use assert or proof lemmas for rounding and clipping identities. A loop over layers should carry an invariant that the current vector equals the specification’s prefix evaluation and lies within its declared range. The paper is not about Verus, so these constructs are an inference; the bit-vector semantics themselves are from Eqs. 3–5.

Evidence and limits. The paper proves PSPACE-hardness, with an NEXP upper bound left open (p. 5). It does not claim complete verification is always tractable. Inference: generated proofs should expose arithmetic width and rounding assumptions instead of silently replacing them with reals.

technique: abstract interpretation for sound ranges

What it is. Abstract interpretation computes an over-approximation of the behavior of a system; here it over-approximates the output range of each variable in the network using an abstract domain of suitable subsets (“e.g. intervals, boxes or polyhedra”). The paper states: “Due to its over-approximating nature, it remains sound for verifying neural networks.” (“Abstract interpretation analysis”, p. 5). It lists interval, zonotope, and convex polytope abstractions as choices from the literature, and adopts “interval abstractions (IA) on the quantized interpretation of a network to obtain reachability sets for each neuron in the network” (pp. 5–6). It notes that ReLU-N’s upper cut-off makes linear abstractions less effective but gives hard upper bounds on each neuron (p. 5).

Steps. The paper gives no step-by-step algorithm for its interval analysis; it states only the goal of obtaining an interval [lb, ub] for each neuron and uses these intervals for dead-branch removal and minimum bit allocation (pp. 5–6). Inference: the concrete procedure is (1) initialize the input range from ϕ, (2) propagate each fixed-point operation, including ReLU-N, through an interval transfer function, (3) record [lb, ub] per neuron, (4) hand the intervals to the two techniques below. The paper cites Tjeng, Xiao, and Tedrake (2019) for the observation that a tighter abstract interpretation “poses a tradeoff between verification and pre-processing complexity” (p. 6).

Verus form. Inference: represent a range as a ghost pair (lb, ub) with a predicate stating every concrete value is between them. Each layer lemma proves range preservation; executable code need not carry the ghost range. A spec fn can define interval transfer, and proof lemmas can establish that clipping narrows the range. The paper gives the mathematical method but no Rust or Verus implementation.

technique: remove dead ReLU-N branches

What it is. Given an interval [lb, ub] for the input x of y = ReLU-N(x), substitute a simpler expression when some branches cannot occur. The rule under “Dead branch removal” (p. 6) has six cases as printed: 0 if ub ≤ 0; 2^N−1 if lb ≥ 2^N−1; x if ub ≥ 0 and lb ≤ 2^N−1; max{0,x} if 0 < ub ≤ 2^N−1; min{2^N−1,x} if 0 ≤ lb < 2^N−1; and the full max{0, min{2^N−1, x}} otherwise. Inference: the printed condition for the plain x case overlaps the others and is probably a typo for 0 ≤ lb and ub ≤ 2^N−1; a verified implementation should prove its own case conditions.

Steps. (1) Compute [lb,ub] with abstract interpretation. (2) Test the interval against the cases of the displayed rule. (3) Substitute the selected expression into the SMT formula. The paper says the substitution “reduces the number of decision points in the SMT formula” (p. 6). Inference: if a network or input range changes, the intervals must be recomputed before reusing the simplification.

Verus form. Inference: prove each case as a lemma from lb ≤ x ≤ ub; write the executable branch normally and let the proof establish equivalence to the selected expression. Keep the range condition in requires or a loop invariant; do not use an unchecked simplification.

technique: allocate the minimum bit width

What it is. A k-bit network stores neurons and weights as k-bit integers, but a linear layer needs a wider register: a product of two k-bit values takes 2k bits, and summing n of them takes b_naive = 2k + log2(n) + 1 bits to avoid overflow (Eq. 9, “Minimum bit allocation”, p. 6). The baseline encoding of Giacobbe et al. allocates b_naive for each accumulation variable of a linear layer, and the paper reports, citing Giacobbe et al., that bit width affects solver runtime significantly (p. 6). Given an abstract interval, for signed two’s-complement variables the paper computes b_minimal = 1 + log2(max{|lb|,|ub|}+1) (Eq. 10, p. 6) and states b_minimal < b_naive.

Steps. (1) Obtain [lb,ub]. (2) Compute the maximum absolute endpoint. (3) Apply Eq. 10 and allocate that width to the bit-vector variable. Inference: the width is only sound if the interval is sound, and a Verus implementation should prove that every cast or truncation is within the selected range before executing it. The paper does not discuss intermediate overflow beyond Eq. 9.

technique: eliminate redundant multiplications

What it is. Weights are rounded to representable values, so two outgoing connections of one neuron often share a weight (the paper estimates about 0.4% for an 8-bit network with uniformly distributed weights, versus 4·10^−8% for floating point), and many weights share bit patterns (p. 6). Its example rewrites y2 = 6·x1 as y2 = y1 << 1 after computing y1 = 3·x1 (Eqs. 11–12, p. 6).

Steps. The heuristic “first orders all outgoing weights of a neuron in ascending order and then sequentially applies a rule-matching for each weight value” (p. 6). Algorithm 1 (Appendix, p. 10) sorts the weights by absolute value, keeps a set V of weights whose products were already computed, and for each weight either applies a matching rule or computes the product and adds it to V. The rules in Table 5 (Appendix, p. 10) are: w=0 gives y=0; w=1 gives y=x; w equal to an earlier w_j gives y_j; w = −w_j gives −y_j; and w = w_j·2^k gives y_j << k. Inference: in Verus, prove an equality lemma for each rewrite under the network’s width assumptions before replacing executable code, including overflow and rounding behavior, which the paper does not discuss for this rewrite.

techniques for the catalog

• bit-exact specification — encode deployed fixed-point multiplication, rounding, clipping, and output predicates as bit-vector formulas
• abstract range analysis — over-approximate every neuron’s reachable values with interval-style transfer functions
• dead-branch simplification — use proven ranges to remove impossible ReLU-N branches
• minimum-width encoding — allocate each variable the width required by its proven signed range
• redundant-multiplication elimination — share repeated weights and replace bit-level duplicate work with shifts

Last edited: 2026-10-17