ReasonX: Declarative Reasoning on Explanations

Laura State; Salvatore Ruggieri; Franco Turini

cs.CYFeb 27, 2026

ReasonX: Declarative Reasoning on Explanations

Authors: Laura State, Salvatore Ruggieri, Franco Turini

Organizations: University of Pisa, IT · Scuola Normale Superiore, IT · Alexander von Humboldt Institute for Internet and Society, GER

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.

Figures & tables

Panel of Figure 1 — 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}$ .

Method ( ⋆ )	Type		Data			Output			CON	DIV	USI	MM	INT
Method ( ⋆ )	Type		tab.	text	im.	FR	CR	CE	CON	DIV	USI	MM	INT
reasonx	MA/MS	g/l	✓	✗	✗	✓	✓	✓	linear	✓	✓	✓	✓
LORE	MA	l	✓	✗	✗	✓	✓	✗	✗	n.a.	n.a.	✗	✗
GLocalX	MA	g	✓	✗	✗	rule sets		✗	✗	n.a.	n.a.	✗	✗
ANCHORS	MA	l	✓	✓	✓	✓	✗	✗	n.a.	n.a.	n.a.	✗	✗
Wachter	MA	l	✓	✗	✗	✗	✗	✓	✗	✓	✗	✗	✗

Table 1: Comparing reasonx against related explainability methods. Explanation type according to the introduced taxonomy (MA = model-agnostic, MS = model-specific, g = global, l = local). The output can be factual decision rules (FR), contrastive decision rules (CR) or contrastive examples (CE). CON = possibility to enforce constraints on CR/CE, DIV = possibility of optimizing for diversity on a set of CE. USI = under-specified information for a CE. n.a. = not applicable, tab. = tabular, im. = image. MM = explanations over time and multiple models, INT = interactive explanations. ( ⋆ ) For space reasons, corresponding papers are listed next: LORE ( Guidotti et al., 2019a ) , GlocalX ( Setzu et al., 2021 ) , ANCHORS ( Ribeiro et al., 2018 ) , Wachter ( Wachter and others, 2017 ) , DiCE ( Mothilal et al., 2020 ) , DACE ( Kanamori et al., 2020 ) , Cui ( Cui et al., 2015 ) , Russell ( Russell, 2019 ) , Ustun ( Ustun et al., 2019 ) , MACE ( Karimi et al., 2020 ) , Karimi ( Karimi et al., 2021 ) , Bertossi ( Bertossi, 2023 ) , Takemura ( Takemura and Inoue, 2024 ) , LIMEtree ( Sokol and Flach, 2020a ) .

Factual
Base expression	$e_{1}=\mathit{sat}(\mathit{cross}(\mathit{inst}(I_{1},DT_{1},0,0.95),\{U_{1}\}))$
Factual constraints	$c\in Th(\mathit{inst}(I_{1},DT_{1},0,0.95))$
Factual rule	$c\rightarrow l=0\ [p]$
Constrastive
Base expression	$e_{2}=\mathit{sat}(\mathit{cross}(\mathit{inst}(I_{1},DT_{1},0,0.95),\mathit{inst}(I_{2},DT_{1},1,0.95),\{U_{2}\}))$
Constrastive constraint	$c\in Th(e_{3})$ , where $e_{3}=\pi_{I_{2}.\mathbf{x}}(e_{2})$

Table 2: Example expressions for factual, contrastive and minimal contrastive explanations.

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.

Description	Output
$\mathcal{R_{F,\text{$ 0 $}}}$	IF F0.capitalgain<=5095.5, F0.education<=12.5, F0.age>29.5
	THEN <=50K [0.8095]
$\mathcal{R_{F,\text{$ 1 $}}}$	IF F1.capitalgain<=5119.0, F1.education<=12.5, F1.age>33.5
	THEN <=50K [0.7907]

Table 3: Factual rules

\mathcal{R_{F,\text{

}}}

for a same instance and different models over time

DT_{i}

with

i=0,1

Index	Output (rules or contrastive examples)
(1)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain<=5095.5,CE0.education>12.5,CE0.age>30.5
		THEN >50K [0.5087]
(2)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain>5095.5,CE0.capitalgain<=6457.5 THEN >50K [0.9286]
(3)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain>7055.5,CE0.age>20.0 THEN >50K [0.9873]
(4)	$CE_{0}$	CE0.race=AsianPacIslander, CE0.sex=Male,CE0.workclass=Private,
	( $0.267$ )	CE0.education=13.0,CE0.age=40.0,CE0.capitalgain=0.0,

Table 4: Contrastive rules and examples for a same instance and different models. Rules

\mathcal{R_{C,\text{

}}}

and examples

CE_{0}

in (1) - (6) refer to

DT_{0}

. Rules

\mathcal{R_{C,\text{

}}}

and examples

CE_{1}

\mathcal{R_{C,\text{1}}}

in (7) - (12) refer to

DT_{1}

. Rule

\mathcal{R_{C,\text{

0,1

}}}

and example

CE_{0,1}

in (13) and (14) refer to additional conditions that are the result of intersecting explanations from

DT_{0}

and

DT_{1}

. Numerical values in round brackets indicate the distance between factual instance and contrastive examples.

Description	Output
$\mathcal{R_{F,\text{$ 0 $}}}$	IF F0.capitalgain>7055.5,F0.age>20.0 THEN >50K [0.9882]
$\mathcal{R_{F,\text{$ 1 $}}}$	IF F1.education<=12.5,F1.capitalgain>7073.5 THEN >50K [0.9940]

Table 5: Factual rules

\mathcal{R_{F,\text{

}}}

for a same instance and different models types

DT_{i}

with

i=0,1

Index	Output (rules)
(1)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain<=5119.0,CE0.education<=12.5,CE0.age<=30.5
		THEN <=50K [0.9653]
(2)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain<=5119.0,CE0.education<=12.5,CE0.age>30.5
		THEN <=50K [0.8032]
(3)	$\mathcal{R_{C,\text{$ 0 $}}}$	IF CE0.capitalgain<=5119.0,CE0.education>12.5,CE0.age<=28.5
		THEN <=50K [0.9022]

Table 6: Contrastive rules for a same instance and different model types. Rules

\mathcal{R_{C,\text{

}}}

in (1) - (6) refer to

DT_{0}

. Rules

\mathcal{R_{C,\text{

}}}

in (7) - (9) refer to

DT_{1}

. Rules

\mathcal{R_{C,\text{

0,1

}}}

in (10) - (12) refer to additional conditions that are the result of intersecting explanations from

DT_{0}

and

DT_{1}

	case	$acc/f$ ( ⋆ )	$l_{F}$	$l_{C}$	$N_{C}$	$S/N$		$N_{CE}$	$d_{CE}$	$dim_{CE}$
ADULT	(DT-M)	$0.802$	$2.988$	$2.008$	$2.049$	$0.82$	$L_{1}$	$2.049$	$0.063$	p.
							$L_{\infty}$	$2.049$	$0.062$	h.-d.
	(DT-GS)	$0.851/0.919$	$2.978$	$2.832$	$4.674$	$0.92$	$L_{1}$	$4.674$	$0.449$	p.
							$L_{\infty}$	$4.674$	$0.378$	h.-d.
	(DT-LS)	$0.851/0.840$	$1.944$	$2.564$	$2.371$	$0.89$	$L_{1}$	$2.371$	$0.244$	p.
							$L_{\infty}$	$2.371$	$0.201$	h.-d.

Table 7: Evaluation of reasonx . SGC = South German Credit, GMSC = Give Me Some Credit, DCCC = Default Credit Card Clients, ACA = Australian Credit Approval. The CE obtained after the MILP optimization can be a point (abbreviated p.) or a higher-dimensional object such as a line (abbreviated h.-d.). ( ⋆ ) No fidelity in case (DT-M) .

		$N_{CE}$		$d_{CE}$ ( $w_{div}=0$ )
Setting/Approach	$acc/f$	$L_{1}$	$L_{inf}$	$L_{1}$	$L_{inf}$
No constraints
DiCE	$0.785$ (*)	2		1.131	0.775
		3		1.097	0.754
		4		1.170	0.784
		5		1.107	0.767

Table 8: Contrastive examples/constraints: comparison between DiCE and reasonx . (*) No fidelity for DiCE.

Approach	$acc$ / $f$	$D$	$p_{0}$ or $MC_{F}$ ( ⋆⋆ )	$p_{c}$	$c$ or $S/N$ ( ⋆⋆ )	$l_{F}$
ANCHORS	$0.850$ ( ⋆ )	n.a.	$0.9$	$0.910$	$0.433$	$2.06$
			$0.95$	$0.944$	$0.352$	$3.04$
			$0.99$	$0.966$	$0.273$	$4.55$
reasonx (case DT-GS)	$0.851/0.891$	2	$0.9$	n.a.	$0.69$	$2.0$
			$0.95$	n.a.	$0.69$	$2.0$
			$0.99$	n.a.	$0$	n.a.

Table 9: Factual rules: comparison between reasonx and ANCHORS. ( ⋆ ) ANCHORS has no fidelity. ( ⋆⋆ ) The first metric (

p_{0}

c

) is reported for ANCHORS, the second (

MC_{F}

S/M

) is a non-equivalent but similar metric for reasonx .

Approach	Setting	Constraints	Time (in s)
reasonx	initialization ( ⋆ )	n.a.	$0.129$
	case DT-M, $D=3$ , $MC_{F}=0$
	initialization, query	no constraints	$1.102$
	initialization, query	immutability capitalgain	$0.685$
	case DT-GS, $D=3$ , $MC_{F}=0$
	initialization, query	no constraints	$0.825$

Table 10: Runtime for reasonx , ANCHORS and DiCE. ( ⋆ ) relies on case (DT-M) .

Demonstration	Dataset	Splits	Instances	Case	Norm	$\epsilon$	$D$
Synthetic dataset case	synthetic	train/test	training	(DT-M)	$L_{1}$	$0$	3
Adult income case (*)	ADULT	train/test	training	all	$L_{1}$	$0$	3
Reason over time	ADULT	$50:50$ /train/test	test	(DT-M)	$L_{1}$	$0.01$	3
Reason over models	ADULT	train/test/expl	test/expl	(DT-M), (DT-GS)	$L_{1}$	$0.01$	3
Diversity optimization	ADULT	train/test/expl	test/expl	(DT-M), (DT-GS)	$L_{1}$	$0.01$	3
Detecting bias	ADULT	train/test	test	(DT-M)	n.a.	n.a.	5

Table 11: Overview of experimental settings for the demonstrations. For each demonstration, columns list the dataset, how it was split into sets, from which set the data instances were taken, which case of reasonx was used, the norm, the value of the parameter

\epsilon

, and the depth of the base model

D

. (*) case (DT-GS) and (DT-LS) are only shown on the level of Python. n.a.

=

not applicable, because minimal contrastive rules were not used.

Panel of Figure 6 — Figure 6: Diversity optimization: top row shows histograms, bottom row the density functions. The left column shows the value of the optimization function $f(x_{f},S)$ , the middle column the value of only the proximity term and the right column the values of only the diversity term. Color codes indicate the type of optimization.

model	age	race	sex	age, race	age, sex	race,sex
DT	$0.01$	$0.00$	$0.00$	$0.01$	$0.01$	$0.00$
XGB	$0.12$	$0.00$	$0.11$	$0.12$	$0.26$	$0.11$

Table 12: Fraction

N_{s}/N

of cases admitting a solution that change sensitive attributes only.

Name	$N$	Class ratio	$n_{nominal}$	$n_{ordinal}$	$n_{continuous}$
ADULT	$48,842$	$37,155:11,687$ , $(\leq 50k:>50k)$	3	1	4
SGC	$1,000$	$700:300$ , $(1:0)$	0	17	3
GMSC	$150,000$	$139,974:10,024$ , $(0:1)$	0	0	10
DCCC	$30,000$	$23,364:6,636$ , $(0:1)$	3	0	8
ACA	$690$	$383:307$ , $(0,1)$	$8$	0	6

Table 13: Dataset summary statistics.

Description		Notation
Metrics
Base model	accuracy	$acc$
	fidelity ⋆	$f$
	output ratio	$S/N$
Rules ( $\mathbb{R}_{F}$ and $\mathbb{R}_{C}$ )	rule length	$l_{F},l_{C}$
	size of $\mathbb{R}_{C}$	$N_{C}$

Table 14: Notation for evaluation metrics and parameters of reasonx . ( ⋆ ) The fidelity metric applies only if there is a surrogate model, i.e., in cases (DT-GS) and (DT-LS) .

Figure 7: Parameter testing: metrics depending on depth of the base model, case (DT-M) .

Figure 8: Parameter testing: metrics depending on depth of the base model, case (DT-GS) .

Figure 9: Parameter testing: metrics depending on depth of the base model, case (DT-LS) .

Figure 10: Parameter testing: metrics depending on minconf value of CE, case (DT-M) .

Figure 11: Parameter testing: metrics depending on minconf value of CE, case (DT-GS) .

Figure 12: Parameter testing: metrics depending on minconf value of CE, case (DT-LS) .

Explore similar work

ExplAIner: A Declarative Query Language for Explaining Classification Models
Jul 7, 2026Marcelo Arenas, Pablo Barceló, Diego Bustamante +3Explainable Artificial Intelligence Interpretable ML
Pontificia Universidad Católica de Chile, Chile · Carnegie Mellon University, USA
A Causal Argumentation Method for Explainability of Machine Learning Models
May 20, 2026Henry Salgado, Meagan R. Kendall, Martine CeberioExplainable Artificial Intelligence Causal Explanation
Department of Computer Science, The University of Texas at El Paso, El Paso, TX, USA · Department of Engineering Education and Leadership, The University of Texas at El2026 Paso, El Paso, TX, USA
MEA: A Reward-Driven Multi-Agent System for Faithful Model Explanations
Oct 1, 2026Yuyang Cheng, Raghav Kaushik Ravi, Srivarshinee Sridhar +3Explainable Artificial Intelligence Faithfulness of Language Model Explanations
University of Virginia · Vellore Institute of Technology · Indian Institute of Technology, Patna

Jul 7, 2026J/K move · Enter open · S save

ExplAIner: A Declarative Query Language for Explaining Classification Models

Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball+2

Pontificia Universidad Católica de Chile, Chile · Carnegie Mellon University, USA

Explainable Artificial Intelligence Interpretable ML

Open paper AskPDF arXiv

The XAI community has studied a wide range of queries and scores for explaining predictions of ML models. From a data management perspective, this proliferation of explanation notions calls for declarative query languages in which such notions can be specified, combined, and analyzed uniformly. In this paper, we develop such a framework for Boolean models. We first revisit FOIL, an interpretability query language for black-box models, and show that it has two fundamental limitations: it cannot express central optimality-based explanation queries, and its evaluation problem over decision trees is hard for every level of the polynomial hierarchy. We then introduce ExplAIner, a query language based on FOIL with an extended vocabulary and a layered structure. We show that ExplAIner can express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. We also prove that the evaluation problem for each query in ExplAIner belongs to the Boolean hierarchy over every class of Boolean models for which some basic predicates can be evaluated in polynomial time. In particular, that property holds for deterministic and decomposable Boolean circuits. Finally, we introduce Opt-FOIL, an optimization-oriented fragment of ExplAIner for computing explanations that are minimal with respect to strict partial orders, and prove that its evaluation problem is in

\mathrm{FP}^{\mathrm{NP}}

under the same tractability assumptions. These complexity results have a direct algorithmic consequence: a fixed ExplAIner query can be evaluated with a fixed number of calls to a SAT solver, while a notion of explanation specified in Opt-FOIL can be computed with a polynomial number of such calls. This is particularly relevant in formal XAI, where SAT solvers have been successfully used to compute explanations for several classes of ML models.

Abstract

Explore similar work

ExplAIner: A Declarative Query Language for Explaining Classification Models

A Causal Argumentation Method for Explainability of Machine Learning Models

MEA: A Reward-Driven Multi-Agent System for Faithful Model Explanations