FAME: Formal Abstract Minimal Explanation for Neural Networks

📝 Paper Summary

Formal Verification Abstract Interpretation

FAME scales provable explanations to large neural networks by using abstract interpretation to certify and discard batches of irrelevant features simultaneously, removing the need for sequential traversal.

Core Problem

Formal explanations (AXp) provide mathematical guarantees but rely on exact verification (NP-hard) and sequential feature elimination, making them intractable for large networks like ResNets.

Why it matters:

Lack of transparency in neural networks undermines trust in high-stakes environments where reasoning must be verified
Existing formal methods face a sequential bottleneck (traversal order), preventing effective parallelization and scaling
Heuristic explanations estimate importance but lack provable correctness, while exact formal methods cannot handle realistic model sizes

Concrete Example: In a classification task, determining which pixels are essential for a prediction typically requires checking them one by one. Exact solvers might time out verifying a robust feature set for a ResNet on CIFAR-10, whereas FAME's abstract approach can identify the subset efficiently.

Key Novelty

Abstract Batch Certificate via LiRPA

Defines explanations on an abstract domain (using linear relaxation bounds) rather than the concrete domain, allowing for faster, conservative verification
Eliminates sequential feature traversal by formulating feature selection as a Knapsack problem, identifying a 'batch' of irrelevant features that can be removed simultaneously
Leverages the asymmetry of verification: proving features are irrelevant (freeing them) requires handling complex dependencies, which the proposed certificate does via a joint upper bound

Evaluation Highlights

First method to produce abstract formal abductive explanations for a ResNet architecture on CIFAR-10, where exact methods are intractable
Achieves O(n) time complexity for solving the feature selection Knapsack problem in binary classification settings
Demonstrates consistent gains in explanation size and runtime compared to the SOTA baseline VERIX+ on medium- to large-scale networks

Breakthrough Assessment

8/10

Significant methodology shift from exact to abstract verification for XAI. Solving the scalability bottleneck of formal explanations (ResNet/CIFAR-10 scale) is a major step forward, though reliance on approximations introduces a precision trade-off.

⚙️ Technical Details

Problem Definition

Setting: Finding a minimal subset of features (Abductive Explanation) that guarantees the model prediction remains invariant under a defined perturbation domain.

Inputs: Neural network f, input sample x, perturbation domain Omega, property P

Outputs: Abstract Minimal Explanation (subset of features fixed to their nominal values)

Pipeline Flow

Abstract Interpretation (LiRPA)
Batch Certificate Computation
Feature Selection (Greedy Heuristic)

System Modules

Abstract Interpreter

Compute linear upper and lower bounds of the model output over the perturbation domain

Model or implementation: LiRPA (Linear Relaxation based Perturbation Analysis)

Certificate Optimizer

Identify the maximal set of features that can be freed (treated as irrelevant) without violating the property

Model or implementation: Greedy Heuristic for Multidimensional Knapsack Problem (MKP)

Novel Architectural Elements

Replacement of the iterative binary verifier (SAT/UNSAT oracle) with a batch certificate based on conservative linear bounds
Formulation of the feature selection step as a Multidimensional Knapsack Problem driven by feature contribution costs

Comparison to Prior Work

vs. VERIX+: FAME eliminates the need for traversal order entirely using batch certificates, whereas VERIX+ optimizes the order
vs. DistanceAXp: FAME uses abstract interpretation for scalability, whereas DistanceAXp typically relies on exact verification
vs. Bassan and Katz (2023): FAME provides a publicly described algorithm for batch processing, whereas prior work lacked code and was slower [cited in paper]

Limitations

Relies on conservative approximations (LiRPA); if bounds are too loose, the certificate may fail to identify irrelevant features even if they exist (vacuous bounds)
The generated explanations are 'abstract minimal', which is a stronger condition than 'concrete minimal'; the explanation size might be larger than the true optimum
Greedy heuristic for the Knapsack problem is suboptimal compared to exact MILP solutions, potentially missing some freeable features

📊 Experiments & Results

Evaluation Setup

Verification of local robustness properties on neural networks to produce explanations

Benchmarks:

CIFAR-10 (Image Classification)
MNIST (Image Classification (Digit Recognition))

Metrics:

Explanation Size (cardinality of the subset)
Runtime
Worst-case distance between abstract and true minimal explanation
Statistical methodology: Not explicitly reported in the paper

Key Results

Benchmark	Metric	Baseline	This Paper	Δ
Theoretical Analysis	Time Complexity (Binary Classification)	NP-hard	O(n)	Reduced from NP-hard to Linear

Main Takeaways

FAME successfully scales to ResNet architectures on CIFAR-10, a domain where exact verification methods (like Marabou) typically timeout or are intractable
The method eliminates the 'circular dependency' of traversal order: previous methods needed feature importance to order traversal, but FAME determines importance dynamically via the batch certificate
While using a greedy heuristic for the internal Knapsack problem is suboptimal, it is necessary for scalability and allows the method to parallelize feature contribution computations on GPUs

📚 Prerequisite Knowledge

Prerequisites

Formal Verification of Neural Networks
Abstract Interpretation (specifically Linear Relaxation)
Constraint Satisfaction Problems (Knapsack)

Key Terms

AXp: Abductive Explanation—a subset of features sufficient to guarantee the model's prediction remains unchanged within a perturbation domain

LiRPA: Linear Relaxation based Perturbation Analysis—an efficient method to compute linear upper and lower bounds for neural network outputs

Abstract Batch Certificate: A computed value derived from LiRPA bounds that, if non-positive, mathematically guarantees a set of features can be simultaneously treated as irrelevant

Knapsack Problem: A combinatorial optimization problem used here to maximize the number of irrelevant features 'packed' into the explanation's safety margin

Traversal Order: The sequence in which features are tested for relevance; a major bottleneck in prior sequential deletion algorithms

ResNet: Residual Network—a deep convolutional neural network architecture characterized by skip connections

CIFAR-10: A standard dataset for image classification containing 60,000 32x32 color images in 10 classes

VERIX+: The state-of-the-art baseline tool for computing formal abductive explanations using optimized traversal strategies