Provably Explaining Neural Additive Models

AI summary

Overview

Research area: Explainable AI and formal neural network verification, specifically provable, minimal sufficient explanations for Neural Additive Models (NAMs).

Technical level: Advanced.

Scope: The paper introduces a NAM-specific algorithm that computes provably cardinally-minimal sufficient explanations using only a logarithmic number of verification queries in the number of input features, plus a parallelized preprocessing step with logarithmic runtime in the required precision on each univariate component.

What This Paper Is About

Explanations of neural network predictions often lack provable guarantees, and the strongest form of explanation — a cardinally-minimal subset of input features that is provably sufficient to determine the prediction — is computationally infeasible for standard networks, requiring a worst-case exponential number of NP-hard verification queries. This paper shows that for Neural Additive Models (NAMs), which decompose a prediction into a sum of univariate neural network components, cardinally-minimal provably sufficient explanations can be computed efficiently, and in practice faster and smaller than algorithms that only target the weaker notion of subset-minimal explanations.

Key Contributions

1. The first method for certifiable explanations in NAMs. The paper introduces an approach that returns provably sufficient and provably cardinally-minimal explanations for NAMs, covering regression, binary classification, and multi-class classification (with the main presentation focused on binary classification and extensions in Appendix E), boosting trustworthiness in safety-critical settings.
2. A two-stage algorithm replacing exponential search with a logarithmic one. Stage 1 (Algorithm 2) computes an importance ordering of features by running verification queries independently and in parallel on each small univariate component f_i, with a parallelized binary-search preprocessing step whose runtime is logarithmic in the required precision. Stage 2 (Algorithm 4) then uses binary search over ordered feature prefixes to identify the cardinally-minimal sufficient explanation using O(log n) queries.
3. Formal complexity guarantees. Theorem 1 shows the combined algorithm needs O((n/p) · log(max_i (β_i − α_i)/ξ_i)) queries to the univariate f_i components with p parallel processors, approaching O(log(max_i (β_i − α_i)/ξ_i)) as p → n, plus O(log n) queries to the full NAM f. Theorem 2 gives upper and lower bounds in terms of the model encoding size m: at most O(m) NP-oracle queries (Claim 1) and at least O(log(m)) such queries (Lemma 5), with the algorithm terminating after at most O(m) queries (Proposition 5).
4. Empirical comparison against subset-minimal baselines and sampling-based interpretation. Experiments with α,β-CROWN as the backend verifier show the method produces smaller explanations and substantially lower computation times than the standard greedy subset-minimal algorithm, despite solving a strictly harder problem, and demonstrate that purely sampling-based NAM interpretations can be misleading.

Main Findings

• Logarithmic query complexity replaces exponential. Standard algorithms require O(2^n) verification queries to the full network f for a cardinally-minimal explanation, or O(n) queries to f for only a subset-minimal explanation. The proposed algorithm instead uses O(log n) queries to f plus queries on much smaller univariate components.
• Complexity scales with feature separation, not just feature count. The query bound is parameterized by ξ_i, the minimum separation between adjacent features in the sorted order. In the edge case where ξ_i → 0, the paper shows (Appendix D.1) that with ReLU activations the algorithm still terminates after a linear number of steps in the size of the model encoding — still far better than the exponential worst case for general networks.
• Smaller explanations than subset-minimal baselines on all three named benchmarks. On Breast Cancer the method returns explanations of size 4.00 (±4.24) versus 16.58 (±5.44) for the lexicographic ordering and 16.27 (±5.57) for the reverse-sensitivity ordering; on CREDIT, 3.76 (±2.62) versus 12.42 (±6.45) and 3.82 (±1.84); on FICO HELOC, 5.59 (±1.80) versus 15.60 (±7.53) and 9.45 (±5.90).
• Lower computation time on two of three benchmarks. Breast Cancer: 35.60 s (±1.34) for the proposed method versus 634.92 s (±77.23, lexicographic) and 636.79 s (±87.44, sensitivity). CREDIT: 132.67 s (±36.76) versus 473.63 s (±128.38) and 407.93 s (±126.63). On FICO HELOC the lexicographic baseline was faster (146.16 s ±188.07) than the proposed method (317.92 s ±222.07), while the sensitivity baseline took 250.09 s (±148.44).
• Explanations converge faster over time. Figure 3 tracks explanation size over time across the datasets: subset-minimal approaches converge slowly and often stagnate in local minima, whereas the proposed method starts later because of the Algorithm 2 preprocessing but quickly outpaces them.
• Sampling-based NAM interpretation can be actively misleading. Figure 2 uses the FICO HELOC dataset to show that a user might wrongly conclude feature 1 alone determines a positive output, when small changes in features 15 or 18 can flip the classification, and that sampling can miss extrema — for example, feature 2's output can become negative enough to flip the classification even if sampled values look positive.
• Benchmarks and verifier used. The paper states it uses "four widely used tabular-data benchmarks" but names three in the text: Breast Cancer, CREDIT, and FICO HELOC, all described as prominent in safety-critical domains; model architectures follow prior NAM literature, and α,β-CROWN is the backend verifier.

Methodology in Plain English

The starting point is a formal definition of a sufficient explanation: a subset of features S such that fixing those features to their observed values keeps the prediction unchanged for any assignment to the remaining features within an ℓ_p-norm ball of radius ϵ_p around the input (Definition 1). Whether a given subset satisfies this can be posed as a neural network verification query. Minimality comes in two flavors (Definition 2): subset-minimal (no proper subset is sufficient) and the stronger cardinally-minimal (no sufficient subset of smaller size exists).

For a general network, the standard greedy procedure (Algorithm 1) removes features one at a time, needing a linear number of queries and only guaranteeing subset-minimality; exhaustive search for cardinal minimality needs 2^n queries.

The paper's approach exploits additivity in two stages:

1. Parallel interval importance sorting (Algorithm 2). Because each feature enters the prediction only through its own univariate function f_i, each component can be analyzed on its own, in parallel. For each component the algorithm obtains initial bounds from an incomplete verification query and then binary-searches with verification queries to tighten the interval around the component's worst-case (minimum, or maximum when the prediction is 0) value inside the perturbation region. Each small univariate network is far cheaper to verify than the full model. Before the preprocessing begins, all features are treated as equally important — the algorithm initializes importance values as zero and only refines when gaps are detected between features. The binary search stops as soon as the intervals of all components become non-overlapping, yielding a total order of features by how strongly they can drive the output toward the decision boundary. The number of iterations per component depends on the ratio between its initial bound gap and the separation ξ_i from its neighbors in the final ordering, giving the logarithmic dependence on precision.
2. Feature selection on the resulting order (Algorithms 3 and 4). A naive greedy version (Algorithm 3) walks the ordered features and removes one whenever the remainder is still sufficient, requiring O(n) queries but already returning a cardinally-minimal explanation. The improved version (Algorithm 4) uses binary search over prefixes {F[1], …, F[m]} of the sorted order, checking sufficiency of each prefix and narrowing the search, which yields a cardinally-minimal explanation in O(log n) queries. The paper notes this binary search is only sound because Algorithm 2 supplies a structured ordering — with an arbitrary ordering, sufficiency may switch back and forth and binary search would be unreliable.

Evaluation uses α,β-CROWN and compares against the standard greedy subset-minimal algorithm under two orderings:

Authors’ abstract

Despite significant progress in post-hoc explanation methods for neural networks, many remain heuristic and lack provable guarantees. A key approach for obtaining explanations with provable guarantees is by identifying a cardinally-minimal subset of input features which by itself is provably sufficient to determine the prediction. However, for standard neural networks, this task is often computationally infeasible, as it demands a worst-case exponential number of verification queries in the number of input features, each of which is NP-hard. In this work, we show that for Neural Additive Models (NAMs), a recent and more interpretable neural network family, we can efficiently generate explanations with such guarantees. We present a new model-specific algorithm for NAMs that generates provably cardinally-minimal explanations using only a logarithmic number of verification queries in the number of input features, after a parallelized preprocessing step with logarithmic runtime in the required precision is applied to each small univariate NAM component. Our algorithm not only makes the task of obtaining cardinally-minimal explanations feasible, but even outperforms existing algorithms designed to find the relaxed variant of subset-minimal explanations - which may be larger and less informative but easier to compute - despite our algorithm solving a much more difficult task. Our experiments demonstrate that, compared to previous algorithms, our approach provides provably smaller explanations than existing works and substantially reduces the computation time. Moreover, we show that our generated provable explanations offer benefits that are unattainable by standard sampling-based techniques typically used to interpret NAMs.