Browsing by Author "Caraball Mieri, José Thomas"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    A logic-based language for querying decision tree explanations
    (2025) Caraball Mieri, José Thomas; Arenas Saavedra, Marcelo Alejandro; Pontificia Universidad Católica de Chile. Escuela de Ingeniería
    La IA Explicable, el campo de investigación que estudia métodos para comprender las respuestas de modelos de aprendizaje de máquina, ha crecido sustancialmente junto con la necesidad de entender mejor las decisiones de estos modelos. Este trabajo responde al llamado de Arenas et al., 2021, quienes propusieron la lógica de interpretabilidad de primer orden (FOIL): un lenguaje declarativo agnóstico al modelo, basado en lógica de primer orden, que captura diversas nociones de explicabilidad. Primeramente, se analiza formalmente FOIL, demostrando sus limitaciones inherentes tanto en expresividad como en complejidad. Para superar estas deficiencias, se introduce la lógica DT-FOIL, una lógica diseñada para árboles de decisión que garantiza evaluación en tiempo polinomial al incorporar predicados específicos de arboles y restringir la cuantificación. Aunque DT-FOIL proporciona una base tratable, su expresividad es limitada. Consecuentemente, se proponen dos extensiones: Q-DT-FOIL y OPT-DT-FOIL. Q-DT-FOIL agrega cuantificación general, ampliando significativamente el alcance de las explicaciones expresables. Se establece que su problema de evaluación extiende la Jerarquía Booleana, mientras que su problema de cómputo es intratable bajo supuestos de complejidad estándar. En contraste, O PT-DT-FOIL está diseñada para computar instancias óptimas que satisfacen una propiedad dada con respecto a un orden parcial estricto. Este diseño enfocado permite a O PT-DT-FOIL capturar explicaciones óptimas cruciales, asegurando que su problema de cómputo sea tratable accediendo a un oráculo NP. Finalmente, para materializar el valor practico de los marcos teóricos, se presenta GoExpDT, una librería de Golang que implementa tanto Q-DT-FOIL como OPT-DT-FOIL. Aprovechando solucionadores SAT modernos como oráculos NP, GoExpDT proporciona un motor de consultas eficiente. Los resultados experimentales confirman su capacidad para manejar consultas de explicabilidad complejas sobre árboles de decisión de tamaño industrial en un tiempo manejable, afirmando la viabilidad del enfoque propuesto. Este trabajo representa un paso significativo hacia una base uniforme y práctica para la explicabilidad de árboles de decisión.
  • Thumbnail Image
    Item
    A Uniform Language to Explain Decision Trees
    (International Joint Conferences on Artificial Intelligence (IJCAI), 2024) Arenas Saavedra, Marcelo Alejandro; Barceló Baeza, Pablo; Bustamante Henríquez, Diego Emilio; Caraball Mieri, José Thomas; Subercaseaux, Bernardo
    The formal XAI community has studied a plethora of interpretability queries aiming to understand the classifications made by decision trees. However, a more uniform understanding of what questions we can hope to answer about these models, traditionally deemed to be easily interpretable, has remained elusive. In an initial attempt to understand uniform languages for interpretability, Arenas et al. (2021) proposed FOIL, a logic for explaining black-box ML models, and showed that it can express a variety of interpretability queries. However, we show that FOIL is limited in two important senses: (i) it is not expressive enough to capture some crucial queries, and (ii) its model agnostic nature results in a high computational complexity for decision trees. In this paper, we carefully craft two fragments of first-order logic that allow for efficiently interpreting decision trees: Q-DT-FOIL and its optimization variant OPT-DT-FOIL. We show that our proposed logics can express not only a variety of interpretability queries considered by previous literature, but also elegantly allows users to specify different objectives the sought explanations should optimize for. Using finite model-theoretic techniques, we show that the different ingredients of Q-DT-FOIL are necessary for its expressiveness, and yet that queries in Q-DT-FOIL can be evaluated with a polynomial number of queries to a SAT solver, as well as their optimization versions in OPT-DT-FOIL. Besides our theoretical results, we provide a SAT-based implementation of the evaluation for OPT-DT-FOIL that is performant on industry-size decision trees.