LEARNING A META-SOLVER FOR SYNTAX-GUIDED PROGRAM SYNTHESIS
A general formulation of program synthesis called syntax-guided synthesis (SyGuS) seeks to synthesize a program that follows a given grammar and satisfies a given logical specification. Both the logical specification and the grammar have complex structures and can vary from task to task, posing significant challenges for learning across different tasks. Moreover, supervision is often unavailable for domain-specific synthesis tasks. To address these challenges, we propose a metalearning framework that learns a transferable policy using only weak supervision. Our framework consists of three components: 1) an encoder, which embeds both the logical specification and grammar at the same time using a graph neural network; 2) a grammar adaptive policy network which enables learning a transferable policy; and 3) a reinforcement learning algorithm that jointly trains the embedding and adaptive policy with sparse reward. We evaluate the framework on 214 cryptographic circuit synthesis tasks. It solves 141 of them in the out-of-box solver setting, significantly outperforming a similar search-based approach but without learning, which solves only 31. The result is comparable to two state-of-the-art classical synthesis engines, which solve 129 and 153 respectively. In the metasolver setting, the framework can efficiently adapt to unseen tasks and achieves speedup ranging from 2× up to 100×.
This paper presents a (meta-)solver for particular program synthesis problems, where the model has access to a (logic) specification of the program to be synthesized, and a grammar that can change from one task instance to another. The presented model is an RL-based model that jointly trains 1) the joint graph-based embedding of the specification and the grammar, and 2) a policy able to operate on different (from instance to instance) grammars. Interestingly, not only can the model operate as a stand-alone solver, but it can be run as a meta-solver - trained on a subset of tasks, and applied (with tuning) on a new task. Experiments show that the model outperforms two baselines (one being a (near-to-)SOTA model) in the stand-alone setting and that the model successfully transfers knowledge (considers fewer candidates) in the meta-solving mode.
First, I enjoyed reading the paper. I think the problem is interesting, particularly due to the model being able to train and operate on various grammars (from task to task), and not on a single, pre-specified grammar. The additional bonus is that the problem the paper solves does not require program as supervision, but an external verifier.
The evaluation shows that this approach not only makes sense but (significantly) outperforms, under same conditions, specialized program synthesis programs. However, there’s one issue here, and that’s what the comparison hasn’t been done to SOTA model but to a less performant model (see issues). 
The particular approach of jointly training a specification+grammar graph embedding and learning a policy that acts on different grammars seems original and significant enough for publication.
The paper is well (with a few kinks) written, and mostly clear. There are still some issues in the paper.
Issues:
- The dataset used is 210 cryptographic circuit synthesis tasks from SyGuS 2017. Why only this particular subset of all the tasks, and not the other tasks/categories (there is 569 of them in total, no)?
- Alur et al mention 214 examples in the said tasks, yet the paper says 210. Why?
- The SyGuS results paper https://arxiv.org/abs/1711.11438 mentions EUSolver as the SOTA model, solving 152 tasks (out of 214). Why didn’t you compare your model to EUSolver?
- The same paper reports CVC4 solving 117 tasks (out of 214), as opposed to 129 (out of 210) reported in your paper. Could you comment on the (possible) differences in the experimentation protocol?
- you mention global graph embedding, but you never describe how you calculate it
- abstract mentions outperforming two SOTA engines, but later you say ESymbolic is a baseline (which it seems by description)
Questions:
- W for different edge types and different propagation steps t? Why is there a need for such a large number of parameters? What is the number of propagation steps?
- In the extreme case where all inputs can be enumerated - how often does this happen in the tasks you solve?
- figure 2 is not clear. There is too much information on one side (grammar) and too little on the other (what is the meaning of \tau^(t-1)?)? Is the tree on the right a generated subtree?
- details of the state s are unclear - it is tracked by an LSTM? Is there a concrete training signal for s, or is it a part of the architecture and everything is end-to-end trainable from the final reward? The same for s0=MLP(h(G)) - is that also trained in the same way?
- can you provide some intuition on why you chose that particular architecture (state-tracking LSTM,  s0 as such, instead of something simpler?)
- can you provide details on the state value estimator MLP architecture, as well as the s0 MLP, and the state-tracking LSTM?
- the probability of each action (..) is defined as ….H_\alpha^(i) - what does the i stand for? Was that supposed to be the t or \alpha_t was supposed to be \alpha_i?
Minor stuff:
- Figure 5a is referred to as Table 5a in the text
- out-of-out-solver
- global graph embedding, figure 1 - G(phi, G), figure 2 - h(G)
- a figure of the policy architecture would be beneficial
- Figure 1
  - d_1 ->X OR Y in the graph is d1T, why isn’t it d1_OR, and connected to the OR node?
  - why isn’t d1_OR connected to OR node?
  - AST edge - but grammar is a DAG - (well, multigraph)
  - what are the reversed links? e.g. if A->B, reversed link is B->A ?
  - what is the meaning of the concrete figures in ‘one step’?
- consider relating to ‘DREAMCODER: Bootstrapping Domain-Specific Languages for Neurally-Guided Bayesian Program Learning’ (https://uclmr.github.io/nampi/extended_abstracts/ellis.pdf), as it’s another model that steps away from the fixed-DSL story