MIT Research News' Journal
[Most Recent Entries]
[Calendar View]
Tuesday, February 25th, 2014
| Time |
Event |
| 5:00a |
Self-completing programs
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.
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 software developers. “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 code manually, now a system like Sketch could do it.” | | 5:00a |
How to create selective holes in graphene
Researchers have devised a way of making tiny holes of controllable size in sheets of graphene, a development that could lead to ultrathin filters for improved desalination or water purification.
The team of researchers at MIT, Oak Ridge National Laboratory, and in Saudi Arabia succeeded in creating subnanoscale pores in a sheet of the one-atom-thick material, which is one of the strongest materials known. Their findings are published in the journal Nano Letters.
The concept of using graphene, perforated by nanoscale pores, as a filter in desalination has been proposed and analyzed by other MIT researchers. The new work, led by graduate student Sean O’Hern and associate professor of mechanical engineering Rohit Karnik, is the first step toward actual production of such a graphene filter.
Making these minuscule holes in graphene — a hexagonal array of carbon atoms, like atomic-scale chicken wire — occurs in a two-stage process. First, the graphene is bombarded with gallium ions, which disrupt the carbon bonds. Then, the graphene is etched with an oxidizing solution that reacts strongly with the disrupted bonds — producing a hole at each spot where the gallium ions struck. By controlling how long the graphene sheet is left in the oxidizing solution, the MIT researchers can control the average size of the pores.
A big limitation in existing nanofiltration and reverse-osmosis desalination plants, which use filters to separate salt from seawater, is their low permeability: Water flows very slowly through them. The graphene filters, being much thinner, yet very strong, can sustain a much higher flow. “We’ve developed the first membrane that consists of a high density of subnanometer-scale pores in an atomically thin, single sheet of graphene,” O’Hern says.
For efficient desalination, a membrane must demonstrate “a high rejection rate of salt, yet a high flow rate of water,” he adds. One way of doing that is decreasing the membrane’s thickness, but this quickly renders conventional polymer-based membranes too weak to sustain the water pressure, or too ineffective at rejecting salt, he explains.
With graphene membranes, it becomes simply a matter of controlling the size of the pores, making them “larger than water molecules, but smaller than everything else,” O’Hern says — whether salt, impurities, or particular kinds of biochemical molecules.
The permeability of such graphene filters, according to computer simulations, could be 50 times greater than that of conventional membranes, as demonstrated earlier by a team of MIT researchers led by graduate student David Cohen-Tanugi of the Department of Materials Science and Engineering. But producing such filters with controlled pore sizes has remained a challenge. The new work, O’Hern says, demonstrates a method for actually producing such material with dense concentrations of nanometer-scale holes over large areas.
“We bombard the graphene with gallium ions at high energy,” O’Hern says. “That creates defects in the graphene structure, and these defects are more chemically reactive.” When the material is bathed in a reactive oxidant solution, the oxidant “preferentially attacks the defects,” and etches away many holes of roughly similar size. O’Hern and his co-authors were able to produce a membrane with 5 trillion pores per square centimeter, well suited to use for filtration. “To better understand how small and dense these graphene pores are, if our graphene membrane were to be magnified about a million times, the pores would be less than 1 millimeter in size, spaced about 4 millimeters apart, and span over 38 square miles, an area roughly half the size of Boston,” O’Hern says.
With this technique, the researchers were able to control the filtration properties of a single, centimeter-sized sheet of graphene: Without etching, no salt flowed through the defects formed by gallium ions. With just a little etching, the membranes started allowing positive salt ions to flow through. With further etching, the membranes allowed both positive and negative salt ions to flow through, but blocked the flow of larger organic molecules. With even more etching, the pores were large enough to allow everything to go through.
Scaling up the process to produce useful sheets of the permeable graphene, while maintaining control over the pore sizes, will require further research, O’Hern says.
Karnik says that such membranes, depending on their pore size, could find various applications. Desalination and nanofiltration may be the most demanding, since the membranes required for these plants would be very large. But for other purposes, such as selective filtration of molecules — for example, removal of unreacted reagents from DNA — even the very small filters produced so far might be useful.
“For biofiltration, size or cost are not as critical,” Karnik says. “For those applications, the current scale is suitable.”
Bruce Hinds, a professor of materials engineering at the University of Kentucky who was not involved in this work, says, “Previous groups had tried just ion bombardment or plasma radical formation.” The idea of combining these methods “is nice and has the potential to be fine-tuned.” While more work needs to be done to refine the technique, he says, this approach is “promising” and could ultimately help to lead to applications in “water purification, energy storage, energy production, [and] pharmaceutical production.”
The work also included Jing Kong, the ITT Career Development Associate Professor of Electrical Engineering; MIT graduate students Michael Boutilier and Yi Song; researcher Juan-Carlos Idrobo of the Oak Ridge National Laboratory; and professors Tahar Laoui and Muataz Atieh of the King Fahd University of Petroleum and Minerals (KFUPM). The project received support from the Center for Clean Water and Clean Energy at MIT and KFUPM and the U.S. Department of Energy.
| | 2:30p |
Can entrenched energy systems undergo rapid changes?
The world’s energy infrastructure — with its massive generating plants, mines, refineries, electric grids, and gas stations — is often likened to an aircraft carrier: Trying to change its direction is a slow and difficult process. But at times, such changes can take place with surprising rapidity, as some speakers pointed out at this year’s MIT Energy Conference.
One stunning recent example, author Daniel Yergin said, has been the change in the natural gas industry with the twin technologies of horizontal drilling and hydraulic fracturing (commonly known as “fracking”). Just a few years ago, he pointed out, the assumption was that the United States was running out of natural gas and would need to begin importing the fuel. Now, instead, there are sufficient reserves not only to meet the nation’s own demands, but likely enough to begin significant exports.
Similarly, Yergin pointed out, new technologies for the extraction of shale oil have vastly increased estimates of U.S. oil reserves — so much so that the country could ultimately become a leading exporter of oil as well. New technologies in other areas of energy, he added, could trigger similarly unexpected changes in energy supplies and usage.
Yergin, the author of “The Quest: Energy, Security and the Remaking of the Modern World,” says that while many people think of climate change as the principal driver of changing energy use, that it is only one of several pressures that point in the same overall direction, including security, jobs, and economic growth. For example, he said, the availability of cheap natural gas has already begun to have a dramatic impact on the competitiveness of U.S. manufacturing.
However, this newfound abundance of natural gas could be both a blessing and a curse, as several speakers at the conference pointed out. Maria van der Hoeven, executive director of the International Energy Agency, said that while natural gas produces fewer greenhouse gas emissions than coal, it is still a contributor to global climate change.
“Let me be clear,” she said. “An expansion of gas alone is no panacea for climate change. Natural gas may be the cleanest fossil fuel, but it is still a fossil fuel.” Abundant cheap gas could actually undermine efforts to develop carbon-free energy sources, she said, prompting “a need for policies to defend truly low-carbon energy sources from the economic pressures of gas. These policies could take the form of a realistic price on carbon, for example, or — in the absence of such a carbon price — a policy mandate and strong public support of research, development, and deployment to foster technologies that can compete on their own.”
Despite the downsides of cheap gas, van der Hoeven finds encouragement in the recent expansion of renewable energy sources. “The current rapid growth of renewable power is a bright spot in the otherwise-bleak picture of global progress toward a cleaner and more diversified energy mix,” she said. Her agency’s projections show a 40 percent increase in renewable electricity production worldwide over the next five years, she said.
That growth would bring renewables up to one-quarter of global electricity generation. Perhaps more significantly, it would mean that by 2016, renewables would surpass gas and reach twice the level of nuclear power in total generating capacity, van der Hoeven said — making renewables second only to coal.
One key to further growth of renewables, she added, is improved storage systems to help compensate for the intermittent nature of many renewable energy sources. Indeed, other speakers described several new technologies for energy storage — some of which could help in the proliferation of intermittent and distributed energy sources.
Donald Sadoway, the John F. Elliott Professor of Materials Chemistry at MIT, described his group’s development of a new kind of battery designed to be cheap, reliable, and easily scalable. The key to this work, he explained, was starting from scratch, rethinking every aspect of battery design and using abundant materials. “If you want it to be dirt cheap,” he said, “you’ve got to make it out of dirt — and preferably local dirt.” His battery design, which led to a company that has already raised $11 million in funding, uses metals that are abundant around the world, he said.
Other examples were presented by Alexander Slocum, the Neil and Jane Pappalardo Professor of Mechanical Engineering at MIT, who described huge concrete tanks as a means of mooring offshore windmills; these would use excess wind power to pump water out of the tanks, letting the water flow back into them and turn a turbine to provide power when it’s needed. Another system would use a large cauldron of molten salt to collect solar heat, which could then be used to heat water and generate power as needed.
But as promising as these technologies may be, their widespread implementation remains years away, van der Hoeven suggested. While such storage systems might be competitive today in some places, battery costs need to come down considerably to be competitive in most situations, she said. And today, she pointed out, fossil fuels still account for 82 percent of global energy — a figure that hasn’t changed in two decades.
The MIT Energy Conference was started in 2005 by MIT’s student-led Energy Club; it has remained a student-run conference ever since, and has become recognized as a leading showcase of energy technology and policy research. |
|