Explainable artificial intelligence - learning decision sets with sat

Tese de mestrado, Engenharia Informática (Interação e Conhecimento) Universidade de Lisboa, Faculdade de Ciências, 2018Artificial Intelligence is a core research topic with key significance in technological growth. With the increase of data, we have more efficient models that in a few seconds will inform us of their prediction on a given input set. The more complex techniques nowadays with better results are Black Box Models. Unfortunately, these can’t provide an explanation behind their prediction, which is a major drawback for us humans. Explainable Artificial Intelligence, whose objective is to associate explanations with decisions made by autonomous agents, breaks this lack of transparency. This can be done by two approaches, either by creating models that are interpretable by themselves or by creating frameworks that justify and interpret any prediction made by any given model. This thesis describes the implementation of two interpretable models (Decision Sets and Decision Trees) based on Logic Reasoners, either SAT (Satisfiability) or SMT (Satisfiability Modulo Theories) solvers. This work was motivated by an in-depth analysis of past work in the area of Explainable Artificial Intelligence, with the purpose of seeking applications of logic in this domain. The Decision Sets approach focuses on the training data, as does any other model, and encoding the variables and constraints as a CNF (Conjuctive Normal Form) formula which can then be solved by a SAT/SMT oracle. This approach focuses on minimizing the number of rules (or Disjunctive Normal Forms) for each binary class representation and avoiding overlap, whether it is training sample or feature-space overlap, while maintaining interpretable explanations and perfect accuracy. The Decision Tree model studied in this work consists in computing a minimum size decision tree, which would represent a 100% accurate classifier given a set of training samples. The model is based on encoding the problem as a CNF formula, which can be tackled with the efficient use of a SAT oracle