ReasonX: Declarative Reasoning on Explanations

ReasonX is a declarative and interactive explanation tool that leverages a closed algebra of linear constraint operators and Mixed-Integer Linear Programming to enable users to reason about decision tree-based ML models at multiple levels of abstraction by integrating symbolic background knowledge.

The Gist

Imagine you've built a super-smart robot that makes important decisions, like whether to approve a loan or not. You trust the robot, but you can't see how it thinks. It's a "black box." You ask, "Why did you say no?" and the robot just says, "Because." That's frustrating and dangerous.

This paper introduces REASONX, a new tool designed to open that black box, but not just by showing you a list of rules. Instead, it gives you a magic conversation where you can ask "What if?" questions and get answers that make sense to humans.

Here is how REASONX works, explained with simple analogies:

1. The Problem: The "Black Box" and the "Rigid" Explainer

Current tools that try to explain AI are like tour guides who only know one specific route.

• If you ask, "Why was this specific person denied a loan?" they can tell you the exact reason (e.g., "Income too low").
• But if you ask, "What if this person had a slightly higher income?" or "What if they lived in a different city?", the guide gets stuck. They can't handle "what if" scenarios easily, and they can't mix in your own common sense (like "But wait, they have a very stable job!").

2. The Solution: REASONX as a "Logic Detective"

REASONX is different. Think of it as a Logic Detective that speaks a special language of "Constraints" (rules like "Income must be > $50k").

Instead of just giving you a static answer, REASONX lets you build a puzzle with the AI.

• The Setup: You give the detective the AI's decision tree (a flowchart of how the AI thinks).
• The Query: You can say, "Here is a person who was denied. Now, imagine a different person who is similar but got approved. What is the smallest change needed to make that happen?"
• The Magic: You can also add your own rules. "Make sure the new person's age doesn't change," or "Make sure they don't change their job." REASONX solves the puzzle while respecting your rules.

3. The Superpower: "Under-Specified" Thinking

Most tools need every single detail to be perfect before they can talk. REASONX is like a sketch artist.

• Normal Tool: Needs a photo of the person (Age: 34, Income: $50k, Job: Engineer) to draw a picture.
• REASONX: Can work with a rough sketch. You can say, "I don't know their exact income, but it's at least $40k." REASONX can still figure out the answer. It can reason about a group of people who fit that description, not just one specific individual.

4. The "Time Travel" Feature

AI models change over time, just like a recipe might get tweaked.

• Imagine you have two versions of the loan-approving robot: Robot A (from last year) and Robot B (from today).
• REASONX can compare them. It can tell you: "Robot A would deny a loan if you have a car lease, but Robot B doesn't care about the car lease."
• It finds the intersection: "Here is a rule that is true for both robots." This helps you see if the AI is becoming fairer or if it's hiding new biases.

5. How It Works Under the Hood (The "Kitchen")

The paper describes a two-layer kitchen:

• The Front Counter (Python): This is where you, the user, talk to the system. It's friendly and easy to use. You type in your questions and constraints here.
• The Back Kitchen (Constraint Logic Programming): This is the heavy lifter. It's a super-math engine that takes your questions and turns them into a giant logic puzzle. It solves the puzzle to find the exact "What if" scenarios you asked for, then sends the answer back to the front counter.

Why Does This Matter?

• Fairness: It helps us find if an AI is discriminating based on race or gender by asking, "If we change the race but keep everything else the same, does the decision change?"
• Trust: It lets you test the AI's logic before you trust it with real money or real lives.
• Actionable Advice: Instead of just saying "You were denied," it can say, "You were denied. If you increase your savings by $2,000, you will be approved."

The Bottom Line

REASONX turns the AI explanation from a one-way lecture into a two-way conversation. It allows us to ask complex "What if" questions, mix in our own common sense, and understand not just what the AI decided, but why it decided it, and how that decision might change if the world around it changes. It's like giving the AI a mirror so we can finally see what's inside.

Technical Summary

1. Problem Statement

The opacity of Machine Learning (ML) models hinders trust and adoption, particularly in high-stakes domains. While eXplainable AI (XAI) methods exist, current approaches suffer from three critical limitations:

• Insufficient Abstraction: Most tools explain only fully specified instances (extensional view), failing to handle under-specified or partially constrained scenarios (intensional view).
• Limited Interactivity: Explanations are typically static; users cannot iteratively refine queries or reason over the explanations themselves using a closed language.
• Lack of Symbolic Integration: Existing methods rarely allow users to integrate background knowledge (e.g., domain constraints, common sense) directly into the reasoning process to generate contrastive or factual explanations.

The authors argue for a shift from descriptive explanations to declarative reasoning, where users can define conditions over explanations and query for answers in a closed algebraic language.

2. Methodology: The REASONX Framework

REASONX is a neurosymbolic tool designed to provide declarative, interactive explanations for decision trees (DTs). These DTs can be the target black-box model (if small enough) or surrogate models (global or local) approximating complex black-boxes.

A. Core Architecture

The system operates on a two-layer architecture:

1. Python Layer (User Interface): Handles data ingestion (pandas), model integration (scikit-learn), and user interaction. It translates user inputs (instances, constraints, distance functions) into formal queries and decodes the results back into human-readable rules.
2. CLP(R) Layer (Reasoning Engine): Implemented in SWI-Prolog using Constraint Logic Programming over the Reals. It acts as a meta-interpreter for a custom query algebra. It performs the heavy lifting of constraint satisfaction, projection, and optimization using Mixed-Integer Linear Programming (MILP).

B. The Query Algebra

The core innovation is a closed algebra of operators over sets of linear constraints. The algebra allows users to compose expressions (queries) that return theories (sets of constraints). Key operators include:

• inst(I, DT, l, pr): Extracts paths in a Decision Tree leading to class $l$ with confidence $\ge pr$ for instance $I$.
• cross(E+): Computes the cross-product of constraints from multiple expressions (e.g., linking a factual instance and a contrastive instance).
• sat(E): Filters for satisfiable constraints.
• πw(E): Projects constraints onto a subset of variables $w$ (existential quantification).
• inf(E, f): Minimizes a linear function $f$ (e.g., distance) subject to constraints in $E$.
• relax(E): Relaxes strict inequalities to non-strict ones to handle boundary uncertainty.

C. Explanation Types

The algebra supports three main types of explanations:

1. Factual Explanations: Why an instance $I$ received prediction $l$.
2. Contrastive Explanations (CEs): What changes are needed to $I$ to achieve a different prediction $l'$. These can be constrained by user-defined background knowledge (e.g., "age cannot decrease").
3. Minimal Contrastive Explanations: CEs that minimize a distance function (e.g., L1 or L∞ norm) between the factual and contrastive instances.

D. Handling Under-Specified Instances

Unlike traditional XAI, REASONX can reason over under-specified instances (e.g., "Age > 30" without a specific value). The system computes explanations valid for the entire set of instances satisfying the constraints, rather than a single point in the feature space.

3. Key Contributions

1. Closed Algebra for XAI: The authors define a formal, closed algebra of operators over linear constraints, enabling the composition of complex explanation queries where the output of one query can serve as the input to another.
2. Neurosymbolic Implementation: The development of REASONX, which bridges the gap between data-driven ML (via surrogate DTs) and symbolic reasoning (via CLP), allowing for the integration of background knowledge as linear constraints.
3. Interactivity and Abstraction: The tool supports iterative reasoning, allowing users to assert/retract constraints, reason over time (comparing models trained at different times), and handle under-specified data profiles.
4. Formal Guarantees: By relying on MILP and CLP, the system provides mathematically sound explanations that are guaranteed to satisfy the user's constraints and the model's logic (assuming high fidelity of the surrogate).

4. Results and Evaluation

The paper evaluates REASONX through qualitative demonstrations and quantitative comparisons against state-of-the-art tools like DiCE (for contrastive examples) and ANCHORS (for factual rules).

• Qualitative Demonstrations:

  • Synthetic Data: Showed the ability to generate factual regions and contrastive regions, and to handle constraints (e.g., keeping a feature constant).
  • Reasoning Over Time: Demonstrated comparing two models (DT0 and DT1) trained on different data splits. REASONX successfully identified which contrastive rules remained valid across both models (intersection) and which were invalidated by model drift.
  • Reasoning Over Model Types: Compared a Decision Tree against an XGBoost surrogate. It revealed that while both models predicted the same class, they relied on different features (e.g., DT used "age," XGBoost used "education"), and only one used a sensitive attribute ("sex").
  • Diversity Optimization: Showed that optimizing for diversity in contrastive examples yields a more varied set of solutions compared to proximity-only optimization.

• Quantitative Evaluation:

  • Contrastive Examples: REASONX produced contrastive examples with smaller distances to the original instance compared to DiCE, indicating more efficient recourse.
  • Factual Rules: Compared to ANCHORS, REASONX produced rules with comparable coverage but with the added benefit of being derived from a closed algebra that supports constraint enforcement.
  • Runtime: REASONX is slower than DiCE and ANCHORS due to the overhead of the CLP layer and MILP solving. However, the runtime is acceptable for offline analysis and interactive sessions where depth of reasoning is prioritized over speed.
  • Constraint Satisfaction: REASONX achieved 100% constraint validity (no violations), whereas other methods often struggle to strictly adhere to user-defined constraints without post-hoc filtering.

5. Significance and Future Work

Significance:

• Paradigm Shift: Moves XAI from "generating a static explanation" to "enabling a reasoning process."
• Actionable Recourse: By integrating background knowledge and constraints directly into the generation process, REASONX produces more realistic and actionable recommendations for users (e.g., in credit scoring).
• Model Drift Analysis: Provides a unique capability to analyze how explanations change as models evolve over time, a critical need for deployed ML systems.

Limitations & Future Directions:

• Scalability: The reliance on MILP limits performance on very large datasets or high-dimensional feature spaces.
• Data Types: Currently focused on tabular data; extension to unstructured data (images, text) requires further formalization.
• User Interaction: The current interface is code-based (Python). Future work aims to integrate Natural Language Processing (NLP) and Large Language Models (LLMs) to allow non-technical users to query the system via natural language.
• Stability Assumption: The tool assumes the model is stable; future work needs to address the uncertainty of model evolution when providing recourse.

In conclusion, REASONX represents a significant step toward declarative XAI, offering a rigorous, interactive, and knowledge-integrated framework for understanding and manipulating the decision logic of machine learning models.