Author name cluster

Bernardo Subercaseaux

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

2 author rows

JAIR Journal 2025 Journal Article

On Computing Probabilistic Explanations for Decision Trees

Marcelo Arenas
Pablo Barcelo
Alexander Kozachinskiy
Miguel Romero
Bernardo Subercaseaux

Formal XAI (explainable AI) is a growing area that focuses on computing explanations with mathematical guarantees for the decisions made by ML models. Inside formal XAI, one of the most studied cases is that of explaining the choices taken by decision trees, as they are traditionally deemed as one of the most interpretable classes of models. Recent work has focused on studying the computation of sufficient reasons, a kind of explanation in which given a decision tree T and an instance x, one explains the decision T (x) by providing a subset y of the features of x such that for any other instance z compatible with y, it holds that T (z) = T (x), intuitively meaning that the features in y are already enough to fully justify the classification of x by T. It has been argued, however, that sufficient reasons constitute a restrictive notion of explanation. For such a reason, the community has started to study their probabilistic counterpart, in which one requires that the probability of T (z) = T (x) must be at least some value δ ∈ (0, 1], where z is a random instance that is compatible with y. Our paper settles the computational complexity of δ-sufficient-reasons over decision trees, showing that both (1) finding δ-sufficient-reasons that are minimal in size, and (2) finding δ-sufficient-reasons that are minimal inclusion-wise, are computationally intractable. By doing this, we answer two open problems originally raised by Izza et al. (2021), and extend the hardness of explanations for Boolean circuits presented by Wäldchen et al. (2021) to the more restricted case of decision trees. Furthermore, we present sharp non-approximability results under a widely believed complexity hypothesis. On the positive side, we identify structural restrictions of decision trees that make the problem tractable.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Probabilistic Explanations for Linear Models

Bernardo Subercaseaux
Marcelo Arenas
Kuldeep S. Meel

Formal XAI is an emerging field that focuses on providing explanations with mathematical guarantees for the decisions made by machine learning models. A significant amount of work in this area is centered on the computation of ``sufficient reasons''. Given a model M and an input instance x, a sufficient reason for the decision x is a subset S of the features of x such that for any instance z that has the same values as x for every feature in S, it holds that M(x) = M(z). Intuitively, this means that the features in S are sufficient to fully justify the classification of x by M. For sufficient reasons to be useful in practice, they should be as small as possible, and a natural way to reduce the size of sufficient reasons is to consider a probabilistic relaxation; the probability of M(x) = M(z) must be at least some value delta in (0,1], where z is a random instance that coincides with x on the features in S. Computing small delta-sufficient reasons (delta-SRs) is known to be a theoretically hard problem; even over decision trees — traditionally deemed simple and interpretable models — strong inapproximability results make the efficient computation of small delta-SRs unlikely. We propose the notion of (delta, epsilon)-SR, a simple relaxation of delta-SRs, and show that this kind of explanations can be computed efficiently over linear models.

PDF Details DOI

KR Conference 2024 Conference Paper

A Uniform Language to Explain Decision Trees

Marcelo Arenas
Pablo Barceló
Diego Bustamante
Jose Caraball
Bernardo Subercaseaux

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. 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.

PDF Details DOI

LPAR Conference 2024 Conference Paper

Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition

Bernardo Subercaseaux

Adding blocked clauses to a CNF formula can substantially speed up SAT-solving, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula [17, 19]. In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly for certain instance families when blocked clauses are added as a preprocessing step [10, 22]. This fact is in contrast to, but not in contradiction with, prior results showing that Blocked- Clause Elimination (BCE) is sometimes an effective preprocessing step [14, 15]. We suggest that the practical role of blocked clauses in SAT-solving might be richer than expected. Concretely, we propose a theoretical study of the complexity of Blocked-Clause Addition (BCA) as a preprocessing step for SAT-solving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might unblock a different clause that was previously blocked. This order-sensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of k-ary blocked clauses that can be added to an input formula F is NP-hard for every k ≥ 2.

Details

LPAR Conference 2023 Conference Paper

Toward Optimal Radio Colorings of Hypercubes via SAT-solving

Bernardo Subercaseaux
Marijn J. H. Heule

Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of two vertices u and v differ by at least 2 if u and v are neighbors, and by at least 1 if u and v have a common neighbor. Our work improves the best-known bounds for optimal radio 2-colorings of small hypercube graphs, a combinatorial problem that has received significant attention in the past. We do so by using automated reasoning techniques such as symmetry breaking and Cube and Conquer, obtaining that for n = 7 and n = 8, the coding-theory upper bounds of Whittlesey et al. (1995) are not tight. Moreover, we prove the answer for n = 7 to be either 12 or 13, thus making a substantial step towards answering an open problem by Knuth (2015). Finally, we include several combinatorial observations that might be useful for further progress, while also arguing that fully determining the answer for n = 7 will require new techniques.

Details

NeurIPS Conference 2022 Conference Paper

Augmenting Online Algorithms with $\varepsilon$-Accurate Predictions

Anupam Gupta
Debmalya Panigrahi
Bernardo Subercaseaux
Kevin Sun

The growing body of work in learning-augmented online algorithms studies how online algorithms can be improved when given access to ML predictions about the future. Motivated by ML models that give a confidence parameter for their predictions, we study online algorithms with predictions that are $\epsilon$-accurate: namely, each prediction is correct with probability (at least) $\epsilon$, but can be arbitrarily inaccurate with the remaining probability. We show that even with predictions that are accurate with a small probability and arbitrarily inaccurate otherwise, we can dramatically outperform worst-case bounds for a range of classical online problems including caching, online set cover, and online facility location. Our main results are an $O(\log(1/\varepsilon))$-competitive algorithm for caching, and a simple $O(1/\varepsilon)$-competitive algorithm for a large family of covering problems, including set cover and facility location, with $\epsilon$-accurate predictions.

PDF Details

NeurIPS Conference 2022 Conference Paper

On Computing Probabilistic Explanations for Decision Trees

Marcelo Arenas
Pablo Barceló
Miguel Romero Orth
Bernardo Subercaseaux

Formal XAI (explainable AI) is a growing area that focuses on computing explanations with mathematical guarantees for the decisions made by ML models. Inside formal XAI, one of the most studied cases is that of explaining the choices taken by decision trees, as they are traditionally deemed as one of the most interpretable classes of models. Recent work has focused on studying the computation of sufficient reasons, a kind of explanation in which given a decision tree $T$ and an instance $x$, one explains the decision $T(x)$ by providing a subset $y$ of the features of $x$ such that for any other instance $z$ compatible with $y$, it holds that $T(z) = T(x)$, intuitively meaning that the features in $y$ are already enough to fully justify the classification of $x$ by $T$. It has been argued, however, that sufficient reasons constitute a restrictive notion of explanation. For such a reason, the community has started to study their probabilistic counterpart, in which one requires that the probability of $T(z) = T(x)$ must be at least some value $\delta \in (0, 1]$, where $z$ is a random instance that is compatible with $y$. Our paper settles the computational complexity of $\delta$-sufficient-reasons over decision trees, showing that both (1) finding $\delta$-sufficient-reasons that are minimal in size, and (2) finding $\delta$-sufficient-reasons that are minimal inclusion-wise, do not admit polynomial-time algorithms (unless P = NP). This is in stark contrast with the deterministic case ($\delta = 1$) where inclusion-wise minimal sufficient-reasons are easy to compute. By doing this, we answer two open problems originally raised by Izza et al. , and extend the hardness of explanations for Boolean circuits presented by W{\"a}ldchen et al. to the more restricted case of decision trees. On the positive side, we identify structural restrictions of decision trees that make the problem tractable, and show how SAT solvers might be able to tackle these problems in practical settings.

PDF Details

TCS Journal 2022 Journal Article

On the expressiveness of Lara: A proposal for unifying linear and relational algebra

Pablo Barceló
Nelson Higuera
Jorge Pérez
Bernardo Subercaseaux

We study the expressive power of the Lara language – a recently proposed unified model for expressing relational and linear algebra operations – both in terms of traditional database query languages and some analytic tasks often performed in machine learning pipelines. Since Lara is parameterized by a set of user-defined functions which allow to transform values in tables, known as extension functions, the exact expressive power of the language depends on how these functions are defined. We start by showing Lara to be expressive complete with respect to a syntactic fragment of relational algebra with aggregation (under the mild assumption that extension functions in Lara can cope with traditional relational algebra operations such as selection and renaming). We then look further into the expressiveness of Lara based on different classes of extension functions, and distinguish two main cases depending on the level of genericity that queries are enforced to satisfy. Under strong genericity assumptions the language cannot express matrix convolution, a very important operation in current machine learning pipelines. This language is also local, and thus cannot express operations such as matrix inverse that exhibit a recursive behavior. For expressing convolution, one can relax the genericity requirement by adding an underlying linear order on the domain. This, however, destroys locality and turns the expressive power of the language much more difficult to understand. In particular, although under complexity assumptions some versions of the resulting language can still not express matrix inverse, a proof of this fact without such assumptions seems challenging to obtain.

Details DOI

SAT Conference 2022 Conference Paper

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

Bernardo Subercaseaux
Marijn J. H. Heule

A packing k-coloring of a graph G = (V, E) is a mapping from V to {1, .. ., k} such that any pair of vertices u, v that receive the same color c must be at distance greater than c in G. Arguably the most fundamental problem regarding packing colorings is to determine the packing chromatic number of the infinite square grid. A sequence of previous works has proved this number to be between 13 and 15. Our work improves the lower bound to 14. Moreover, we present a new encoding that is asymptotically more compact than the previously used ones.

Details

NeurIPS Conference 2021 Conference Paper

Foundations of Symbolic Languages for Model Interpretability

Marcelo Arenas
Daniel Báez
Pablo Barceló
Jorge Pérez
Bernardo Subercaseaux

Several queries and scores have recently been proposed to explain individual predictions over ML models. Examples include queries based on “anchors”, which are parts of an instance that are sufficient to justify its classification, and “feature-perturbation” scores such as SHAP. Given the need for flexible, reliable, and easy-to-apply interpretability methods for ML models, we foresee the need for developing declarative languages to naturally specify different explainability queries. We do this in a principled way by rooting such a language in a logic called FOIL, which allows for expressing many simple but important explainability queries, and might serve as a core for more expressive interpretability languages. We study the computational complexity of FOIL queries over two classes of ML models often deemed to be easily interpretable: decision trees and more general decision diagrams. Since the number of possible inputs for an ML model is exponential in its dimension, tractability of the FOIL evaluation problem is delicate but can be achieved by either restricting the structure of the models, or the fragment of FOIL being evaluated. We also present a prototype implementation of FOIL wrapped in a high-level declarative language and perform experiments showing that such a language can be used in practice.

PDF Details

NeurIPS Conference 2020 Conference Paper

Model Interpretability through the lens of Computational Complexity

Pablo Barceló
Mikaël Monet
Jorge Pérez
Bernardo Subercaseaux

In spite of several claims stating that some models are more interpretable than others --e. g. , "linear models are more interpretable than deep neural networks"-- we still lack a principled notion of interpretability that allows us to formally compare among different classes of models. We make a step towards such a theory by studying whether folklore interpretability claims have a correlate in terms of computational complexity theory. We focus on post-hoc explainability queries that, intuitively, attempt to answer why individual inputs are classified in a certain way by a given model. In a nutshell, we say that a class C1 of models is more interpretable than another class C2, if the computational complexity of answering post-hoc queries for models in C2 is higher than for C1. We prove that this notion provides a good theoretical counterpart to current beliefs on the interpretability of models; in particular, we show that under our definition and assuming standard complexity-theoretical assumptions (such as P! =NP), both linear and tree-based models are strictly more interpretable than neural networks. Our complexity analysis, however, does not provide a clear-cut difference between linear and tree-based models, as we obtain different results depending on the particular {post-hoc explanations} considered. Finally, by applying a finer complexity analysis based on parameterized complexity, we are able to prove a theoretical result suggesting that shallow neural networks are more interpretable than deeper ones.

PDF Details