Formal verification of deep neural networks using learning cellular automata

Deep neural networks (DNNs) have found diverse applications such as image processing, video processing, text classification, computer vi- sion, safety-critical systems such as controllers for autonomous vehicles , etc. But for DNNs in safety-critical systems, formal verification becomes really essential before actual deployment. There have been several al- gorithms, like the Reluplex algorithm, which are limitedly scalable. It has been claimed that formal verification can be made significantly more scalable by means of intelligent parallelisation. Cellular automata (CAs) have also analysed to have some computational power and univer- sality apart from highly scaling data parallelism. Recent literature reveals that cellular automata have been studied as a black box for neural net- works to study their temporal evolution and predict the transition rules. In this article, we propose a formal verification system for deep neural networks by using equivalent learning cellular automata (LCA), a new discrete structure that incorporates all the properties of a CA associated with some learning algorithm. We provide necessary formal definitions of CAs, DNNs, and LCAs, and prove that the emulation complexity of an equivalent LCA for a given DNN is NP-complete. Finally, we describe the overall layout of the verier based on a polynomial-time approximation of the emulation, illustrated by extensive experimental results