Abstract
There is significant room for improving program synthesis algorithms in terms of scalability and quality of target programs. I will present a framework based on the counterexample-guided inductive synthesis (CEGIS) paradigm where the generator is a neural agent and the verifier is a symbolic solver. The neural agent allows to effectively adapt the search strategy, circumvents the need for hand-engineered heuristics, and is able to generate higher quality programs faster. I will demonstrate how this architecture improves upon existing approaches for diverse tasks over graph structured data, such as loop invariant generation, syntax-guided synthesis from logical specifications, constrained Horn clause solving, and programmatic expression generation for referring to objects in images.
This is joint work with Aaditya Naik, Jiani Huang, Xujie Si, and Osbert Bastani (UPenn), Hanjun Dai and Rishabh Singh (Google Brain), and Le Song (Georgia Tech).