We study a general formulation of program synthesis called syntax-guided synthesis(SyGuS) that concerns synthesizing 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. Furthermore, training data is often unavailable for domain specific synthesis tasks. To address these challenges, we propose a meta-learning framework that learns a transferable policy from 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. 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 meta-solver setting, the framework can efficiently adapt to unseen tasks and achieves speedup ranging from 2x up to 100x. Program synthesis concerns automatically generating a program that satisfies desired functional requirements. Promising results have been demonstrated by applying this approach to problems in diverse domains, such as spreadsheet data manipulation for end-users BID21 , intelligent tutoring for students , and code auto-completion for programmers BID19 , among many others.In a common formulation posed by BID3 called syntax-guided synthesis (SyGuS), the program synthesizer takes as input a logical formula φ and a grammar G, and produces as output a program in G that satisfies φ. In this formulation, φ constitutes a semantic specification that describes the desired functional requirements, and G is a syntactic specification that constrains the space of possible programs.The SyGuS formulation has been targeted by a variety of program synthesizers based on discrete techniques such as constraint solving BID36 , enumerative search BID5 , and stochastic search BID37 . A key limitation of these synthesizers is that they do not bias their search towards likely programs. This in turn hinders their efficiency and limits the kinds of programs they are able to synthesize.It is well known that likely programs have predictable patterns BID23 BID1 . As a result, recent works have leveraged neural networks for program synthesis. However, they are limited in two aspects. First, they do not target general SyGuS tasks; more specifically:• They assume a fixed grammar (i.e., syntactic specification G) across tasks. For example, BID39 learn loop invariants for program verification, but the grammar of loop invariants is fixed across different programs to be verified. • The functional requirements (i.e., semantic specification φ) are omitted, in applications that concern identifying semantically similar programs BID34 BID0 BID2 , or presumed to be input-output examples BID33 BID7 BID16 BID11 BID13 BID43 BID42 BID35 .In contrast, the SyGuS formulation allows the grammar G to vary across tasks, thereby affording flexibility to enforce different syntactic requirements in each task. It also allows to specify functional requirements in a manner more general than input-output examples, by allowing the semantic specification φ to be a logical formula (e.g., f (x) = 2x instead of f (1) = 2 ∧ f (3) = 6). As a result, the general SyGuS setting necessitates the ability to capture common patterns across different specifications and grammars. A second limitation of existing approaches is that they rely on strong supervision on the generated program BID33 BID7 BID11 . However , in SyGuS tasks, ground truth programs f are not readily available; instead, a checker is provided that verifies whether f satisfies φ.In this paper, we propose a framework that is general in that it makes few assumptions on specific grammars or constraints, and has meta-learning capability that can be utilized in solving unseen tasks more efficiently. The key contributions we make are (1) a joint graph representation of both syntactic and semantic constraints in each task that is learned by a graph neural network model; (2) a grammar adaptive policy network that generalizes across different grammars and guides the search for the desired program; and (3) a reinforcement learning training method that enables learning transferable representation and policy with weak supervision.We demonstrate our meta-learning framework on a challenging and practical instance of the SyGuS problem that concerns synthesizing cryptographic circuits that are provably free of side-channel attacks BID17 . In our experiments, we first compare the framework in an out-of-box solver setting against a similar search-based approach and two state-of-the-art classical solvers developed in the formal methods community. Then we demonstrate its capability as a meta-solver that can efficiently adapt to unseen tasks, and compare it to the out-of-box version. We proposed a framework to learn a transferable representation and strategy in solving a general formulation of program synthesis, i.e. syntax-guided synthesis (SyGuS). Compared to previous work on neural synthesis, our framework is capable of handling tasks where 1) the grammar and semantic specification varies from task to task, and 2) the supervision is weak. Specifically, we introduced a graph neural network that can learn a joint representation over different pairs of syntactic and semantic specifications; we implemented a grammar adaptive network that enables program generation to be conditioned on the specific task; and finally, we proposed a meta-learning method based on the Advantage Actor-Critic (A2C) framework. We compared our framework empirically against one baseline following a similar search fashion and two classical synthesis engines. Under the outof-box solver setting with limited computational resources and without any prior knowledge from training, our framework is able to solve 141 of 214 tasks, significantly outperforming the baseline ESymbolic by 110. In terms of the absolute number of solved tasks, the performance is comparable to two state-of-the-art solvers, CVC4 and EUSolver, which solve 129 and 153 respectively. However, the two state-of-the-art solvers failed on 4 tasks solved by our framework. When trained as a meta-solver, our framework is capable of accelerating the solving process by 2× to 100×.
We propose a meta-learning framework that learns a transferable policy from only weak supervision to solve synthesis tasks with different logical specifications and grammars.
{"src": "scitldr-AIC_train", "paper_id": "Syl8Sn0cK7"}