How Many Bits Keep a Neural Network Controller Safe? Error-Margin Conditions, Sound Certificates and the Seed Lottery in Quantized Neural Feedback Control
A neural network controller stored with few bits can lose the safety proof of its full-precision version, and whether it does depends on the training seed. We prove that an invariant ellipsoid survives weight rounding if the control error stays below a state-dependent contraction slack, and that the constant in the simplified global form is sharp. We bound the error between two ReLU networks soundly by propagating intervals for their difference, and we add a verifier for saturated plants that are affine in the control, using full CROWN bounds, a clip relaxation and an exact bound over the ellipse. On a nonlinear pendulum and a four-state vehicle model, with 15 trained networks each, a weight-norm formula asks for about 15 bits where 4 suffice. Direct proofs of the rounded network need 3.8 and 4.3 bits, and error-margin certificates need 5.3 and 8.0 bits. At 3 bits only 5 of 15 post-training-quantized pendulum networks are provably safe, against 15 of 15 after quantization-aware training, while a fine-tuning control without rounding stays at 5.
Authors
- Singh Viren (ORCID: https://orcid.org/0009-0001-6618-0126)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-10-26
- DOI
- https://doi.org/10.5281/zenodo.23661796
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00