Table of Contents
Fetching ...

ReasonX: Declarative Reasoning on Explanations

Laura State, Salvatore Ruggieri, Franco Turini

TL;DR

ReasonX, an explanation tool based on expressions in a closed algebra of operators over theories of linear constraints, provides declarative and interactive explanations for decision trees, which may represent the ML models under analysis or serve as global or local surrogate models for any black-box predictor.

Abstract

Explaining opaque Machine Learning (ML) models has become an increasingly important challenge. However, current eXplanation in AI (XAI) methods suffer several shortcomings, including insufficient abstraction, limited user interactivity, and inadequate integration of symbolic knowledge. We propose ReasonX, an explanation tool based on expressions (or, queries) in a closed algebra of operators over theories of linear constraints. ReasonX provides declarative and interactive explanations for decision trees, which may represent the ML models under analysis or serve as global or local surrogate models for any black-box predictor. Users can express background or common sense knowledge as linear constraints. This allows for reasoning at multiple levels of abstraction, ranging from fully specified examples to under-specified or partially constrained ones. ReasonX leverages Mixed-Integer Linear Programming (MILP) to reason over the features of factual and contrastive instances. We present here the architecture of ReasonX, which consists of a Python layer, closer to the user, and a Constraint Logic Programming (CLP) layer, which implements a meta-interpreter of the query algebra. The capabilities of ReasonX are demonstrated through qualitative examples, and compared to other XAI tools through quantitative experiments.

ReasonX: Declarative Reasoning on Explanations

TL;DR

ReasonX, an explanation tool based on expressions in a closed algebra of operators over theories of linear constraints, provides declarative and interactive explanations for decision trees, which may represent the ML models under analysis or serve as global or local surrogate models for any black-box predictor.

Abstract

Explaining opaque Machine Learning (ML) models has become an increasingly important challenge. However, current eXplanation in AI (XAI) methods suffer several shortcomings, including insufficient abstraction, limited user interactivity, and inadequate integration of symbolic knowledge. We propose ReasonX, an explanation tool based on expressions (or, queries) in a closed algebra of operators over theories of linear constraints. ReasonX provides declarative and interactive explanations for decision trees, which may represent the ML models under analysis or serve as global or local surrogate models for any black-box predictor. Users can express background or common sense knowledge as linear constraints. This allows for reasoning at multiple levels of abstraction, ranging from fully specified examples to under-specified or partially constrained ones. ReasonX leverages Mixed-Integer Linear Programming (MILP) to reason over the features of factual and contrastive instances. We present here the architecture of ReasonX, which consists of a Python layer, closer to the user, and a Constraint Logic Programming (CLP) layer, which implements a meta-interpreter of the query algebra. The capabilities of ReasonX are demonstrated through qualitative examples, and compared to other XAI tools through quantitative experiments.
Paper Structure (45 sections, 21 equations, 12 figures, 14 tables)

This paper contains 45 sections, 21 equations, 12 figures, 14 tables.

Figures (12)

  • Figure 1: A simple decision tree illustrating the state of a cup of water in a room at temperature $T_1$, which is warmed by a heater contributing an additional temperature $T_2$.
  • Figure 2: Workflow of data, models and explanations for reasonx. To be read from left to right. The three paths show the cases (DT-M), (DT-GS) and (DT-LS) for the base model: base model is a DT model, or a global, or a local surrogate. The explanations are created from the answer constraints produced by a meta-interpreter of the query language over queries generated from user inputs (background and distance), and embeddings of the base model (path constraints).
  • Figure 3: Left: factual region (FR) as provided by reasonx. Right: contrastive regions (CR) as provided by reasonx. Grey lines refer to the decision boundary of the base DT.
  • Figure 4: Left: contrastive region (CR) as provided by reasonx, and given a constraint on feature2. Right: given the constraint on feature1, no solution exists. The dashed line refers to the enforced constraint. Grey lines refer to the decision boundary of the DT.
  • Figure 5: Left: minimal CEs provided by reasonx, under the constraint denoted by the identity line. Right: minimal CEs provided by reasonx for under-specified instances. Grey lines refer to the decision boundary of the DT.
  • ...and 7 more figures