Armando Solar-Lezama

The Reality & Potential of Program Synthesis with Professor Armando Solar-Lezama

Written By: Audrey Woods

The idea of automating software development has tantalized researchers all the way back to the days of Alan Turing. In 1945, Turing argued that in the future, “any processes that are quite mechanical may be turned over to the machine itself.” It’s easy to imagine why this idea might be enticing, especially with the current buzz around AI-generative programs like DALL-E and ChatGPT. Imagine being able to ask a computer to, say, create a new word processor or code an app. Suddenly anyone with an idea could be an expert programmer. 

Realistically, CSAIL Professor Armando Solar-Lezama says we have a long way to go before we reach that level of automation. In his conversation with CSAIL Alliances, Professor Solar-Lezama says, “today we can do a really good job automating [on a small] level of programming,” like manipulating data or moving files around. “However, once we talk about programming in the large—developing computer systems and really writing applications that people will use—we're talking about a very different set of concerns.” He explains how creating programs that have multiple interfaces and integrated systems “is something that we’re not close to automating.” Professor Solar-Lezama elaborates that there are “a lot of tasks that professional programmers do in their day-to-day work that are hard to automate because they require navigating very different levels of abstraction [and] a lot of creativity,” something AI is not yet capable of.  

But as the head of the Computer Assisted Programming group, Professor Solar-Lezama is bringing that level of automation closer every day. 

Programming Squared: Finding His Interest 

When asked what first drew him to the computer science field, Professor Solar-Lezama says that fundamentally, “I really like programming. It’s something I do for fun, even when I don’t have to.” Dating back to elementary school, he was always deeply interested in STEM, going above and beyond in his school’s technical projects to the point that teachers would fail him for writing code that was too complex for the assignment. He says of that period in his life, “I was doing my own thing. As long as school didn’t take up too much of my time, it was fine.” 

Little did Professor Solar-Lezama know that he was destined for a life in academia. After earning a bachelor’s in computer science from Texas A&M—finishing his degree in three years—he went to UC Berkeley to continue his work on large parallel computing systems. Soon after beginning, though, he was drawn into larger questions about the coding and programming process, specifically if there was a way to automate some of the low-level decisions that went into design strategy. These questions inspired Sketch, his graduate thesis project and the foundation of his future research. 

Sketch & Other Methods 

Sketch, according to Professor Solar-Lezama, approaches program synthesis as a search problem, where programmers can “leave holes in places where they already know that a complicated piece of code needs to be, but they don’t know exactly the details of what that code should look like.” Sketch allows users to leave a placeholder while writing that the synthesizer will then fill in based on local pieces of code. Professor Solar-Lezama explains how the idea was to “get some automation that is helpful for programmers, but that lets the programmers do the things they know how to do well.” This gives programmers full control over their code and satisfies correctness guarantees while speeding up the process of writing large programs. 

At the time, Sketch was groundbreaking because, as Professor Solar-Lezama describes, “before we started this project there was very little attention paid to program synthesis, even in the research community.” He says there was even “hostility toward these kinds of ideas,” explaining how at the time “people thought of program synthesis [as] this unobtainable goal of generating everything from scratch.” But with Sketch, Professor Solar-Lezama and fellow researchers showed that program synthesis didn’t need to be all-or-nothing. Of the program, he says, “it proved very useful as an internal engine for higher-level tools that could do useful things for you. For example: places where you know that you’re going to be solving very similar synthesis problems over and over again.” 

Nowadays, Professor Solar-Lezama is also working on neurosymbolic programing, which combines the benefits of deep learning with the interpretability of program synthesis. He says that deep learning has been “game changing” in program synthesis, allowing them to “bridge the gap between the formal world where programs live, where everything has to be super precise and spelled out in full detail, and the informal world of natural language and whiteboard diagrams.” Combining these two research areas has allowed them to access “much richer forms of interaction with the program synthesizer,” although it’s a challenging combination. Software, by nature, is verifiable, concrete, and has “a lot less tolerance for noise and errors,” whereas something like natural language is nuanced and more imprecise. “One of the things that we’re really interested in,” Professor Solar-Lezama says, “is how do we get programming systems that can bridge these different modes of reasoning.” 

Generally, he describes how the domains best suited for program synthesis—at least currently—are those “where you can do very useful things with relatively small programs and where there are natural or well-established ways of conveying what it is that you want the program to do.” He uses the example of data processing, which can be done with “dozens of lines of code, not thousands or tens of thousands.” Also, data management is often done by non-computer scientists, who will no doubt appreciate a little help writing code.  

Going Forward 

Professor Solar-Lezama sees his work as more than cutting costs and speeding up the development of programs, although those are important aspects. To him, “code is such a powerful and expressive mechanism for describing the world and how things work” and offers “a tool for reasoning that is very different from other mechanisms out there.” Many of today’s scientific theories are expressed in code or as simulations, which means his work could have an impact well beyond software development. Program synthesis could become a powerful tool to generate models of the world that are consistent with data and observations but that also capture existing knowledge and can help scientists gain a better understanding of the world. In this way, programs become “these very expressive knowledge representations” that Professor Solar-Lezama finds exciting. 

One message Professor Solar-Lezama wants to send audiences is that, even though we are beginning to automate aspects of the coding process, it’s still critically important to be educating the next generation of developers and programmers. He says he is “trying to push back on some of what we’re hearing today about how people don’t need to learn about computer programming because machines are going to be able to do it.” For the foreseeable future, he sees program synthesis as complimentary to the job of software developers and human creativity. He says, “when we started working in this field, the goal was to develop technologies that could help people,” and that aspiration continues to this day.