Ensuring a machine learning model’s trustworthiness is crucial to prevent potential harm. One way to foster trust is through the formal verification of the model’s adherence to essential design requirements. However, this approach relies on well-defined, application-domain-centric criteria with which to test the model, and such specifications may be cumbersome to collect in practice. We propose a data-driven approach for creating specifications to evaluate a trained model effectively. Implementing this framework allows us to prove that the model will exhibit safe behavior while minimizing the false-positive prediction rate. This strategy enhances predictive accuracy and safety, providing deeper insight into the model’s strengths and weaknesses, and promotes trust through a systematic approach.

Crowdsourcing and weak supervision offer methods to efficiently label large datasets. Our work builds on existing weak supervision models to accommodate ordinal target classes, in an effort to recover ground truth from weak, external labels. We define a parameterized factor function and show that our approach improves over other baselines.

In recent years, there have been major strides in the safety verification of machine learning models such as neural networks and tree ensembles. However, fuzzy decision trees (FDT), also called soft or differentiable decision trees, are yet unstudied in the context of verification. They present unique verification challenges resulting from multiplications of input values; in the simplest case with a piecewise-linear splitting function, an FDT is piecewise-polynomial with degree up to the depth of the tree. We propose an abstraction-refinement algorithm for verification of properties of FDTs. We show that the problem is NP-Complete, like many other machine learning verification problems, and that our algorithm is complete in a finite precision setting. We benchmark on a selection of public data sets against an off-the-shelf SMT solver and a baseline variation of our algorithm that uses a refinement strategy from similar methods for neural network verification, finding the proposed method to be the fastest. Code for our algorithm along with our experiments and demos are available on GitHub athttps://github.com/autonlab/fdt_verification.

We recommend using a model-centric, Boolean Satisfiability (SAT) formalism to obtain useful explanations of trained model behavior, different and complementary to what can be gleaned from LIME and SHAP, popular data-centric explanation tools in Artificial Intelligence (AI).We compare and contrast these methods, and show that data-centric methods may yield brittle explanations of limited practical utility.The model-centric framework, however, can offer actionable insights into risks of using AI models in practice. For critical applications of AI, split-second decision making is best informed by robust explanations that are invariant to properties of data, the capability offered by model-centric frameworks.

We consider the problem of identifying discrepancies between training and test data which are responsible for the reduced performance of a classification system. Intended for use when data acquisition is an iterative process controlled by domain experts, our method exposes insufficiencies of training data and presents them in a user-friendly manner. The system is capable of working with any classification system which admits diagnostics on test data. We illustrate the usefulness of our approach in recovering compact representations of the revealed gaps in training data and show that predictive accuracy of the resulting models is improved once the gaps are filled through collection of additional training samples.