Just-in-Time Learning for Bottom-Up Enumerative Synthesis

被引:27
作者
Barke, Shraddha [1 ]
Peleg, Hila [1 ]
Polikarpova, Nadia [1 ]
机构
[1] Univ Calif San Diego, San Diego, CA 92093 USA
来源
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2020年 / 4卷 / OOPSLA期
基金
美国国家科学基金会;
关键词
Program Synthesis; Probabilistic models; Domain-specific languages;
D O I
10.1145/3428295
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
A key challenge in program synthesis is the astronomical size of the search space the synthesizer has to explore. In response to this challenge, recent work proposed to guide synthesis using learned probabilistic models. Obtaining such a model, however, might be infeasible for a problem domain where no high-quality training data is available. In this work we introduce an alternative approach to guided program synthesis: instead of training a model ahead of time we show how to bootstrap one just in time, during synthesis, by learning from partial solutions encountered along the way. To make the best use of the model, we also propose a new program enumeration algorithm we dub guided bottom-up search, which extends the efficient bottom-up search with guidance from probabilistic models. We implement this approach in a tool called PROBE, which targets problems in the popular syntax-guided synthesis (SYGuS) format. We evaluate PROBE on benchmarks from the literature and show that it achieves significant performance gains both over unguided bottom-up search and over a state-of-the-art probability-guided synthesizer, which had been trained on a corpus of existing solutions. Moreover, we show that these performance gains do not come at the cost of solution quality: programs generated by PROBE are only slightly more verbose than the shortest solutions and perform no unnecessary case-splitting.
引用
收藏
页数:29
相关论文
共 48 条
[1]  
Albarghouthi A., 2013, P COMPUT AIDED VERIF, P934
[2]   A Survey of Machine Learning for Big Code and Naturalness [J].
Allamanis, Miltiadis ;
Barr, Earl T. ;
Devanbu, Premkumar ;
Sutton, Charles .
ACM COMPUTING SURVEYS, 2018, 51 (04)
[3]  
Alpaydin E, 2014, ADAPT COMPUT MACH LE, P1
[4]  
Alur R., 2018, COMMUN ACM, V61, P84, DOI DOI 10.1145/3208071
[5]   SyGuS-Comp 2017: Results and Analysis [J].
Alur, Rajeev ;
Fisman, Dana ;
Singh, Rishabh ;
Solar-Lezama, Armando .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (260) :97-115
[6]   Scaling Enumerative Program Synthesis via Divide and Conquer [J].
Alur, Rajeev ;
Radhakrishna, Arjun ;
Udupa, Abhishek .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT I, 2017, 10205 :319-336
[7]   SyGuS-Comp 2016: Results and Analysis [J].
Alur, Rajeev ;
Fisman, Dana ;
Singh, Rishabh ;
Solar-Lezama, Armando .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (229) :178-202
[8]  
Alur R, 2013, 2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), P26
[9]  
[Anonymous], 2013, HACKERS DELIGHT
[10]  
[Anonymous], 2010, P 32 ACMIEEE INT C S, DOI DOI 10.1145/1806799.1806833