From smart home appliances to business processes, automation is changing our lives for the better, freeing up our time and resources to dedicate to higher level tasks. The same should be true for computer programming — the growing availability of computing power allows computer scientists to automate the more tedious and difficult aspects of programming.

Professor Armando Solar-Lezama, who is an Associate Director and the COO of MIT CSAIL and leads the Computer-Aided Programming Group, aims to reduce the skill and effort required to develop software that is secure, reliable, and efficient. One of his research group’s central contributions to this goal is the development of new approaches to software synthesis that can combine information from different sources to produce the code that the programmer wants. The group’s research ranges from the design of new analysis techniques and automated reasoning mechanisms to the development of new programming models that automate challenging aspects of programming.

Prof. Solar-Lezama is most interested in software synthesis and its applications to particular program domains such as high-performance computing. He first found this niche area of program synthesis as a graduate student at Berkeley, for which his thesis project, a language called Sketch, treats program synthesis as a search problem in which the algorithms pare down the search space to make the search faster and more efficient. Since then, program synthesis research has greatly expanded into the active field it is today.

More recently, his group has been exploring the use of program synthesis beyond software development applications, leveraging techniques from program synthesis for domains ranging from Computer Aided Design to Linguistics. The idea is to take what would traditionally be considered machine learning problems and frame them as program synthesis problems, where the goal is to generate a program that explains the observed data. The approach works particularly well in domains where data is scarce or expensive to collect and where interpretability is important.

His group has also been exploring the combination of logical reasoning and deep learning-based techniques into a new approach of neurosymbolic program learning. This research direction arose from a need to leverage the benefits of deep learning for program synthesis tasks while maintaining the ability to reason precisely about the behavior of the synthesized programs. This paradigm has given rise to a number of new techniques for a variety of tasks ranging from program development to control problems.

For example, in a recent paper, his group used neurosymbolic techniques to learn interpretable policies for multi-agent systems. If you have a swarm of drones, for example, and you want them to work together or avoid each other, traditional planning can be hard to scale. Recently, people have observed that reinforcement learning can help with these positioning and coordinating tasks. Prof. Solar-Lezama was able to use this neurosymbolic reasoning approach to extract a policy from the neural network that is defined in a higher-level interpretable language, so that the drones’ tasks could be completed more efficiently with minimal communication — both individual messages each individual agent is sending, as well as how many messages each individual agent has to pay attention to.

Prof. Solar-Lezama and the Computer-Aided Programming Group are continuing to push the development of these neurosymbolic technologies, focusing on scientific discovery. This promising application of program synthesis for machine learning has the benefit of improved interpretability, which can help researchers understand natural phenomena.

For example, as part of this work, his current research in RNA splicing involves training a deep learning model to accurately predict how a piece of RNA is going to be processed, end-to-end. While such a model is not particularly useful in that it doesn’t tell you how that process actually works, the ability to generate models you can probe and match against what is known in scientific literature about that process means that you can move from simply making a prediction to truly understanding how a process works.

Overall, Prof. Solar-Lezama believes that the future of programming will involve significantly higher levels of automation. His goal is to transform software synthesis, contributing to a future where a combination of automated logical reasoning and machine learning help make programmers more productive in delivering efficient and reliable software.