A trained weight is a real number. Hardware would rather it were a byte. Quantization forces the continuous weight onto a coarse integer grid so a float model can run in 8-bit integer arithmetic only — the trick behind on-device inference. The scheme is runnable: pick a scale s = max|x| / 127, snap each weight to the nearest of 255 rungs, and read back x̂ = s·q. Down the center, data flows: the floats go in, the grid snaps them, the integers come out. The blue team proves the rounding bound; the red team swaps rounding for truncation to break it.
source Jacob et al., Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference (2017) — arxiv.org/abs/1712.05877. Rendered, not quoted.
No lookup table. Three lines of arithmetic on a float vector x:
s = max|x| / qmax (qmax=127 for int8, 7 for int4)
q = clamp( round(x / s), −qmax, +qmax )
x̂ = s · q — the dequantized value
Five things must hold, and the witness re-proves them live:
| invariant | holds |
|---|
This sphere is the-floating-point compressed to integers. There, a real number was already an approximation — a sign, an exponent, a 23-bit mantissa on a logarithmic grid. Here we throw the exponent away entirely: one shared scale s, a linear grid of 255 rungs, and a plain signed byte for each weight.
The float carried its own scale per number; the int8 tensor shares one scale across the whole vector. That is the whole compression — and the whole risk. Each sphere is the next one's premise.
The blue team's live check: re-quantize the current vector, verify the rounding bound |x−x̂| ≤ s/2 on every element, and confirm int8 beats int4. If red swaps round for floor, this badge is where it shows.
The input is a vector of trained real-valued weights — what a float32 layer actually holds. The current tensor:
One shared scale s is derived from the single largest magnitude in this vector. Every element is then measured in units of that scale. That is what you feed the panel below.
int8: 255 rungs. The largest weight lands exactly on ±127; every other weight rounds to the nearest rung.
| x | q | x̂ = s·q | |x−x̂| |
|---|
Change the bit-width or the vector — every q, every x̂, and the error bound are computed from the three formulas on the spot, never looked up.
What the machine produces, proven: a vector of signed integers plus one scale s — the float tensor now fits in a quarter of the bytes, and the reconstruction error is bounded: every |x−x̂| ≤ s/2, the max weight uses the full range, zero stays exactly zero, and int8 error is strictly below int4 error on the same vector.
The blue team's witness (left) re-proves these bounds live; the red team (right) tries to break the rounding step.
Symmetric quantization also wastes a rung on activations that are one-sided (post-ReLU ≥ 0) — that is why the paper uses an asymmetric scheme with a zero-point for activations. And the hard part isn't the weights: it's keeping accuracy through quantized matmuls, which needs quantization-aware training, not a post-hoc snap.
"8 bits is 32× smaller than float32." Cut. It is 4× — 8 bits vs 32. The speed win is integer arithmetic, not a 32× size drop.
"Quantization is just rounding the weights." Cut. Weights are the easy half. The paper's contribution is integer-only matmul plus a training procedure; a naive round loses accuracy.
"Nearest-rung rounding is optional." Kept, corrected. It is load-bearing: round guarantees error ≤ s/2; truncation (floor) lets it reach s — exactly the tamper in window 6.
The red team's move: replace round() with floor() — truncate toward zero-ish instead of snapping to nearest. The blue team's witness (window 7) is watching the s/2 bound.
Truncation biases every weight downward; the error can reach a full step s, breaking |x−x̂| ≤ s/2. The witness recomputes, finds a violated element, and turns red. Nothing is faked; the attack is real and it is caught.