Compositional synthesis of piece-wise functions by learning classifiers

Daniel Neider, Shambwaditya Saha, P. Madhusudan

Research output: Contribution to journalArticlepeer-review

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 languageEnglish (US)
Article number10
JournalACM Transactions on Computational Logic
Volume19
Issue number2
DOIs
StatePublished - Feb 2018

Keywords

  • Constraint solving
  • Counterexamples
  • Machine learning
  • Piece-wise functions
  • Program synthesis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)
  • Logic
  • Computational Mathematics

Fingerprint Dive into the research topics of 'Compositional synthesis of piece-wise functions by learning classifiers'. Together they form a unique fingerprint.

Cite this