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

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

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.