  Program synthesis is the task of automatically generating code based on a
specification. In Syntax-Guided Synthesis (SyGuS) this specification is a
combination of a syntactic template and a logical formula, and the result is
guaranteed to satisfy both.
  We present a reinforcement-learning guided algorithm for SyGuS which uses
Monte-Carlo Tree Search (MCTS) to search the space of candidate solutions. Our
algorithm learns policy and value functions which, combined with the upper
confidence bound for trees, allow it to balance exploration and exploitation. A
common challenge in applying machine learning approaches to syntax-guided
synthesis is the scarcity of training data. To address this, we present a
method for automatically generating training data for SyGuS based on
anti-unification of existing first-order satisfiability problems, which we use
to train our MCTS policy. We implement and evaluate this setup and demonstrate
that learned policy and value improve the synthesis performance over a baseline
by over 26 percentage points in the training and testing sets. Our tool
outperforms state-of-the-art tool cvc5 on the training set and performs
comparably in terms of the total number of problems solved on the testing set
(solving 23% of the benchmarks on which cvc5 fails). We make our data set
publicly available, to enable further application of machine learning methods
to the SyGuS problem.
