SHF: Medium: Collaborative Research: Bridging Automated Formal Reasoning and Continuous Optimization for Provably Safe Deep Learning

University Of Texas At Austin, Austin TX

Investigators

Abstract

Deep neural networks have emerged as a transformative computing technology in the last few years. However, as illustrated by recent research on adversarial machine learning, they can behave in obviously erroneous ways on anomalous or adversarial inputs and cannot be debugged using traditional software development methods. Thus, there is an urgent need for developing formal methods techniques that can assure the safety of neural networks, particularly in safety- or security-critical application domains. Motivated by this problem, this project investigates automated formal reasoning techniques for provably safe deep learning. In particular, the investigators explore verification methods for certifying robustness properties of trained networks as well as new verified training methods for finding network parameters that are safe by construction. The technical approach closely couples techniques for automated formal reasoning about systems (in particular abstraction) and continuous optimization. In particular, the project explores the use of automated abstraction techniques, originally developed for reasoning about human-written programs, in the analysis of neural networks. The project investigates the coupling of abstraction and gradient-based optimization in searching for correctness proofs and network parameters. The project introduces undergraduate and high school students from underrepresented groups to research on programming languages and formal methods through outreach programs centered around the topics on artificial intelligence. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.