Toward More Accessible and Trustworthy Program Synthesis
- 講者Xiaokang Qiu 教授 (美國普渡大學)
邀請人：王柏堯 - 時間2023-11-24 (Fri.) 10:30 ~ 12:00
- 地點資訊所新館106演講廳 , Auditorium 106 at IIS new Building
摘要
Program synthesis is the process of automatically generating programs that meet the user’s intent. In the last two decades, this traditional research area has experienced a renaissance and witnessed emerging programming paradigms, automated tools, and prominent applications. However, the promising progress also exposes a tension between making program synthesis more user-friendly and guaranteeing the quality of the produced code.
In this talk, I will discuss two projects from our work on pushing further toward more accessible and trustworthy program synthesis. First, I will present Comparative Synthesis, an interactive synthesis framework that learns near-optimal programs through comparative queries, without explicitly specified optimization objectives. We develop a voting-guided learning algorithm which provides a provable guarantee on the quality of the found program. We have implemented this approach in a system Net10Q for wide-area network design. Experiments with oracles and a pilot user study with network practitioners and researchers show Net10Q is effective in finding allocations that meet diverse user policy goals in an interactive fashion. Second, I will present a new synthesis algorithm for bit vectors which has been integrated into DryadSynth, our competition-winning SyGuS solver. The algorithm is driven by a new term-graph-based enumeration and enhanced by large language models (LLMs) and a novel bottom-up deduction technique. The algorithm outperformed existing algorithms (including CVC4, Duet and Simba) in terms of the number of solved problems, execution time, and solution size, and successfully solved many difficult benchmarks for the first time, including 5 renowned Hacker’s Delight benchmarks.
In this talk, I will discuss two projects from our work on pushing further toward more accessible and trustworthy program synthesis. First, I will present Comparative Synthesis, an interactive synthesis framework that learns near-optimal programs through comparative queries, without explicitly specified optimization objectives. We develop a voting-guided learning algorithm which provides a provable guarantee on the quality of the found program. We have implemented this approach in a system Net10Q for wide-area network design. Experiments with oracles and a pilot user study with network practitioners and researchers show Net10Q is effective in finding allocations that meet diverse user policy goals in an interactive fashion. Second, I will present a new synthesis algorithm for bit vectors which has been integrated into DryadSynth, our competition-winning SyGuS solver. The algorithm is driven by a new term-graph-based enumeration and enhanced by large language models (LLMs) and a novel bottom-up deduction technique. The algorithm outperformed existing algorithms (including CVC4, Duet and Simba) in terms of the number of solved problems, execution time, and solution size, and successfully solved many difficult benchmarks for the first time, including 5 renowned Hacker’s Delight benchmarks.
BIO
Xiaokang Qiu is an Associate Professor with the Elmore Family School of Electrical and Computer Engineering at Purdue University. He finished his Ph.D. in Computer Science at the University of Illinois at Urbana-Champaign in 2013. Before starting at Purdue in 2016, he was a postdoctoral associate at the Massachusetts Institute of Technology. His current research interests lie in the algorithmic aspects of software verification and synthesis, and their applications. He is a member of the Purdue Center for Programming Principles and Software Systems (PurPL) and leads the Computer-Aided Programming (CAP) group at Purdue. He received a Seed for Success award from Purdue University (2020), an NSF CAREER award (2021) and an U.S. Air Force summer faculty fellowship (2022). He is a senior member of ACM and IEEE.