QuantifyML: How good is my machine learning model?

This paper presents an approach, QuantifyML, which employs
model counting to assess the learnability and robustness of machine
learning models. Typically the efficacy of machine learning
models is determined by computing their accuracy statistically on
test data sets. However, this may be misleading, if the test data is
not representative of the problem that is being studied. Further,
two different models may have the same accuracy on a given data
set, measured statistically, but may be very different in their behavior
on unseen data. Also, models with high accuracy could have
poor adversarial robustness. In QuantifyML, our goal is to precisely
quantify the extent to which machine learning models have learned
and generalized from the given data. In QuantifyML, a trained
model is translated into a C program, which is fed to the CBMC
model checking tool to produce a formula in Conjunctive Normal
Form (CNF), which in turn is analyzed with state-of-the-art model
counters to efficiently obtain precise counts w.r.t different outputs.
QuantifyML enables i) evaluating the learnability of models by
comparing the counts for the outputs to ground truth, expressed
as logical predicates (if available), ii) comparing the performance
of different models that may be built with different machine learning
algorithms (e.g., decision-trees vs. neural networks), and iii)
quantifying the robustness of trained models around given inputs.
Our evaluation demonstrates these applications of QuantifyML
on decision trees and neural networks trained to learn relational
properties of graphs, for which we know the ground truth, and to
perform image classification, for which we do not have the ground
truth, but we can quantify local robustness.