Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems

arXiv:2607.15328 · cs.CR, cs.AI, cs.AR · Submitted 2026-07-16 · Read on arXiv

Taisa Kushner, Ryan McCleeary, Martin Brain

Galois Inc · Galois Inc · City St George University of London

cs.CR, cs.AI, cs.AR

Submitted: 2026-07-16

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

Quantization — 21× in this paper · explained in 12 episodes
Verification — 16× in this paper · explained in 2 episodes
Edge Devices — 4× in this paper · explained in 2 episodes
Activation Function — 3× in this paper · explained in 1 episode
Robustness — 3× in this paper · explained in 5 episodes
Formal Verification — 2× in this paper · explained in 2 episodes
Accuracy — 1× in this paper · explained in 1 episode
Benchmarking — 1× in this paper · explained in 3 episodes
Defense Advanced Research Projects Agency — 1× in this paper
Digital Twin — 1× in this paper · explained in 5 episodes
Edge AI — 1× in this paper · explained in 2 episodes
Quantization-Aware Training — 1× in this paper · explained in 3 episodes

Sources

TorchLean: Formalizing Neural Networks in Lean

Related papers