Robustness Verification of Decision Tree Ensembles.
Francesco Ranzato, Marco Zanella · Padua Research Archive (University of Padova) · 2019
We study the problem of formally and automatically verifying robustness properties of decision tree ensemble classifiers such as random forests and gradient boosted decision tree models.A recent stream of works showed how abstract interpretation can be successfully deployed to formally verify neural networks.In this work we push forward this line of research by designing a general abstract interpretationbased framework for the formal verification of robustness and stability properties of decision tree ensemble models.Our method may induce complete robustness checks of standard adversarial perturbations or output concrete adversarial attacks.We implemented our abstract verification technique in a tool called silva, which leverages an abstract domain of not necessarily closed real hyperrectangles and is instantiated to verify random forests and gradient boosted decision trees.Our experimental evaluation on the MNIST dataset shows that silva provides a precise and efficient tool which advances the current state-of-the-art in tree ensembles verification.