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.

翻译：解释不透明的机器学习（ML）模型已成为日益重要的挑战。然而，当前人工智能解释（XAI）方法存在若干不足，包括抽象程度不足、用户交互性有限以及符号知识整合不充分。我们提出ReasonX，一种基于线性约束理论上的封闭算子代数表达式（或称查询）的解释工具。ReasonX为决策树提供声明式和交互式解释，这些决策树既可代表被分析的ML模型，也可作为任何黑盒预测器的全局或局部替代模型。用户可以将背景知识或常识表达为线性约束。这使得推理能够在多个抽象层次上进行，范围从完全指定的实例到未充分指定或部分约束的实例。ReasonX利用混合整数线性规划（MILP）对事实实例和对比实例的特征进行推理。本文介绍ReasonX的架构，该架构包含一个更接近用户的Python层，以及一个实现查询代数元解释器的约束逻辑编程（CLP）层。通过定性示例展示了ReasonX的能力，并通过定量实验与其他XAI工具进行了比较。