Dr. Guy Katz

Researcher interests: Creating complex software is difficult, and so people have started using machine learning (ML) to generate software instead of writing it manually. The problem: ML-produced software is opaque to humans, and it is difficult to certify that it always behaves correctly. In safety-critical systems, i.e. autonomous vehicles, this raises serious concerns. As part of my research, I seek to develop techniques and tools that will allow us to formally reason about deep neural networks (a specific kind of ML-produced software), and in particular to verify that they are correct. Research on neural network verification is still at an early phase, and there are many challenges to overcome. First, there is the matter of scalability: the verification problem is NP-complete, i.e. is exponentially difficult in the size of the network, and so it is challenging to apply verification to large networks. Our research group is addressing this difficulty by applying state-of-the-art techniques from the fields of verification, linear programming and SMT solving. Another interesting topic is that of applications: verification of neural networks is a useful hammer, and we are just beginning to discover all the potential nails. One project where we've successfully applied this technique is the ACAS Xu system: an airborne collision-avoidance systems for drones, currently being developed by the US Federal Aviation Administration (FAA). The ACAS Xu system includes 45 deep neural networks, and it is very important that these networks behave correctly as to avoid potential mid-air collisions. Using verification, we were able to formally prove that this is indeed the case (for a list of desired properties), and in one case even detected a bug. Another interesting application is robustness to adversarial examples, where we use verification to prove that small perturbations to a network's inputs do not cause it to make mistakes.