Research map / Reinforcement learning / Visual and representation RL
Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes an MCTS-based SyGuS solver guided by RL-trained XGBoost policy and value models, plus an anti-unification method for generating new SyGuS training problems from SMT problems.
Problem
Syntax-guided synthesis (SyGuS) with logical specifications lacks training data, so machine-learned search heuristics have been hard to apply and enumerative solvers dominate.
Approach
Frames SyGuS as a single-player game searched by AlphaZero-style MCTS with UCT, where policy and value functions are gradient-boosted trees trained in an RL loop, and training data is generated from first-order SMT problems via (anti-)unification to yield feasible specifications with new solutions.
Key results
- Best RL iteration solves 859.8 of 1425 training problems (60.3%) vs 33.1% baseline, and 289 of 476 test problems (60.7%) vs 34.3% baseline.
- On the test set the tool solves about 6 fewer problems than cvc5 (289 vs 295), while outperforming cvc5 on the training set (859.8 vs 834 on average).
- Training on new generated problems raises solved fraction on the new training set to 93.2% versus cvc5's 77.0%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| train policy and value guidance through the RL loop | MCTS SyGuS synthesizer · Exp. 1 train, old + new | solved (%): 33.1% -> 60.3% | Helped |
| train policy and value guidance through the RL loop | MCTS SyGuS synthesizer · Exp. 1 test, old + new | solved (%): 34.3% -> 60.7% | Helped |
| train policy and value guidance through the RL loop | MCTS SyGuS synthesizer · Exp. 2 test, old* | solved (%): 16.6% -> 30.7% | Helped |
| train policy and value guidance using generated new problems | MCTS SyGuS synthesizer · Exp. 3 test, old | solved (%): 15.9% -> 18.3% | Helped |
| train exclusively on generated new problems rather than old problems | MCTS SyGuS synthesizer · old test set, Exp. 3 versus Exp. 2 | solved (%): 30.7% vs 18.3% | Hurt |
| use the proposed MCTS + RL method instead of cvc5 | SyGuS LIA synthesis · Exp. 1 train, old + new | solved (%): 58.5% -> 60.3% | Helped |
| use the proposed MCTS + RL method instead of cvc5 | SyGuS LIA synthesis · Exp. 1 test, old + new | solved (%): 62.0% vs 60.7% | Hurt |
| use the proposed MCTS + RL method instead of cvc5 | SyGuS LIA synthesis trained on generated problems · Exp. 3 train, new | solved (%): 77.0% -> 93.2% | Helped |
Surprising findings
- Training on newly generated problems did not improve performance on old test problems compared with training on old data (18.3% vs 30.7%), which the authors attribute to the new benchmarks being atypical.
Limitations
- No comparison with specialized invariant synthesis tools or Euphony (code did not compile).
- Requires an initial set of solved problems in the first iteration to generate training data.
- Data generation only applies to domains where first-order verification problems are available.
Experimental setup
Datasets: SyGuS competition LIA benchmarks SMT-LIB LIA and QFLIA problems (used to generate new SyGuS problems)
Benchmarks: SyGuS LIA (old SyGuS competition benchmarks) generated SyGuS LIA problems (new)
Metrics: number of problems solved percentage solved time-out 100s
Baselines: cvc5 first iteration of RL loop (default policy/value)
Builds on: AlphaZero UCT XGBoost
Closest papers by meaning
- Online Prompt Selection for Program Synthesis (AAAI 2025 · similarity 0.87)
- $\mathcal{B}$-Coder: Value-Based Deep Reinforcement Learning for Program Synthesis (ICLR 2024 · similarity 0.87)
- HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis (NeurIPS 2024 · similarity 0.86)
- Program Synthesis via Test-Time Transduction (NeurIPS 2025 · similarity 0.86)
- Learning to Reason via Program Generation, Emulation, and Search (NeurIPS 2024 · similarity 0.85)
- Generating Code World Models with Large Language Models Guided by Monte Carlo Tree Search (NeurIPS 2024 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.