Towards Explainability in Machine Learning: The Formal Methods Way

Explainable Al is a new direction aiming at the maturation of a fi eld that has experienced a boost in particular because of its fancy heuristics and corresponding breakthroughs in specific applications like the AlphaGo program for the game Go. In this context, the typical concept of "explanation" is still comparatively weak. For example, highlighting the most important pixel for a certain image classification is not really a comprehensive explanation, but rather a hint, an indication that helps pinpoint situations where things went drastically wrong. In contrast we take a formal methods-based path, originally established in STTT, 5 where the concept of "explanation" is interpreted as a precise characterization of the considered phenomenon. Our illustration on how much information about the how and why can be extracted with exact methods from a random forest consisting of 100 trees indicates that such characterization may indeed turn out to be practical.