Model-Centric Verification of Artificial Intelligence

Abstract

This work shows how provable guarantees can be used to supplement probabilistic estimates in the context of Artificial Intelligence (AI) systems. Statistical techniques measure the expected performance of a model, but low error rates say nothing about the ways in which errors manifest. Formal verification of model adherence to design specifications can yield certificates which explicitly detail the operational conditions under which violations occur. These certificates enable developers and users of AI systems to reason about their trained models in contractual terms, eliminating the chance that otherwise easily preventable harm be inflicted due to an unforeseen fault leading to model failure. As an illustration of this concept, we present our verification pipeline named Tree Ensemble Accreditor (TEA). TEA leverages our novel Boolean Satisfiability (SAT) formalism for voting tree ensemble models for classification tasks. Our formalism yields disruptive speed gains over related tree ensemble verification techniques. The efficiency of TEA allows us to verify harder specifications on models of larger scales than reported in literature.

In a radiation safety context, we show how Local Adversarial Robustness (LAR) of trained models on validation data points can be incorporated into the model selection process. We explore the relationship between prediction outcome and model robustness, allowing us to yield the definition of LAR that best satisfies the engineering desiderata that the model should be robust only when it makes correct predictions. In an algorithmic fairness context, we show how Global Individual Fairness (GIF) can be tested, both in and out of data support. When the model violates the GIF specification, we enumerate all counterexamples to the formula so we may reveal the structure of unfairness that is absorbed by the model during training. In a clinical context, we show how a Safety-Paramount Engineering Constraint (SPEC) can be satisfied simply by tuning the prediction threshold of the tree ensemble. This facilitates a pareto-optimal selection of prediction threshold such that false positives cannot be reduced further without compromising safety of the system.

The goal of this thesis is to investigate if formal verification of trained models can answer a wide range of existing questions about real-world systems. Our methods are meant for those who are ultimately responsible for ensuring the safe operation of AI in their particular context. By expanding current practice in Verification and Validation (V&V) for trained tree ensembles, we hope to increase real-world adoption of AI systems.