FMitF: Collaborative Research: Synergies between Program Synthesis and Neural Learning of Graph Structures

在多样化和不断增长的应用主体中的一个具有挑战性的问题涉及自动生成满足期望的功能要求的计算机程序。最近出现的两种有前途的和互补的方法来解决这个问题是程序合成和神经学习。本项目旨在协同联合收割机这两种方法，以提高程序员的生产力和软件的质量。该项目还旨在培养研究生在形式化方法和机器学习的交叉点上的能力，通过实习让本科生参与研究，并以公开课程材料和开源软件工件的形式传播研究成果。程序合成确保生成的程序在逻辑规范方面是正确的。此外，用户可以很容易地引导合成器远离一个不需要的节目，朝着一个所需的，通过改变规范。另一方面，神经学习可以处理不可能通过逻辑规范提供的用户需求-神经网络在自然语言处理，计算机视觉和机器人等领域的成功突出了这一事实。此外，神经网络的扩展性非常好，因为它们能够学习在不同程序中重复的潜在模式。该项目建立在程序合成的最新进展，通过开发新的基于学习的机制，使灵活的规范，更丰富的验证程序和可扩展的求解器。在机器学习领域，它使深度神经网络能够提供在推理丰富的结构化数据时通常需要的正确性保证。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.