How Interpretable Is “Interpretable” Machine Learning?

The modern machine learning (ML) revolution has led to ML systems deployed at scale for the first time, substantially impacting society beyond computer science experts. It is critical that these systems are integrated appropriately with minimal negative side effects, and an important component of this goal is identifying whether these tools are interpretable by humans. Formal methods is a computer science discipline that may address this problem via mathematically grounded techniques for specifying and verifying the desired operation of software and hardware systems. In the ML context, ML systems may be designed to output a set of formal specifications that describe precisely what they learned, which can then be translated into a set of natural language rules. A widespread belief in the formal methods community is that the use of their approaches in machine learning lends interpretability to systems, making their reasoning understandable by humans. We evaluate the claim that formal specifications are interpretable by humans via an experiment with sixty-two participants. We describe the format of the study, provide statistical analysis of the results, and recommend modifications to researchers’ claims and ergonomic improvements to data presentation and validation training.