  Machine learned models often must abide by certain requirements (e.g.,
fairness or legal). This has spurred interested in developing approaches that
can provably verify whether a model satisfies certain properties. This paper
introduces a generic algorithm called Veritas that enables tackling multiple
different verification tasks for tree ensemble models like random forests (RFs)
and gradient boosting decision trees (GBDTs). This generality contrasts with
previous work, which has focused exclusively on either adversarial example
generation or robustness checking. Veritas formulates the verification task as
a generic optimization problem and introduces a novel search space
representation. Veritas offers two key advantages. First, it provides anytime
lower and upper bounds when the optimization problem cannot be solved exactly.
In contrast, many existing methods have focused on exact solutions and are thus
limited by the verification problem being NP-complete. Second, Veritas produces
full (bounded suboptimal) solutions that can be used to generate concrete
examples. We experimentally show that Veritas outperforms the previous state of
the art by (a) generating exact solutions more frequently, (b) producing
tighter bounds when (a) is not possible, and (c) offering orders of magnitude
speed ups. Subsequently, Veritas enables tackling more and larger real-world
verification scenarios.
