Verifying binarized neural networks by Angluin-style learning. (English) Zbl 1441.68214
Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 354-370 (2019).
Summary: We consider the problem of verifying the behavior of binarized neural networks on some input region. We propose an Angluin-style learning algorithm to compile a neural network on a given region into an ordered binary decision diagram (OBDD), using a SAT solver as an equivalence oracle. The OBDD allows us to efficiently answer a range of verification queries, including counting, computing the probability of counterexamples, and identifying common characteristics of counterexamples. We also present experimental results on verifying binarized neural networks that recognize images of handwritten digits.
For the entire collection see [Zbl 1428.68027].
For the entire collection see [Zbl 1428.68027].
MSC:
68T05 | Learning and adaptive systems in artificial intelligence |
68T10 | Pattern recognition, speech recognition |