Title: Conflict-Driven Synthesis
Abstract:
Program synthesis is expanding rapidly and getting a lot of attention from both industry and academia. The goal of program synthesis is to find a program that satisfies the user intent expressed in the form of some specification. Program synthesis has proven to be useful to both end-users and programmers. For instance, program synthesis has been used to automate tedious tasks that arise in everyday life, such as string manipulations in spreadsheets or data wrangling tasks in R.
Program synthesis has also been used for improving programmer productivity by automatically completing parts of a program or helping programmers use complex APIs.
This talk will present a new conflict-driven program synthesis framework that is capable of learning from past mistakes. Given a 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. The team has 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. The experiments demonstrate an order of magnitude improvement when using conflict-driven learning and opens a new research direction that can push the boundaries of program synthesis.
Abstract:
Program synthesis is expanding rapidly and getting a lot of attention from both industry and academia. The goal of program synthesis is to find a program that satisfies the user intent expressed in the form of some specification. Program synthesis has proven to be useful to both end-users and programmers. For instance, program synthesis has been used to automate tedious tasks that arise in everyday life, such as string manipulations in spreadsheets or data wrangling tasks in R.
Program synthesis has also been used for improving programmer productivity by automatically completing parts of a program or helping programmers use complex APIs.
This talk will present a new conflict-driven program synthesis framework that is capable of learning from past mistakes. Given a 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. The team has 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. The experiments demonstrate an order of magnitude improvement when using conflict-driven learning and opens a new research direction that can push the boundaries of program synthesis.
Bio:
Ruben Martins is a Systems Scientist at Carnegie Mellon University. His interests lie in the intersection of constraint programming with program synthesis, analysis, and verification. His recent research focuses on using programming synthesis to automate data science related tasks such as data querying, imputation, consolidation, and tidying. Ruben received his PhD with honors from the Technical University of Lisbon, Portugal (2013). He was a postdoctoral researcher at University of Oxford, UK (2014-2015) and a postdoctoral researcher at UT Austin (2015-2017). He has developed several award winning constraint solvers and is the main developer of Open-WBO: an open source Maximum Satisfiability (MaxSAT) solver that won several gold medals in MaxSAT competitions.
