# Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis

arXiv: https://arxiv.org/abs/2307.09564 · HTML: https://mlsanity.com/paper/2307.09564/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 45 references that are in the map.
- First posted on arXiv 13 Jul 2023.

## Builds on (most cited first, 20 of 20)

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [DeepCoder: Learning to Write Programs](https://mlsanity.com/paper/1611.01989/) (2016)
- [Write, Execute, Assess: Program Synthesis with a REPL](https://mlsanity.com/paper/1906.04604/) (2019)
- [Leveraging Grammar and Reinforcement Learning for Neural Program Synthesis](https://mlsanity.com/paper/1805.04276/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration](https://mlsanity.com/paper/2007.14381/) (2020)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [A Theory of Formal Synthesis via Inductive Learning](https://mlsanity.com/paper/1505.03953/) (2015)
- [What can we Learn Even From the Weakest? Learning Sketches for Programmatic Strategies](https://mlsanity.com/paper/2203.11912/) (2022)
- [Anti-unification and Generalization: A Survey](https://mlsanity.com/paper/2302.00277/) (2023)
- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [Using SyGuS to Synthesize Reactive Motion Plans](https://mlsanity.com/paper/1611.07620/) (2016)
- [Anti-unification in Constraint Logic Programming](https://mlsanity.com/paper/1907.10333/) (2019)
- [Grammar Filtering For Syntax-Guided Synthesis](https://mlsanity.com/paper/2002.02884/) (2020)
- [Learning compositional programs with arguments and sampling](https://mlsanity.com/paper/2109.00619/) (2021)
- [Predicting SMT Solver Performance for Software Verification](https://mlsanity.com/paper/1701.08466/) (2017)
- [SyGuS Techniques in the Core of an SMT Solver](https://mlsanity.com/paper/1711.10641/) (2017)

## Built on by (most cited first, 3 of 3)

- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)
- [ObscuraCoder: Powering Efficient Code LM Pre-Training Via Obfuscation Grounding](https://mlsanity.com/paper/2504.00019/) (2025)
- [ShIOEnv: A Command Evaluation Environment for Grammar-Constrained Synthesis and Execution Behavior Modeling](https://mlsanity.com/paper/2505.18374/) (2025)

## Abstract (arXiv)

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.