2017

Verification of Binarized Neural Networks via Inter-Neuron Factoring

Cheng, Chih-Hong, Nührenberg, Georg, Huang, Chung-Hao et al.

Understand

We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks.

The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer.
By proving the NP-hardness of finding optimal factoring as well as the hardness of PTAS approximability, we design polynomial-time search heuristics to generate factoring solutions.
The overall framework allows applying verification techniques to moderately-sized BNNs for embedded devices with thousands of neurons and inputs.

Built on

Sorting networks and their applications
K. E. Batcher · 1968
Earlier work this paper cites.
The mnist database of handwritten digits
Y. LeCun · 1998
Earlier work this paper cites.
The maximum edge biclique problem is np-complete
R. Peeters · 2003
Earlier work this paper cites.
Picosat essentials
A. Biere · 2008
Earlier work this paper cites.
ABC: An academic industrial-strength verification tool
R. Brayton and A. Mishchenko · 2010
Earlier work this paper cites.
An abstraction-refinement approach to verification of artificial neural networks
L. Pulina and A. Tacchella · 2010
Earlier work this paper cites.
Inapproximability results for maximum edge biclique, minimum linear arrangement, and sparsest cut
C. Ambühl, M. Mastrolilli, and O. Svensson · 2011
Earlier work this paper cites.
The German Traffic Sign Recognition Benchmark: A multi-class classification competition
J. Stallkamp, M. Schlipsing, J. Salmen, and C. Igel · 2011
Earlier work this paper cites.
Imagenet classification with deep convolutional neural networks
A. Krizhevsky, I. Sutskever, and G. E. Hinton · 2012
Earlier work this paper cites.
Overfeat: Integrated recognition, localization and detection using convolutional networks
Original
P. Sermanet, D. Eigen, X. Zhang, M. Mathieu, R. Fergus, and Y. LeCun · 2013
Earlier work this paper cites.

Similar

Yosys-a free verilog synthesis suite
C. Wolf, J. Glaser, and J. Kepler · 2013
Cited alongside, same era.
Generative adversarial nets
I. Goodfellow, J. Pouget-Abadie, M. Mirza, B. Xu, D. Warde-Farley, S. Ozair, A. Courville, and Y. Bengio · 2014
Cited alongside, same era.
Explaining and harnessing adversarial examples
Original
I. J. Goodfellow, J. Shlens, and C. Szegedy · 2014
Cited alongside, same era.
arXiv preprint arXiv:1709.06662
Original
N. Narodytska, S. P. Kasiviswanathan, L. Ryzhyk, M. Sagiv, T. Walsh. Verifying Properties of Binarized Deep Neural Networks · 2014
Cited alongside, same era.
Certification considerations for adaptive systems: Technical report
S. Bhattacharyya, D. Cofer, D. Musliner, J. Mueller, and E. Engstrom · 2015
Cited alongside, same era.
Deepdriving: Learning affordance for direct perception in autonomous driving
C. Chen, A. Seff, A. Kornhauser, and J. Xiao · 2015
Cited alongside, same era.
An empirical evaluation of deep learning on highway driving
Original
B. Huval, T. Wang, S. Tandon, J. Kiske, W. Song, J. Pazhayampallil, M. Andriluka, P. Rajpurkar, T. Migimatsu, R. Cheng-Yue, et al · 2015
Cited alongside, same era.
Fully convolutional networks for semantic segmentation
J. Long, E. Shelhamer, and T. Darrell · 2015
Cited alongside, same era.
End to end learning for self-driving cars
Original
M. Bojarski, D. D. Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. D. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, J. Zhao, and K. Zieba · 2016
Cited alongside, same era.
Binarized neural networks: Training deep neural networks with weights and activations constrained to+ 1 or-1
Original
M. Courbariaux, I. Hubara, D. Soudry, R. El-Yaniv, and Y. Bengio · 2016
Cited alongside, same era.

Then

Bitwise neural networks
Original
M. Kim and P. Smaragdis · 2016
Later among the works it cites.
Universal adversarial perturbations
Original
S.-M. Moosavi-Dezfooli, A. Fawzi, O. Fawzi, and P. Frossard · 2016
Later among the works it cites.
The cryptominisat 5 set of solvers at sat competition 2016
M. Soos · 2016
Later among the works it cites.
Maximum resilience of artificial neural networks
C.-H. Cheng, G. Nührenberg, and H. Ruess · 2017
Closest in time.
Formal verification of piece-wise linear feed-forward neural networks
R. Ehlers · 2017
Closest in time.
Safety verification of deep neural networks
X. Huang, M. Kwiatkowska, S. Wang, and M. Wu · 2017
Closest in time.
Reluplex: An efficient SMT solver for verifying deep neural networks
G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer · 2017
Closest in time.
Deep neural networks for markovian interactive scene prediction in highway scenarios
D. Lenz, F. Diehl, M. Troung Le, and A. Knoll · 2017
Closest in time.
An approach to reachability analysis for feed-forward relu neural networks
Original
A. Lomuscio and L. Maganti · 2017
Closest in time.
A fast integrated planning and control framework for autonomous driving via imitation learning
Original
L. Sun, C. Peng, W. Zhan, and M. Tomizuka · 2017
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…