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 deﬁne 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.