Invited Talk: Symbolic Reasoning About Machine Learning Systems (PADL 2020 : 22nd Symposium on Practical Aspects of Declarative Languages) - POPL 2020

I will discuss a line of work in which we compile common machine learning systems into symbolic representations that have the same input-output behavior to facilitate formal reasoning about these systems. We have targeted Bayesian network classifiers, random forests and some types of neural networks, compiling each into tractable Boolean circuits, including Ordered Binary Decision Diagrams (OBDDs). Once the machine learning system is compiled into a tractable Boolean circuit, reasoning can commence using classical AI and computer science techniques. This includes generating explanations for decisions, quantifying robustness and verifying properties such as monotonicity. I will particularly discuss a new theory for unveiling the reasons behind the decisions made by classifiers, which can detect classifier bias sometimes from the reasons behind unbiased decisions.