Program Synthesis for Reliable and Interpretable Artificial Intelligence

We are currently in an "aI spring" , largely fueled by recent
breakthroughs in deep learning. However, deep neural networks have
certain well-known flaws: they are susceptible to adversarial
examples, are difficult to interpret, debug and verify, can be
exceedingly data-hungry, and sometimes do not generalize well. These
flaws make the design of reliable systems with neural components an
especially challenging task.

In this talk, I will argue that viewing machine learning as program
synthesis — the automatic discovery of high-level programs that
satisfy a specification — can provide a way around many of these
difficulties. Program synthesis is an old problem that has had a
recent renaissance in the Formal Methods community. Framed as program
synthesis, machine learning becomes the problem of automatically
discovering a model (represented as a program in a high-level
"neurosymbolic" language) that optimally fits a dataset and satisfies
additional correctness invariants such as robustness. Such a
formulation has a number of advantages. First, it is easier to enforce
formal safety guarantees at the time of learning as opposed to after
the fact, and at the level of high-level programs as opposed to
low-level neural networks. Second, high-level models are easier to
interpret, and more easily constrained by domain-specific insights,
than neural nets. Third, the compositional representation offered by
modern programming languages can aid transfer of knowledge across
learning tasks, and reduce the need for data. Fourth, the syntactic
constraints of a programming language can serve as a form of
regularization, allowing the model to generalize better.

The fundamental algorithmic challenge in program synthesis is that it
is a hard combinatorial optimization problem. I will describe a few
recent efforts from my group that approach this challenge using a mix
of ideas from Formal Methods and Deep Learning. One of these methods
learns a neural representation of the target function using
gradient-based techniques, then synthesizes a high-level program that
imitates the behavior of this neural model. A second leverages
functional programming abstractions and type-based deduction to search
a vast space of neural architectures. A third develops a series of
differentiable approximations to a program verifier that can be used
to learn model parameters while ensuring a set of Boolean correctness
properties. These results open up a playground of new algorithmic
problems, and form the beginnings of a long-term agenda of marrying
Formal Methods with Machine Learning.
Swarat Chaudhuri is an Associate Professor of Computer Science at
Rice University. He studies algorithms — based on automated
deduction, combinatorial search and optimization, and statistical
machine learning — for program analysis and synthesis, and the use
of these algorithms in practical systems that make programs more
reliable, faster, and easier to write.

Swarat received a bachelor's degree in computer science from the
Indian Institute of Technology, Kharagpur, in 2001, and a doctoral
degree in computer science from the University of Pennsylvania in
2007. From 2008-2011, he was an Assistant Professor at the
Pennsylvania State University. He is a recipient of the National
Science Foundation CAREER award, the ACM SIGPLAN John Reynolds
Doctoral Dissertation Award, the Morris and Dorothy Rubinoff
Dissertation Award, and a Google Research Award. He has served on
program committees of many conferences in Formal Methods and
Programming Languages, and chaired the 2016 Conference on
Computer-Aided Verification (CAV).