System that automatically fills the gaps in programmers' code improved

February 25, 2014 by Larry Hardesty
Credit: Christine Daniloff/MIT

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 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.

With the new version of Sketch, however, the programmer can simply specify conditions that the square-root function has to meet: The output multiplied by itself must equal the input. Now, Sketch can satisfy itself that the square-root function it comes up with meets that criterion and move on to the higher-level function. It doesn't need to re-evaluate the square-root function at every pass.

In fact, this places a slightly greater onus on the programmer, who now has to reason about the criteria that each low-level function must meet. But it allows Sketch to handle much more complicated problems.

Immediate prospects

Solar-Lezama concedes that it will take a good deal of work before Sketch is useful to commercial . "The application as a tool-building infrastructure, using it to build higher-level systems on top of it, we've demonstrated very convincingly by building a variety of systems that do things that couldn't be done before," he says.

He has, however, conducted usability studies with Sketch, recruiting MIT undergraduates with only a semester's worth of programming experience to test it. In all cases, he says, the students successfully used Sketch to produce working code. But in many cases, the missing code took an unacceptably long time to synthesize, because of the way the students had described the problem.

"It still requires a level of expertise and understanding about the underlying technology in order for it not to blow up," Solar-Lezama says. "As far as the more ambitious goal of everybody dumping C and using Sketch instead, we'd still have to push quite a bit."

As Rajeev Alur, a professor in the Department of Computer and Information Science at the University of Pennsylvania, explains, the new paper draws on principles from the field of "formal verification," which, Alur says, investigates methods for "checking the correctness of programs using automated reasoning."

"In verification, people have always used modular reasoning as a technique to make it scale to more interesting systems," Alur says. "What this paper does is take some of those ideas and meshes them nicely with the synthesis routines they have in Sketch."

Alur acknowledges that "having a general software developer use [Sketch], maybe that's not realistic in the foreseeable time." But, he says, "even now it could be used in very specific, specialized tasks. If you're trying to optimize some piece of code for some reason, instead of doing all that fine-tuning of the manually, now a system like Sketch could do it."

Explore further: How to program unreliable chips

Related Stories

How to program unreliable chips

November 4, 2013

As transistors get smaller, they also become less reliable. So far, computer-chip designers have been able to work around that problem, but in the future, it could mean that computers stop improving at the rate we've come ...

Dude, where's my code?

October 16, 2013

Compilers are computer programs that translate high-level instructions written in human-readable languages like Java or C into low-level instructions that machines can execute. Most compilers also streamline the code they ...

An oracle for object-oriented programmers

October 7, 2011

In the last 40 years, the major innovation in software engineering has been the development of what are called object-oriented programming languages. “Objects” are, effectively, repositories for the computational ...

Computer program can identify sketches

September 13, 2012

(—Computers are good at speed, numbers, and massive amounts of data, but understanding the content of a simple drawing is more difficult. Researchers at Brown and the Technical University of Berlin have produced ...

Method developed to match police sketch, mug shot

March 3, 2011

( -- The long-time practice of using police facial sketches to nab criminals has been, at best, an inexact art. But the process may soon be a little more exact thanks to the work of some Michigan State University ...

Recommended for you

Enhancing solar power with diatoms

October 20, 2017

Diatoms, a kind of algae that reproduces prodigiously, have been called "the jewels of the sea" for their ability to manipulate light. Now, researchers hope to harness that property to boost solar technology.


Adjust slider to filter visible comments by rank

Display comments: newest first

1 / 5 (2) Feb 25, 2014
I don't know but I feel that this may just lead to true "Artificial Intelligence".
1 / 5 (1) Feb 25, 2014
Ah well indeed bearly can say but, might there be just as much potential for the passably intelligent humans patterned with bureaucratic & officious systems, of their own making, wishing to get an easier ride attempting to simplify intellectually taut programming tasks & thus produce "Artificial Stupidity".

ie. When all is said & done & those systems must work together with inestimable & unfathomable combinatorial complexity humans have enough trouble dealing with already (& thats with other humans & not ostensibly) between AI/AS systems whizzing their garbage in/garbage out protocols on a much larger scale & by then, us far from the loop so to speak are completely clueless & way too comfortable theorists to attempt to diagnose a systemic demise.

No, we will not go out with a bang, we'll likely go out with a whimper, a grand scale form of digital Alzheimer's if we allow AI/AS to get too much of a foothold & allow it control our primal motives;

Food, Shelter & Sex.

Where's my phone?
3 / 5 (2) Feb 27, 2014
Here is a test program:

Step 1: Collect underpants
Step 2:
Step 3: Profit!

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more

Click here to reset your password.
Sign in to get notified via email when new comments are made.