Recent advances in machine learning (ML) have demonstrated that statistical models can be trained to recognize complicated patterns and make sophisticated decisions, often outperforming human capabilities. However, current ML-based systems sometimes exhibit faulty behavior, which prevents their use in safety-critical applications. Furthermore, the increased autonomy and complexity of ML-based systems raise additional trustworthiness concerns such as explainability. To mitigate risks associated with these concerns, the European Union has agreed on a legal framework called the AI Act that governs ML-based products that are placed on the European market.

To meet the goals set out by the AI Act with diligence, manufacturers of critical systems that leverage machine learning need new rigorous and scalable approaches to ensure trustworthiness. One natural pathway towards this aim is to leverage formal methods, a class of reasoning approaches that has proved useful in the past when arguing for safety. Unfortunately, these methods often suffer from computational scalability issues, a problem that becomes even more challenging when applied to complex ML-based systems.

This dissertation seeks to assess and improve the trustworthiness of a class of machine learning models called tree ensembles. To this end, a reasoning engine based on abstract interpretation is developed from the ground up, exploiting unique characteristics of tree ensembles for improved runtime performance. The engine is designed to support deductive and abductive reasoning with soundness and completeness guarantees, hence enabling formal verification and the ability to accurately explain why a tree ensemble arrives at a certain prediction.

Through extensive experimentation, we demonstrate speedup improvements of several orders of magnitude compared to current state-of-the-art approaches. More importantly, we show that many classifiers based on tree ensembles are extremely sensitive to additive noise, despite demonstrating high accuracy. For example, in one case study involving the classification of images of handwritten digits, we find that changing the light intensity of a single pixel in an image by as little as 0.1% causes some tree ensembles to misclassify the depicted digit. However, we also show that it is possible to compute provably correct explanations without superfluous information, called minimal explanations, for predictions made by complex tree ensembles. These types of explanations can help to pinpoint exactly which inputs are relevant in a particular classification. Moreover, we explore approaches for computing explanations that are also globally optimal with respect to a cost function, called minimum explanations. These types of explanations can be tailored for specific target audiences, e.g., for engineers trying to improve robustness, for system operators making critical decisions, or for incident investigators seeking the root cause of a hazard.

Recent advances in machine learning and artificial intelligence are now beingconsidered in safety-critical autonomous systems where software defects maycause severe harm to humans and the environment. Design organizations in thesedomains are currently unable to provide convincing arguments that their systemsare safe to operate when machine learning algorithms are used to implement theirsoftware.

In this paper, we present an efficient method to extract equivalence classes from decision trees and tree ensembles, and to formally verify that their input-output mappings comply with requirements. The idea is that, given that safety requirements can be traced to desirable properties on system input-output patterns, we can use positive verification outcomes in safety arguments.

This paper presents the implementation of the method in the tool VoTE (Verifier of Tree Ensembles), and evaluates its scalability on two case studies presented in current literature. We demonstrate that our method is practical for tree ensembles trained on low-dimensional data with up to 25 decision trees and tree depths of up to 20.Our work also studies the limitations of the method with high-dimensionaldata and preliminarily investigates the trade-off between large number of trees and time taken for verification.

In the presence of data and computational resources, machine learning can be used to synthesize software automatically. For example, machines are now capable of learning complicated pattern recognition tasks and sophisticated decision policies, two key capabilities in autonomous cyber-physical systems. Unfortunately, humans find software synthesized by machine learning algorithms difficult to interpret, which currently limits their use in safety-critical applications such as medical diagnosis and avionic systems. In particular, successful deployments of safety-critical systems mandate the execution of rigorous verification activities, which often rely on human insights, e.g., to identify scenarios in which the system shall be tested.

A natural pathway towards a viable verification strategy for such systems is to leverage formal verification techniques, which, in the presence of a formal specification, can provide definitive guarantees with little human intervention. However, formal verification suffers from scalability issues with respect to system complexity. In this thesis, we investigate the limits of current formal verification techniques when applied to a class of machine learning models called tree ensembles, and identify model-specific characteristics that can be exploited to improve the performance of verification algorithms when applied specifically to tree ensembles.

To this end, we develop two formal verification techniques specifically for tree ensembles, one fast and conservative technique, and one exact but more computationally demanding. We then combine these two techniques into an abstraction-refinement approach, that we implement in a tool called VoTE (Verifier of Tree Ensembles).

Using a couple of case studies, we recognize that sets of inputs that lead to the same system behavior can be captured precisely as hyperrectangles, which enables tractable enumeration of input-output mappings when the input dimension is low. Tree ensembles with a high-dimensional input domain, however, seems generally difficult to verify. In some cases though, conservative approximations of input-output mappings can greatly improve performance. This is demonstrated in a digit recognition case study, where we assess the robustness of classifiers when confronted with additive noise.

Recent advances in machine learning are now being considered for integration in safety-critical systems such as vehicles, medical equipment and critical infrastructure. However, organizations in these domains are currently unable to provide convincing arguments that systems integrating machine learning technologies are safe to operate in their intended environments.

In this paper, we present a formal verification method for tree ensembles that leverage an abstraction-refinement approach to counteract combinatorial explosion. We implemented the method as an extension to a tool named VoTE, and demonstrate its applicability by verifying the robustness against perturbations in random forests and gradient boosting machines in two case studies. Our abstraction-refinement based extension to VoTE improves the performance by several orders of magnitude, scaling to tree ensembles with up to 50 trees with depth 10, trained on high-dimensional data.

Recent advances in machine learning and artificial intelligence are now being applied in safety-critical autonomous systems where software defects may cause severe harm to humans and the environment. Design organizations in these domains are currently unable to provide convincing arguments that systems using complex software implemented using machine learning algorithms are safe and correct.

In this paper, we present an efficient method to extract equivalence classes from decision trees and random forests, and to formally verify that their input/output mappings comply with requirements. We implement the method in our tool VoRF (Verifier of Random Forests), and evaluate its scalability on two case studies found in the literature. We demonstrate that our method is practical for random forests trained on low-dimensional data with up to 25 decision trees, each with a tree depth of 20. Our work also demonstrates the limitations of the method with high-dimensional data and touches upon the trade-off between large number of trees and time taken for verification.

The ability to reliably explain why a machine learning model arrives at a particular prediction is crucial when used as decision support by human operators of critical systems. The provided explanations must be provably correct, and preferably without redundant information, called minimal explanations. In this paper, we aim at finding explanations for predictions made by tree ensembles that are not only minimal, but also minimum with respect to a cost function.

To this end, we first present a highly efficient oracle that can determine the correctness of explanations, surpassing the runtime performance of current state-of-the-art alternatives by several orders of magnitude. 

Secondly, we adapt an algorithm called MARCO from the optimization field (calling the adaptation m-MARCO) to compute a single minimum explanation per prediction, and demonstrate an overall speedup factor of 2.7 compared to a state-of-the-art algorithm based on minimum hitting sets, and a speedup factor of 27 compared to the standard MARCO algorithm which enumerates all minimal explanations.