When Does Compensating Inherited Quantization Error Help? Mean-Square Guarantees for Layer-Wise Quantization and Their Limits
Tianhao Guo
cs.LG
Oct 12, 2026 · v1
cs.AI cs.IT eess.SP
TL;DR
Selected statements, including counterexamples and identities about layer-wise quantization error compensation, are machine-checked in Lean 4 with Mathlib.
Abstract
Layer-wise post-training quantization methods let each layer compensate for the quantization error inherited from earlier layers. We ask under what assumptions such compensation guarantees a network output error no larger than without it. For linear networks of any depth, with the required calibration Gram matrices invertible, if the rounding error of each layer has zero conditional mean and a deterministic second-moment map common to both schemes, as under subtractive dither on an unbounded grid, then compensation with strengths in $[0,1]$ fixed in advance gives a mean-square output error no larger than no compensation, each scheme being followed along its own trajectory. The exact gain separates error removed directly from reduced excitation of later rounding noise. Outside this setting the comparison can fail. With rectified linear activations it fails for two independent reasons: noise changes activation states, and, even when no state changes, the correction moves error from samples on which a unit is inactive to samples on which it is active. With stable activations, commutators between the calibration projection and the activation patterns bound the excess. With a bounded codebook, even unique exact layer-wise minimizers with no overload can give a larger output error. For fixed rounding errors it already fails for two scalar linear layers, refuting a published universal guarantee. An exact residual identity gives the necessary and sufficient condition on a common layer input. All these comparisons hold the calibration input fixed. On two 8B models at 4 bits, fixed half-strength compensation beat uncompensated rounding in every model, text and draw tested, yet no rule for choosing the strength beat a layer-wise rule consistently, and lowering the full-network loss on the data used to choose did not reliably lower it on new text.
Problem
Layer-wise post-training quantization methods such as QEP let each layer compensate for quantization error inherited from earlier layers. It is unclear under what assumptions this compensation guarantees a network output error no larger than without it. A published universal guarantee claims that it always does.
Approach
An exact residual identity decides, on a common input, when a correction of a given strength helps. Mean-square comparisons are proved for linear networks under zero-conditional-mean rounding errors with a common second-moment map, as produced by subtractive dither. Explicit counterexamples are built for ReLU networks, bounded codebooks and fixed rounding errors. A commutator condition bounds the excess error. Some results are checked in a scoped Lean 4/Mathlib formalization, and experiments are run on synthetic networks and two 8B LLMs at 4 bits.
Results
Compensation provably helps in mean square for linear networks of any depth. It can fail for ReLU networks, for exact minimizers over a bounded codebook, and for fixed errors even with two scalar layers, which refutes the published QEP guarantee. On the 8B models, half-strength compensation beat uncompensated rounding in every model, text and draw tested, but no rule for choosing the strength was consistently better than a layer-wise rule.
