FAME: Formal Abstract Minimal Explanation for Neural Networks
Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe, Shahaf Bassan, Guy Katz
TL;DR
FAME introduces a scalable, formal method for generating minimal explanations of neural network decisions using abstract interpretation, reducing explanation size and improving efficiency over existing approaches.
Contribution
It is the first approach to scale formal explanations to large neural networks by using dedicated perturbation domains and LiRPA bounds, eliminating traversal order dependence.
Findings
FAME produces smaller explanations than previous methods.
FAME demonstrates faster runtimes on large neural networks.
FAME maintains high explanation quality with a new evaluation procedure.
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…
Peer Reviews
Decision·ICLR 2026 Poster
1. The paper presents a novel approach to formal explanations, eliminating the traditional traversal order bottleneck. This is a significant step forward in making formal XAI methods scalable to large networks. 2. The proposed FAME framework is sound, and the experiments demonstrate its potential to scale well with complex networks. 3. The writing is generally clear, and the method is presented in an organized way. The diagrams and figures help illustrate key points effectively.
**Traversal Order Issue:** The paper claims to eliminate traversal relationships, but the algorithm still performs multiple rounds of feature selection, which can be considered a form of traversal. This method needs further clarification to truly eliminate traversal relationships. **Impact of Feature Order:** The paper underestimates the significant impact that the order of feature selection has on the results. A more thorough discussion and empirical validation are required. Specifically, when
- Formally computing explanations with guarantees for neural networks is a critical and important research problem, with room for novel contribution. - The approach is described in coherent manner, and paper storytelling is linear.
- Coming from a different community, I found hard to familiarize with the jargon, as some key concepts are left without definition (e.g. abstract interpretation, LiRPA). They may be second nature for the authors, but gently introducing them would help clarify and broaden up the audience. - The paper could use some examples, to ease the understanding from a broader audience (e.g. when introducing the verification task, 99-102, or by providing additional examples properties to verify $P$ - other t
* The paper shows a novel approach to breaking the 'sequential bottleneck' in formal XAI. * Using LiRPA-based abstract interpretation (which is GPU-accelerated), instead of CPU-bound solvers, is practical. This can speed up and improve scalability. * The formulation of batch freeing as a knapsack problem is a clever and effective
### 1. Data The experiments are limited to MNIST and GTSRB. These are relatively small-scale and low-dimensional datasets. The paper's claim to "scale to large neural networks" is not fully substantiated by this evidence. The scalability of FAME on high-dimensional data (e.g., CIFAR-100 or ImageNet) is a major open question. ### 2. Model Similarly, the models used (small FC and CNNs) are not "large-scale" by modern standards (e.g., ResNets, Transformers). The quality of LiRPA bounds is known to
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsExplainable Artificial Intelligence (XAI) · Adversarial Robustness in Machine Learning · Advanced Graph Neural Networks