Abstract
We present a novel general technique that uses classifier learning to synthesize piece-wise functions (functions that split the domain into regions and apply simpler functions to each region) against logical synthesis specifications. Our framework works by combining a synthesizer of functions for fixed concrete inputs and a synthesizer of predicates that can be used to define regions. We develop a theory of single-point refutable specifications that facilitate generating concrete counterexamples using constraint solvers. We implement the framework for synthesizing piece-wise functions in linear integer arithmetic, combining leaf expression synthesis using constraint-solving with predicate synthesis using enumeration, and tie them together using a decision tree classifier.We demonstrate that this compositional approach is competitive compared to existing synthesis engines on a set of synthesis specifications.
Original language | English (US) |
---|---|
Article number | 10 |
Journal | ACM Transactions on Computational Logic |
Volume | 19 |
Issue number | 2 |
DOIs | |
State | Published - Feb 2018 |
Keywords
- Constraint solving
- Counterexamples
- Machine learning
- Piece-wise functions
- Program synthesis
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science
- Logic
- Computational Mathematics