Synthesizing Neurosymbolic Programs

/by

In a previous post, I talked about the potential of program synthesis as an approach to discovering truths about the natural world. As it happens, a team that Armando Solar-Lezama leads and that I am a part of recently won a US NSF Expeditions in Computing grant to work on this topic. The Expeditions program aims to fund “ambitious, fundamental research agendas that promise to define the future of computing and information.” The program has played an important role in PL research. The ExCAPE expedition enabled major progress in program synthesis: the problem of automatically discovering programs from specifications. The ongoing DeepSpec expedition is making the dream of formally verified software ever closer to reality. I am optimistic that our expedition will continue this tradition and produce results that are deeply grounded in PL while also being of fundamental interest to science and the broader society.

My last post primarily focused on the application dimension of the project. In this post, I will talk about the central technical idea that we aim to pursue: the data- and specification-driven synthesis of neurosymbolic programs, or programs in which traditional code is melded together with neural modules.

Read more

Understanding the World with Program Synthesis

/by

Most PL research is concerned with the engineering of software. Programs, in the narrative driving this work, are human-built artifacts. The PL research challenge is to make sure that they can be engineered, with as little effort as possible, to be reliable and have high performance.

But programming languages can also be used for modeling natural phenomena. This is the central goal in the discipline of computational science, which develops tools for programmatically modeling real-world processes ranging from nuclear reactions to climate change to protein synthesis.

PL research has always played a critical role in computational science. It is impossible to simulate complex natural processes without high-performance computing (HPC), and advances in HPC are often, really, advances in compilers and runtime systems.

However, a new, intriguing path for PL ideas to shape our understanding of the natural world has opened up in the recent past. This path concerns not just the representation of the natural world as programs, but also the automatic, data-driven discovery of these programs through program synthesis.

Read more

AI Safety as a PL Problem

/by

In the last few years, there have been many anxious ruminations about AI safety. To a significant extent, these fears come from the realization that modern AI systems can be alarmingly brittle. For example, a deep neural net used for image classification can produce different outputs on inputs that are indistinguishable to humans. Machine learning algorithms can reflect harmful biases in their training data. Robots trained in controlled settings routinely fail in the real world.

Fortunately, AI systems are ultimately software, and therefore PL researchers can play a key role in making them more reliable. An emerging body of research uses PL ideas — such as high-level language abstractions and automated reasoning about correctness — to aid the design of robust and accountable AI systems. In this post, I will give a taste of some recent work on this topic.

My focus here is on sequential decision-making problems, which naturally arise in safety-critical domains like autonomous cyber-physical systems. Here, we have an AI agent that is interacting with its environment using a learned policy: a function from environment states to agent actions. A popular approach to discovering policies is >reinforcement learning (RL), in which the agent explores the environment strategically, receiving rewards for various actions, and seeks to learn a policy that maximizes the expected reward over a long time horizon. In contemporary work, it is common to represent policies using deep neural networks. Because neural nets are differentiable in their parameters, this representation allows the use of scalable, gradient-based learning techniques.

Read more