  Deep neural networks (DNNs) have become the technology of choice for
realizing a variety of complex tasks. However, as highlighted by many recent
studies, even an imperceptible perturbation to a correctly classified input can
lead to misclassification by a DNN. This renders DNNs vulnerable to strategic
input manipulations by attackers, and also oversensitive to environmental
noise.
  To mitigate this phenomenon, practitioners apply joint classification by an
*ensemble* of DNNs. By aggregating the classification outputs of different
individual DNNs for the same input, ensemble-based classification reduces the
risk of misclassifications due to the specific realization of the stochastic
training process of any single DNN. However, the effectiveness of a DNN
ensemble is highly dependent on its members *not simultaneously erring* on many
different inputs.
  In this case study, we harness recent advances in DNN verification to devise
a methodology for identifying ensemble compositions that are less prone to
simultaneous errors, even when the input is adversarially perturbed --
resulting in more robustly-accurate ensemble-based classification.
  Our proposed framework uses a DNN verifier as a backend, and includes
heuristics that help reduce the high complexity of directly verifying
ensembles. More broadly, our work puts forth a novel universal objective for
formal verification that can potentially improve the robustness of real-world,
deep-learning-based systems across a variety of application domains.
