TITLE: Program Synthesis at the Edge of Artificial Intelligence
Program synthesis, the problem of automatically discovering programs that implement a given specification, is a long-standing goal in computer science. The last decade has seen a resurgence of interest in this area. Many new algorithmic solutions to the problem have emerged, and diligent engineering and the availability of powerful hardware have raised hopes for practical deployment.
While this "surge" has primarily taken place in the programming languages (PL) community, it is now becoming clear that progress in program synthesis can broadly impact applications across computer science. Specifically, my group has worked on applications of program
synthesis in artificial intelligence for quite some time, and in this talk I will describe some of this work.
The talk starts with the observation that the essential AI tasks of learning and motion planning can be naturally formulated as program synthesis. Learning is formulated as the automatic discovery of a statistical model, represented as a program in a higher-level language
with symbolic and neural components, that optimally fits a dataset. Motion planning is framed as the automatic discovery of a high-level program that directs a robot's behavior, and that can be "executed" by a specific robot in a specific physical environment. The problems are then solved using a combination of symbolic methods for program synthesis, and traditional sampling- or optimization-based methods for learning and motion planning.
I will speak about two concrete bodies of work that implement this worldview, each drawing an arc from foundational research on program synthesis and ending with applications in machine learning and robotics. The first of these starts with a procedure for synthesis of
functional programs (published in the PL community), then applies it to synthesize programmatic classifiers and reinforcement learning policies (published in the ML community). The second starts with amethod for synthesis of reactive programs (published in a PL venue), and applies it in the setting of safe-by-construction robot motion planning under adversarial and uncertain environments (published in the robotics community). These efforts illustrate the value of the view of learning/planning as program synthesis: specifically, that it facilitates the discovery of plans/models that are easier to interpret, are guaranteed to satisfy a set of formal requirements, can leverage domain-specific axiomatic knowledge, and can reuse knowledge from previously performed tasks. They also open up a playground of new algorithmic problems, and form the beginnings of a long-term agenda of marrying formal methods with artificial intelligence.
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).