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

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
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

How Many Bits Keep a Neural Network Controller Safe? Error-Margin Conditions, Sound Certificates and the Seed Lottery in Quantized Neural Feedback Control

Singh Viren
Zenodo (CERN European Organization for Nuclear Research)
Formal Methods in Verification
article

How Many Bits Keep a Neural Network Controller Safe? Error-Margin Conditions, Sound Certificates and the Seed Lottery in Quantized Neural Feedback Control

Singh Viren
article en

Abstract

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.

Zenodo (CERN European Organization for Nuclear Research)
Openalex Percentile: Top 13%
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Laika access coming soon