Efficiently Computing Compact Formal Explanations
This work addresses the need for efficient and compact formal explanations in AI, particularly for applications like autonomous systems and sentiment analysis, though it is incremental as it builds on prior work.
The paper tackles the problem of generating formal explanations for machine learning models by introducing VeriX+, which improves both the size and generation time of explanations, achieving a 38% size reduction on GTSRB and a 90% time reduction on MNIST.
Building on VeriX (Verified eXplainability, arXiv:2212.01051), a system for producing optimal verified explanations for machine learning models, we present VeriX+, which significantly improves both the size and the generation time of formal explanations. We introduce a bound propagation-based sensitivity technique to improve the size, and a binary search-based traversal with confidence ranking for improving time -- the two techniques are orthogonal and can be used independently or together. We also show how to adapt the QuickXplain algorithm to our setting to provide a trade-off between size and time. Experimental evaluations on standard benchmarks demonstrate significant improvements on both metrics, e.g., a size reduction of $38\%$ on the GTSRB dataset and a time reduction of $90\%$ on MNIST. We demonstrate that our approach is scalable to transformers and real-world scenarios such as autonomous aircraft taxiing and sentiment analysis. We conclude by showcasing several novel applications of formal explanations.