We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. Specifically, we introduce the notion of equivalence modulo conflict and show how this idea can be used to learn useful lemmas that allow the synthesizer to prune large parts of the search space. We have implemented a general-purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate the substantial benefits of conflict-driven learning and show that Neo outperforms two state-of-the-art synthesis tools, Morpheus and Deepcoder, that target these respective domains.
Thu 21 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:40 | Synthesis and LearningPLDI Research Papers at Grand Ballroom CD Chair(s): Xin Zhang Massachusetts Institute of Technology, USA | ||
14:00 25mTalk | A General Path-Based Representation for Predicting Program Properties PLDI Research Papers Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion Media Attached | ||
14:25 25mTalk | Program Synthesis using Conflict-Driven Learning PLDI Research Papers Yu Feng University of Texas at Austin, USA, Ruben Martins Carnegie Mellon University, Osbert Bastani Stanford University, Işıl Dillig UT Austin Media Attached | ||
14:50 25mTalk | Accelerating Search-Based Program Synthesis using Learned Probabilistic Models PLDI Research Papers Woosuk Lee University of Pennsylvania, USA, Kihong Heo University of Pennsylvania, USA, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania Media Attached | ||
15:15 25mTalk | Inferring Crypto API Rules from Code Changes PLDI Research Papers Rumen Atanasov Paletov , Petar Tsankov ETH Zurich, Veselin Raychev ETH Zurich, Martin Vechev ETH Zürich Media Attached |