May 7-10, 2017 Asilomar, California
Marrying program synthesis and computational learning theory
Loris D'Antoni
Program synthesis has become a central topic in computer science and it has been used to solve many practical problems that can make the lives of programmers easier. Despite the practical successes, we are still far far from understanding why and when synthesis algorithms work. A similar "lack of understanding" phenomenon occurred in the early days of machine learning and lead to the study of computational learning theory, which explained convergence and runtime properties of machine learning algorithms and increased our understanding of them. It is therefore natural to ask, can we develop a computational synthesis theory that will help us understand program synthesis? We propose a first step in this direction and present an algorithm for synthesizing probabilistic programs that adhere to a certain specification. We borrow notions from computational learning theory and prove that, under certain assumptions, our algorithm converges to correct solutions using polynomially many steps.