A system that automatically fills in the gaps in programmers’ code becomes more powerful.
Since he was a graduate student, Armando Solar-Lezama, an associate professor in MIT’s Department of Electrical Engineering and Computer Science, has been working on a programming language called Sketch, which allows programmers to simply omit some of the computational details of their code. Sketch then automatically fills in the gaps.
If it’s fleshed out and made more user-friendly, Sketch could ultimately make life easier for software developers. But in the meantime, it’s proving its worth as the basis for other tools that exploit the mechanics of “program synthesis,” or automatic program generation. Recent projects at MIT’s Computer Science and Artificial Intelligence Laboratory that have built on Sketch include a system for automatically grading programming assignments for computer science classes, a system that converts hand-drawn diagrams into code, and a system that produces SQL database queries from code written in Java.
At this year’s Verification, Model Checking, and Abstract Interpretation Conference, Solar-Lezama and a group of his students — grad students Rohit Singh, Rishabh Singh, and Zhilei Zu, along with MIT senior Rebecca Krosnick — described a new elaboration on Sketch that, in many cases, enables it to handle complex synthesis tasks much more efficiently. The researchers tested the new version of Sketch on several existing applications, including the automated grading system. In cases where the previous version would “time out,” or take so long to reach a solution that it simply gave up, the new version was able to correct students’ code in milliseconds.
Sketch treats program synthesis as a search problem. The idea is to evaluate a huge range of possible variations on the same basic program and find one that meets criteria specified by the programmer. If the program being evaluated is too complex, the search space balloons to a prohibitively large size. In their new paper, the researchers find a way to shrink that search space.
Chain of command
“When you’re trying to synthesize a larger piece of code, you’re relying on other functions, other subparts of the code,” Rishabh Singh explains. “If it just so happens that your system only depends on certain properties of the subparts, you should be able to express that somehow in a high-level language. Once you are able to specify that only certain properties are required, then you are able to successfully synthesize the larger code.”
For instance, Singh explains, suppose that one of the subparts of the code is a routine for finding the square root of a number, and a higher-level function relies on the results of that computation. If the previous version of Sketch were trying to evaluate variations of the high-level function, for each variation, it would also have to evaluate variations of the square-root function. Since finding square roots is a complex process, that would make the search prohibitively time-consuming.