Efficiently Computing Compact Formal Explanations

TL;DR

VeriX+ advances formal explanation methods for machine learning by significantly reducing explanation size and generation time through novel sensitivity and traversal techniques, enabling scalable and practical applications.

Contribution

We introduce VeriX+, which enhances the size and speed of formal explanations using new sensitivity bounds and binary search traversal, building on and improving VeriX.

Findings

38% reduction in explanation size on GTSRB

90% faster explanation generation on MNIST

Scalable to transformers and real-world scenarios

Abstract

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.