IC Colloquium: Program Synthesis for Reliable and Interpretable Artificial Intelligence
Event details
| Date | 13.12.2018 |
| Hour | 10:15 › 11:30 |
| Location | |
| Category | Conferences - Seminars |
By: Swarat Chaudhuri - Rice University
Abstract:
We are currently in an "AI spring", largely fuelled by recent breakthroughs in machine learning. However, the deep neural networks that currently rule machine learning 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 the field of Formal Methods can offer powerful tools for overcoming these difficulties, and that in particular, there is value in seeing machine learning as a form of *program synthesis*. Program synthesis is the problem of automatically discovering high-level programs that satisfy a specification. The problem was first posed in the 1960s and has had a resurgence in the Formal Methods community in the recent past. 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 and fairness. 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 are 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 large 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.
Bio:
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).
More information
Abstract:
We are currently in an "AI spring", largely fuelled by recent breakthroughs in machine learning. However, the deep neural networks that currently rule machine learning 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 the field of Formal Methods can offer powerful tools for overcoming these difficulties, and that in particular, there is value in seeing machine learning as a form of *program synthesis*. Program synthesis is the problem of automatically discovering high-level programs that satisfy a specification. The problem was first posed in the 1960s and has had a resurgence in the Formal Methods community in the recent past. 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 and fairness. 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 are 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 large 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.
Bio:
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).
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Viktor Kuncak