Print Email Facebook Twitter Robustness Verification for Classifier Ensembles Title Robustness Verification for Classifier Ensembles Author Gross, D. Jansen, N. Perez, G.A. Raaijmakers, S. Contributor Sokolsky, D.V. (editor) Hung, O. (editor) Publication year 2020 Abstract We give a formal verification procedure that decides whether a classifier ensemble is robust against arbitrary randomized attacks. Such attacks consist of a set of deterministic attacks and a distribution over this set. The robustness-checking problem consists of assessing, given a set of classifiers and a labelled data set, whether there exists a randomized attack that induces a certain expected loss against all classifiers. We show the NP-hardness of the problem and provide an upper bound on the number of attacks that is sufficient to form an optimal randomized attack. These results provide an effective way to reason about the robustness of a classifier ensemble. We provide SMT and MILP encodings to compute optimal randomized attacks or prove that there is no attack inducing a certain expected loss. In the latter case, the classifier ensemble is provably robust. Our prototype implementation verifies multiple neural-network ensembles trained for image-classification tasks. The experimental results using the MILP encoding are promising both in terms of scalability and the general applicability of our verification procedure. Subject Adversarial attacksEnsemble classifiersRobustnessEncoding (symbols)Formal verificationInteger programmingNP-hardClassifier ensemblesData setEncodingsExpected lossFormal verification proceduresMultiple neural networksPrototype implementationsUpper BoundClassification (of information) To reference this document use: http://resolver.tudelft.nl/uuid:493ca34d-7b37-4cbb-aba2-14e2af00a856 DOI https://doi.org/10.1007/978-3-030-59152-6_15 TNO identifier 955374 Publisher Springer, Cham ISBN 9783030591519 ISSN 0302-9743 Source Automated Technology for Verification and Analysis. ATVA 2020. Lecture Notes in Computer Science Automated Technology for Verification and Analysis. ATVA 2020. Lecture Notes in Computer Science, 12302 (12302), 271-287 Document type conference paper Files To receive the publication files, please send an e-mail request to TNO Library.