FAME: Formal Abstract Minimal Explanation for Neural Networks

TL;DR

FAME is the first method to scale to large neural networks while reducing explanation size and benchmark FAME against VERIX+ and demonstrates consistent gains in both explanation size and runtime on medium- to large-scale neural networks.

Abstract

We propose FAME (Formal Abstract Minimal Explanations), a new class of abductive explanations grounded in abstract interpretation. FAME is the first method to scale to large neural networks while reducing explanation size. Our main contribution is the design of dedicated perturbation domains that eliminate the need for traversal order. FAME progressively shrinks these domains and leverages LiRPA-based bounds to discard irrelevant features, ultimately converging to a formal abstract minimal explanation. To assess explanation quality, we introduce a procedure that measures the worst-case distance between an abstract minimal explanation and a true minimal explanation. This procedure combines adversarial attacks with an optional VERIX+ refinement step. We benchmark FAME against VERIX+ and demonstrate consistent gains in both explanation size and runtime on medium- to large-scale neural networks.

Figures (6)

• Figure 1: FAME Framework. The pipeline operates in two main phases (1) Abstract Pruning (Green) phase leverages abstract interpretation (LiRPA) to simultaneously free a large number of irrelevant (pixels that are certified to have no influence on the model's decision) features based on a batch certificate (Section \ref{['sec:abstract-simult-freeing']}). This iterative process operates within a refined, cardinality-constrained perturbation domain, $\Omega^m(x,A)$ (Eq. \ref{['eq:refined-domain']}) to progressively tighten the domain; To ensure that the final explanation is as small as possible, the remaining features that could not be freed in batches are tested individually (Section \ref{['sec:perturbation_domain']}). (2) Exact Refinement (Orange) phase identifies the final necessary features using singleton addition attacks and, if needed, a final run of (Section \ref{['sec:distance-to-minimality']}). The difference in size, $\lvert \text{$\text{wAXp}^{A^{\star}}$} \rvert - \lvert \text{AXp} \rvert$, serves as an evaluation metric of phase 1.
• Figure 2: FAME's iterative refinement approach against the baseline. The left plot compares the size of the final explanations. The right plot compares the runtime (in $seconds$). The data points for each model are distinguished by color, and the use of circles (card=True) and squares (card=False) indicates whether a cardinality constraint ($||x-x'||_{0}\le m$) was applied.
• Figure 3: Toy example illustrating the asymmetry between adding and freeing features.
• Figure 4: A 3D classification task.
• Figure 5: AXps with different properties.

Theorems & Definitions (12)

• Definition 2.1
• Definition 4.1: Abstract Abductive Explanation ($\text{wAXp}^A$)
• Proposition 4.1: Simultaneous Freeing
• Definition 4.2: Abstract Batch Certificate
• Proposition 4.2: Batch-Certifiable Freeing
• Lemma 4.1
• Proposition B.1: Simultaneous Addition
• proof : Simultaneous Addition \ref{['lemma:simultaneous_add']}
• proof : Simultaneous freeing \ref{['lemma:simultaneous_free']}
• proof : Batch-Certifiable Freeing \ref{['lemma:batch-certificate']}