Verificatie en redeneren voor ensembles van beslissingsbomen

The ability of machine-learned models to generalize to unseen data has been transformative, enabling numerous innovative applications across diverse domains. This ability is typically assessed using cross-validation techniques, which estimate a model's predictive performance by comparing its predictions to ground truth labels on an independent test set (i.e., data that the algorithm did not have access to at training time). However, as machine learning systems are increasingly deployed in high-stakes settings, the limitations of cross-validation are becoming prohibitive. In particular, cross-validation fails to capture critical performance issues. One of the most prominent examples is a model's vulnerability to adversarial examples, which are inputs that are subtly altered to cause incorrect predictions. Consequently, there is an urgent need for evaluation techniques that go beyond merely estimating a model's generalization ability. Specifically, we need reasoning techniques that are able to provide deeper insights into the model's behavior. One form of reasoning is verification, which checks whether a property such as adversarial robustness is present in a model. More broadly, we use reasoning to denote any technique that analyzes the structure of the machine-learned model with the aim of exposing weaknesses in its internals. This thesis focuses on advancing the state of the art in reasoning and verification for tree ensembles, a model family that is widely used due to its ease of configuration, strong predictive performance, and computational efficiency. Existing reasoning and verification techniques for tree ensembles are still in their early stages and face several important limitations. First, existing methods are narrowly scoped, typically addressing only a single verification task with a uniquely tailored approach. While most current systems target the adversarial setting, this focus overlooks a broader range of domain-specific verification tasks that can yield deeper insights into the model's behavior. Second, existing methods do not allow effectively balancing the time to solve and the quality of the solution, an important property given the NP-hardness of verification. Third, most existing verification systems handle multiclass classification problems incorrectly. Fourth, there is a lack of post-deployment reasoning methods for tree ensembles, despite the potential of such techniques for tasks like adversarial example detection during model operation. Fifth, there is currently no effective way to trade off model size versus its predictive performance. Verification's complexity is exponential in the number of trees and the number of leaves in each tree, so minimizing an ensemble's size is crucial for efficient verification. This thesis aims to address these limitations in the context of tree ensembles. Specifically, the thesis makes the following contributions. The first contribution introduces Veritas, an algorithm that is able to solve multiple different verification tasks by posing a large class of verification problems as a generic constrained optimization problem. We propose a novel search space and a consistent heuristic which allows anytime upper and lower bounds, the generation of concrete (counter-)examples, and fine-grained control over the time-versus-quality tradeoff. Empirically, Veritas finds better quality approximations than other approximate methods while often being faster, and is much faster than exact approaches. We released Veritas as an open-source software package. The second contribution proves that the common one-versus-other strategy used for multiclass classification problems is incorrect. The key limitation is the inability to reason about all classes simultaneously. To address this, we propose a generalization of the verification problem that directly operates in the multiclass setting. We implement this setting in Veritas by extending its scoring function and introducing a multiclass-specific consistent heuristic. The third contribution introduces OC-score, a novel reasoning method for detecting adversarial examples in a post-deployment setting that can be used to flag potential tampering when an ensemble is operating in the wild. OC-score analyzes the activation patterns of new inputs, and assesses how unusual the pattern is with respect to those of a set of reference examples. Contrary to existing methods, which often incur a significant performance hit, our method does not require additional model training. Empirically, we show that it achieves state-of-the-art performance. OC-score's source code is openly available. The final contribution proposes LOP, a compression algorithm for tree ensembles. LOP tries to find the smallest ensemble whose predictive accuracy is still within a user-provided margin of the original model. It proceeds in a level-wise manner, from the root towards the leaves, giving it the ability to cut entire trees and large subtrees from the ensemble. Empirically, we show that LOP is more effective than previous methods at reducing the size of an ensemble, and we show that this results in significant verification time improvements.