Program Synthesis with Best-First Bottom-Up Search

被引:0
作者
Ameen, Saqib [1 ]
Lelis, Levi H. S. [1 ]
机构
[1] Univ Alberta, Alberta Machine Intelligence Inst Amii, Dept Comp Sci, Edmonton, AB, Canada
基金
加拿大自然科学与工程研究理事会;
关键词
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Cost-guided bottom-up search (BUS) algorithms use a cost function to guide the search to solve program synthesis tasks. In this paper, we show that current state-of-the-art cost -guided BUS algorithms suffer from a common problem: they can lose useful information given by the model and fail to perform the search in a best-first order according to a cost function. We introduce a novel best-first bottom-up search algorithm, which we call BEE SEARCH, that does not suffer information loss and is able to perform cost-guided bottom-up synthesis in a best-first manner. Importantly, BEE SEARCH performs best-first search with respect to the generation of programs, i.e., it does not even create in memory programs that are more expensive than the solution program. It attains best-first ordering with respect to generation by performing a search in an abstract space of program costs. We also introduce a new cost function that better uses the information provided by an existing cost model. Empirical results on string manipulation and bit-vector tasks show that BEE SEARCH can outperform existing cost-guided BUS approaches when employing more complex domain-specific languages (DSLs); BEE SEARCH and previous approaches perform equally well with simpler DSLs. Furthermore, our new cost function with BEE SEARCH outperforms previous cost functions on string manipulation tasks.
引用
收藏
页码:1275 / 1310
页数:36
相关论文
共 50 条
[1]  
Albarghouthi Aws, 2013, Computer Aided Verification. 25th International Conference, CAV 2013. Proceedings. LNCS 8044, P934, DOI 10.1007/978-3-642-39799-8_67
[2]   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
[3]   Syntax-Guided Synthesis [J].
Alur, Rajeev ;
Bodik, Rastislav ;
Dallal, Eric ;
Fisman, Dana ;
Garg, Pranav ;
Juniwal, Garvit ;
Kress-Gazit, Hadas ;
Madhusudan, P. ;
Martin, Milo M. K. ;
Raghothaman, Mukund ;
Saha, Shamwaditya ;
Seshia, Sanjit A. ;
Singh, Rishabh ;
Solar-Lezama, Armando ;
Torlak, Emina ;
Udupa, Abhishek .
DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2015, 40 :1-25
[4]   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
[5]  
Balog M, 2017, Arxiv, DOI arXiv:1611.01989
[6]   Just-in-Time Learning for Bottom-Up Enumerative Synthesis [J].
Barke, Shraddha ;
Peleg, Hila ;
Polikarpova, Nadia .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (OOPSLA)
[7]  
Bastani O, 2018, ADV NEUR IN, V31
[8]  
Bunel R., 2018, INT C LEARNING REPRE
[9]  
Chen Xuxi, 2020, INT C LEARNING REPRE
[10]  
Colon M. A., 2004, Logic Based Program Synthesis and Transformation. 14th Intenational Symposium, LOPSTR 2004. Revised Selected Papers (Lecture Notes in Computer Science Vol. 3573), P166