Grammar Filtering For Syntax-Guided Synthesis

Programming-by-example (PBE) generates functions from input-output examples but is often too slow for real-time use. Traditional approaches use automated reasoning tools or machine learning techniques. This paper proposes a hybrid system using machine learning to preprocess Syntax Guided Synthesis (SyGuS) problems, reducing search space and enabling faster solutions. The system reduces the runtime of the 2019 SyGuS Competition PBE Strings track winner by 47.65%, outperforming all competing tools.

Program synthesis automatically generates code to meet specifications, focusing on what the code should achieve rather than how it's implemented. Where the specifications can be given as a set of constraints, inferred from program environments, or derived from large data sets. PBE exemplifies this approach, where users provide input-output examples to generate code that generalizes beyond the given examples.

The Syntax Guided Synthesis (SyGuS) format standardizes synthesis problems, defining constraints and grammars to construct programs. However, the real-world applications often require larger grammars, impacting synthesis efficiency. Hence, as per experimentation it is found out that by manually removing some parts of the grammar, the synthesis times can be improved.

A SyGuS synthesis problem consists of a tuple (C, G) where C represents constraints, restricted to pairs (i, o) of input-output examples within the domain of Programming by Example (PBE). G is a context-free grammar from which terminal symbols (e.g., +, -, str.length) construct programs. Notation π(G) denotes the set of terminal symbols in G.

SyGuS aims to find a program P ∈ G satisfying all constraints C. If found within time t, we write (G, C)→t P; otherwise, (G, C)≠t P, with a typical timeout of 3600 seconds.

Gcrit, containing critical terminals for a solution, is also derived from G. The goal in this paper is to identify a grammar G*, a reduced grammar where π(Gcrit) ⊆ π(G*) ⊆ π(G). This will minimize the search space.

The approach this paper uses with GRT demonstrates substantial performance gains over existing SyGuS solvers by leveraging neural network predictions to prune grammar terminals and improve synthesis efficiency.

By encoding semantic approximations into the neural network trained on interpreter output data, the search space is reduced without introducing new timeouts.

However, this paper can be improved, as currently it's predictions of time savings by removing terminals relies on average expected values, which could benefit from more sophisticated neural network strategies tailored to SyGuS problem constraints.