FAME: Formal Abstract Minimal Explanation for Neural Networks

The paper introduces FAME, a novel abductive explanation method for large neural networks that utilizes dedicated perturbation domains and LiRPA-based bounds to efficiently generate formal abstract minimal explanations, demonstrating superior performance in explanation size and runtime compared to VERIX+.

The Gist

🕵️‍♀️ The Problem: The "Black Box" Mystery

Imagine you have a super-smart robot (a Neural Network) that looks at a picture of a cat and says, "That's a cat!" But if you ask, "Why?", the robot just shrugs. It doesn't know how to explain itself.

In high-stakes situations (like self-driving cars or medical diagnosis), we can't just trust the robot. We need to know which specific parts of the input (like the cat's ears or whiskers) were actually necessary for the robot to make that decision. If we remove the ears, would it still say "cat"? If not, the ears are essential. If it still says "cat" even without the ears, the ears were just "noise."

Finding the smallest possible list of essential features is called finding a Minimal Explanation.

🚧 The Old Way: The "One-by-One" Detective

Previously, the best way to find these explanations was like a detective checking suspects one by one.

1. "Is the left ear important?" (Check: Yes/No).
2. "Is the right ear important?" (Check: Yes/No).
3. "Is the tail important?" (Check: Yes/No).

This works for small cases, but for a modern AI looking at a high-definition photo with millions of pixels, checking them one by one takes forever. It's like trying to find a needle in a haystack by picking up every single piece of hay individually. It's too slow and gets stuck.

✨ The New Solution: FAME (The "Group Detective")

The authors propose FAME (Formal Abstract Minimal Explanation). Think of FAME as a super-powered detective that doesn't check suspects one by one. Instead, it checks entire groups of suspects at once.

Here is how FAME works, using a simple analogy:

1. The "Abstract Batch Certificate" (The Group Test)

Imagine you have a room full of people (pixels). You want to know who is irrelevant to a specific crime.

• Old Way: Ask each person, "Were you involved?"
• FAME Way: FAME uses a special mathematical tool (called Abstract Interpretation) to look at a whole group of people at once. It asks: "If we let this entire group of 100 people wander around freely, would the crime still happen?"
  • If the answer is "Yes, the crime still happens," then FAME knows all 100 people are irrelevant and can be let go immediately.
  • This is the "Batch" part. It frees hundreds of pixels in a single second, something the old methods couldn't do.

2. The "Cardinality Constraint" (The Shrinking Room)

Sometimes, the group test is too loose. The math says, "Maybe they are all irrelevant," but it's not 100% sure because the room is too big.

• FAME's Trick: FAME shrinks the room. It says, "Okay, let's pretend only 5 people can move around at a time."
• By making the rules stricter (limiting how many things can change at once), the math becomes sharper. Suddenly, FAME can see that, "Oh! Even with only 5 people moving, the crime still happens. So, those 5 are also irrelevant!"
• It repeats this process, shrinking the "room" and freeing more people, until it can't free anyone else.

3. The "Final Polish" (The Safety Net)

Because FAME uses math shortcuts (approximations) to be fast, it might miss a tiny detail. It might think a pixel is irrelevant when it's actually important.

• To fix this, FAME has a final step called Exact Refinement. It takes the list of "irrelevant" pixels FAME found and runs a super-precise (but slow) check on the remaining ones to make sure the explanation is perfect.
• The Result: You get a list that is almost as small as the perfect list, but you got it hundreds of times faster.

🏆 Why is this a Big Deal?

The paper compares FAME to the current champion, VERIX+.

• Speed: FAME is like a race car compared to a bicycle. On large images, it finds explanations in seconds that used to take minutes or hours.
• Size: FAME finds smaller, cleaner lists of "why" the AI made a decision.
• Scalability: The authors tested FAME on a very complex AI (ResNet) used for recognizing objects in photos (CIFAR-10). The old methods crashed or timed out because the math was too hard. FAME succeeded where the others failed.

🧠 The Takeaway

FAME is a new way to explain AI decisions that breaks the "check one by one" bottleneck.

Instead of asking every single pixel, "Are you important?", FAME asks groups of pixels, "Are you all unimportant?" If the math says yes, it frees them all at once. It then tightens the rules to be more precise, and finally does a quick safety check.

This allows us to understand complex, large AI systems quickly and reliably, bridging the gap between "black box" mystery and "white box" clarity.

Technical Summary

Here is a detailed technical summary of the paper "FAME: Formal Abstract Minimal Explanation for Neural Networks" (ICLR 2026).

1. Problem Statement

The paper addresses the critical challenge of Explainable AI (XAI) for neural networks (NNs), specifically focusing on Formal Abductive Explanations (AXps).

• The Goal: An AXp is a minimal subset of input features that, when fixed to their nominal values, guarantees the model's prediction remains unchanged under any perturbation within a defined domain.
• The Bottleneck: Existing formal methods (e.g., VERIX+) rely on exact solvers (like SMT or MILP) and sequential feature traversal (deletion or insertion). These approaches suffer from:
  1. Scalability Issues: They are computationally intractable for large-scale or deep neural networks (e.g., ResNets).
  2. Sequential Dependency: They require a traversal order of features, which is often arbitrary or requires prior knowledge of feature importance (creating a circular dependency).
  3. High Runtime: The need for thousands of verification calls prevents practical application on complex models.

2. Methodology: The FAME Framework

FAME (Formal Abstract Minimal Explanations) introduces a hybrid framework that combines Abstract Interpretation with Adversarial Search to scale formal explanations to large networks without relying on a fixed traversal order.

Core Components:

1. Abstract Abductive Explanations ($wAXp^A$):

   • Instead of using exact verification, FAME uses Linear Relaxation-based Perturbation Analysis (LiRPA) (specifically the CROWN method) to compute sound over-approximations (linear bounds) of the network's output.
   • This allows for the simultaneous certification of large batches of irrelevant features.

2. Solving the "Freeing" Asymmetry:

   • The Insight: Adding features to an explanation (identifying them as necessary) can be parallelized. However, freeing features (identifying them as irrelevant) cannot be done naively in parallel because features may be individually irrelevant but jointly critical.
   • The Solution: FAME introduces an Abstract Batch Certificate ($\Phi$). This certificate mathematically guarantees that a set of features $A$ can be freed simultaneously if the worst-case contribution of the set does not violate the prediction property.

3. Greedy Batch Freeing (Knapsack Formulation):

   • Finding the maximal set of features to free is formulated as a 0/1 Multidimensional Knapsack Problem (MKP).
   • To ensure scalability, FAME employs a Greedy Heuristic rather than an exact MILP solver. It iteratively selects the feature with the lowest normalized cost (least likely to violate constraints) to add to the "free" set.
   • This process is highly parallelizable on GPUs.

4. Recursive Domain Refinement (Eliminating Traversal Order):

   • Instead of a static traversal order, FAME uses a Cardinality-Constrained Perturbation Domain ($\Omega_m$).
   • Mechanism:
     1. Start with a domain allowing $m$ features to vary.
     2. Use the greedy batch freeing to certify a set of irrelevant features.
     3. Refine: Restrict the domain to allow only $m$ additional features to vary (excluding those already freed).
     4. Recompute LiRPA bounds on this tighter domain. The tighter bounds often reveal more irrelevant features that were previously masked by loose approximations.
   • This recursive process continues until no new features can be freed, effectively shrinking the domain dynamically without a predefined order.

5. Exact Refinement & Quality Assessment:

   • The output of Phase 1 is a sound but potentially non-minimal abstract explanation.
   • Phase 2 (Exact Refinement): The framework optionally runs a final refinement step using exact solvers (like VERIX+ with Marabou) or adversarial attacks to remove any remaining redundant features, ensuring the final explanation is truly minimal.
   • Metric: The paper introduces a procedure to measure the "worst-case distance" between the abstract explanation and the true minimal explanation.

3. Key Contributions

1. First Scalable Formal XAI: FAME is the first method to generate formal abductive explanations for large-scale architectures (e.g., ResNet on CIFAR-10) where exact methods fail.
2. Elimination of Traversal Order: By using dedicated perturbation domains and LiRPA-based batch certificates, FAME removes the sequential bottleneck inherent in prior work (like VERIX+).
3. Abstract Minimal Explanations: It defines a new class of explanations grounded in abstract interpretation that are sound and computationally efficient.
4. Provable Quality Guarantees: It provides a method to quantify the gap between the abstract explanation and the true minimal explanation, combining adversarial search with optional exact refinement.
5. Efficient Heuristics: Demonstrates that a greedy heuristic for the batch freeing problem achieves near-optimal results (within <9 features of the optimal MILP solution) with significantly lower runtime (up to 12x faster in single rounds).

4. Experimental Results

The authors benchmarked FAME against VERIX+ (the current State-of-the-Art) on MNIST and GTSRB datasets (both Fully Connected and CNN models) and a ResNet-2B on CIFAR-10.

• Runtime Efficiency:
  • FAME is significantly faster than VERIX+. For example, on the GTSRB-CNN model, FAME achieved a 25x speedup (7.4s vs. 185s) while producing explanations of comparable or smaller size.
  • The iterative refinement step adds a modest runtime cost but yields significantly more compact explanations (e.g., reducing explanation size by 36% on MNIST-CNN).
• Explanation Size:
  • FAME consistently produces smaller (more concise) explanations than VERIX+ alone.
  • In many cases, the abstract explanation from FAME (before exact refinement) is already smaller than the minimal explanation from VERIX+.
• Scalability:
  • ResNet-2B (CIFAR-10): Exact methods (VERIX+) timed out or ran out of memory. FAME successfully processed the model, freeing an average of ~476 pixels (46% of the image) via recursive refinement, demonstrating its ability to handle deep residual networks.
• Greedy vs. MILP: The greedy heuristic used for batch freeing was found to be nearly optimal, with an average optimality gap of less than 9 features compared to the exact MILP solver, validating its use for scalability.

5. Significance

• Bridging the Gap: FAME bridges the gap between the theoretical rigor of formal verification and the practical scalability required for modern deep learning.
• Paradigm Shift: It moves the field away from sequential, traversal-based explanation generation toward batch processing and adaptive domain refinement.
• Enabling Technology: By proving that formal explanations are feasible for complex architectures like ResNets, FAME opens the door for deploying trustworthy, explainable AI in high-stakes domains (e.g., autonomous driving, medical imaging) where "black box" models are currently unacceptable.
• Hardware Utilization: The method is designed to leverage GPU acceleration (via LiRPA/CROWN), making it compatible with modern deep learning infrastructure.

In summary, FAME represents a major leap forward in Formal XAI, offering a scalable, order-independent, and mathematically sound framework for explaining neural network decisions.