Grammar Filtering for Syntax-Guided Synthesis
Authors: Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac, Mark Santolucito1611-1618
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluated GRT by running it on the Sy Gu S Competition Benchmarks from 2019 in the PBE Strings track. We found GRT outperformed CVC4, the winner of the Sy Gu S Competition from 2019, reducing the overall synthesis time by 47.65%. |
| Researcher Affiliation | Academia | Kairo Morton,1 William Hallahan,2 Elven Shum,3 Ruzica Piskac,2 Mark Santolucito2 1George School, 2Yale University, 3Deerfield Academy mortonk@georgeschool.org, {william.hallahan, ruzica.piskac, mark.santolucito}@yale.edu, eshum20@deerfield.edu |
| Pseudocode | No | The paper describes the approach procedurally but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions implementing their approach in a 'modular tool, GRT,' but does not provide concrete access to its source code, nor does it state that the code is open-source or publicly available. |
| Open Datasets | Yes | The Sy Gu S competition (Alur et al. 2017) provides public competition benchmarks and results from previous years. In particular, the PBE Strings dataset provides a collection of PBE problems over a grammar that includes string, integer, and Boolean manipulating functions. |
| Dataset Splits | No | The paper describes generating a training set (TRcrit and TRtime) and using existing SyGuS competition benchmarks, but does not specify explicit training/validation/test dataset splits for the overall experimental evaluation that would allow reproduction of the data partitioning. |
| Hardware Specification | Yes | All experiments were run on Mac Book Pro with a 2.9 Gh Z Intel i5 processor with 8GB of RAM. |
| Software Dependencies | No | The paper mentions using 'Keras Framework' and 'CVC4' but does not provide specific version numbers for these software components. |
| Experiment Setup | Yes | Our model is made up of five fully connected layers: the input layer, three hidden layers, and the output layer. By using the Keras Framework, we include an embedding layer along with our input layer which enables us to create unique vector embeddings of length 100 for any given input-output pair in the dataset... The hidden layers of the model are all fully connected, and all use the sigmoid activation function. In addition, we implement dropout during training to ensure that overfitting does not occur... Our model used the Adam optimization method and the binary-cross entropy loss function as it is well suited for multi-label classification. Overall, our model was trained on 124928 data points for 15 epochs with a batch size of 200 producing a training time of 228 seconds. |