Phiacta
ExplorePostDocsGuidesContributingAbout

Phiacta

The knowledge backend.

Contact Us
ExploreMinimax NMSE Optimality of Log-Uniform Quantization

Minimax NMSE Optimality of Log-Uniform Quantization

Among all N-level quantizers on [a,b], the log-uniform quantizer uniquely minimizes worst-case NMSE (and MSRE) over all densities. The minimax value is ε²/12 + O(ε⁴) = (R·ln2)²/(12N²). For B=8 bits, R=16 octaves: NMSE* = 1.564×10⁻⁴ (SQNR = 38.1 dB). Verified in Lean 4.

ContentIssuesEditsHistoryFilesReferences5

Minimax NMSE Optimality of Log-Uniform Quantization

This theorem is the central theoretical result of the QF8 paper. It proves that the log-uniform quantizer — the quantizer where consecutive representable values have a constant ratio — is the unique best choice when you want to minimize the worst-case NMSE (normalized mean squared error, the fraction of signal power lost to quantization) regardless of what distribution the input values follow.

This matters for ML because weight, activation, and gradient distributions vary widely across layers and training stages. A format that is optimal only for Gaussian inputs might fail on heavy-tailed gradients. Log-uniform quantization sidesteps this: it delivers the same NMSE for any input distribution.

Statement

Among all N-level quantizers on [a,b], the log-uniform quantizer uniquely minimizes the worst-case NMSE (and MSRE) over all densities:

Qlog⁡∗=arg⁡min⁡Q∈QNmax⁡f∈F[a,b]NMSE(Q,f)Q^*_{\log} = \arg\min_{Q \in \mathcal{Q}_N} \max_{f \in \mathcal{F}[a,b]} \text{NMSE}(Q, f)Qlog∗​=argQ∈QN​min​f∈F[a,b]max​NMSE(Q,f)

The minimax value is:

NMSE∗=ε212+O(ε4)=(Rln⁡2)212N2\text{NMSE}^* = \frac{\varepsilon^2}{12} + O(\varepsilon^4) = \frac{(R \ln 2)^2}{12 N^2}NMSE∗=12ε2​+O(ε4)=12N2(Rln2)2​

where ε = R·ln2/N is the bin width in the log domain, R is the dynamic range in octaves, and N is the number of quantization levels.

For B = 8 bits (N = 256), R = 16 octaves: NMSE = 1.564 × 10⁻⁴* (SQNR = 38.1 dB).

Proof Sketch

Step 1 (Density-independence / Equalization property). For the log-uniform quantizer, the cell width at any point x is proportional to x itself: w(x) ≈ x·ε. Under the high-resolution approximation:

NMSE=∫abw(x)212f(x) dx∫abx2f(x) dx=ε212∫abx2f(x) dx∫abx2f(x) dx=ε212\text{NMSE} = \frac{\int_a^b \frac{w(x)^2}{12} f(x)\,dx}{\int_a^b x^2 f(x)\,dx} = \frac{\frac{\varepsilon^2}{12}\int_a^b x^2 f(x)\,dx}{\int_a^b x^2 f(x)\,dx} = \frac{\varepsilon^2}{12}NMSE=∫ab​x2f(x)dx∫ab​12w(x)2​f(x)dx​=∫ab​x2f(x)dx12ε2​∫ab​x2f(x)dx​=12ε2​

The x² factors cancel exactly — the density f drops out completely. This is the equalization property: the log-uniform quantizer achieves the same NMSE regardless of input distribution.

Numerically verified for three test densities (log-uniform, uniform, f ∝ x²) with N=256, R=16: all give NMSE = 1.564 × 10⁻⁴ within < 0.1% deviation.

Step 2 (Non-constant φ is worse for some density). Define φ(x) = w(x)/x (relative cell width). For any non-log-uniform quantizer, φ is not constant — it must be larger somewhere and smaller elsewhere. Let x* = argmax φ(x). An adversary can concentrate the input density near x* to exploit the wider cells there, achieving MSRE > ε²/12.

Step 3 (Uniqueness). If Q ≠ Q_log, then φ is non-constant and Step 2 gives strict inequality. The log-uniform quantizer is the unique minimax optimizer.

Corollary: Minimax MSRE

The same quantizer also minimizes worst-case MSRE (mean squared relative error). The proof is identical.

Verification

Lean 4 verified (see attached proofs/MinimaxNMSE.lean): constant relative error across all bins for N=16, range [1, 256]. Perturbation tests confirm any deviation from log-uniform spacing increases the maximum error.

Metadata

Type
theorem
Visibility
public
Published
Mar 27, 2026
Last updated
Mar 27, 2026

Tags

lean-verifiedminimaxoptimalityquantizationtheorem