Traditionally, machine learning (ML) is used to find a function from data to optimize a numerical score. On the other hand, traditionally, synthesis is used to find a function (or a program) from a grammar that satisfies a logical specification. The boundary between ML and synthesis has been blurred by some recent work. However, this interaction between ML and synthesis has not been fully explored. In this thesis, we focus on the problem of finding a function given large amounts of data such that it satisfies a logical specification and also optimizes a numerical score over the input data. We present a framework to solve this problem in two impactful application domains: formula simplification and database entity matching (EM).
First, we present a system called SWAPPER based on our framework that can automatically generate code for efficient formula simplifiers specialized to a class of problems. Formula simplification is an important part of modern constraint solvers and writing efficient simplifiers has largely been an arduous manual task. Evaluation of SWAPPER on multiple applications of the SKETCH constraint solver showed 15-60% improvement over the existing hand-crafted simplifier in SKETCH.
Second, we present a system called EM-SYNTH based on our framework that generates as effective and more interpretable EM rules than the state of the art techniques. Database entity matching is a critical part of data integration and cleaning, and, usually involves learning rules or classifiers from labeled examples. Evaluation of EM-SYNTH on multiple real-world datasets against other interpretable (shallow Decision Trees, SIFI ) and non-interpretable methods (SVM, deep Decision Trees) showed that EM-SYNTH generates more concise and interpretable rules without sacrificing much accuracy.
Thesis Committee: Prof. Armando Solar-Lezama, Prof. Adam Chlipala, Prof. Samuel Madden