A challenging problem in a diverse and growing body of applications concerns automatically generating computer programs that satisfy desired functional requirements. Two promising and complementary approaches that have recently emerged to address this problem are program synthesis and neural learning. This project aims to synergistically combine the two approaches to improve the productivity of programmers and the quality of software. The project also aims to train graduate students at the intersection of formal methods and machine learning, engage undergraduate students in research through internships, and disseminate results in the form of publicly available course materials and open-source software artifacts.
Program synthesis ensures that the generated program is correct with respect to a logical specification. Moreover, users can easily guide the synthesizer away from an undesired program and towards a desired one, by changing the specification. On the other hand, neural learning can handle user requirements that are impossible to provide via a logical specification -- a fact highlighted by the success of neural networks in domains such as natural language processing, computer vision, and robotics. Moreover, neural networks scale extremely well, by virtue of their ability to learn latent patterns that repeat across different programs. This project builds upon recent progress in program synthesis by developing novel learning-based mechanisms that enable flexible specifications, richer verifiers, and scalable solvers. In the realm of machine learning, it enables deep neural networks to provide correctness guarantees that are typically required when reasoning about rich structured data. In doing so, it develops novel architectures and methodologies for representation learning, reinforcement learning, and learning with limited data.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
