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

FMITF：协作研究：程序综合与图结构神经学习之间的协同作用

• 批准号: 1836936
• 负责人: Mayur Naik
• 金额: $ 45万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836936&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; Synergies; between

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.

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

项目成果

Generating Programmatic Referring Expressions via Program Synthesis

通过程序合成生成程序引用表达式

• 发表时间: 2020
• 期刊: International conference on machine learning
• 作者: Huang, Jiani;Smith, Calvin;Bastani, Osbert;Singh, Rishabh;Albarghouthi, Aws;Naik, Mayur
• 通讯作者: Naik, Mayur

Code2Inv: A Deep Learning Framework for Program Verification

• DOI: 10.1007/978-3-030-53291-8_9
• 发表时间: 2020-06-16
• 期刊: Computer Aided Verification
• 作者: Si X;Naik A;Dai H;Naik M;Song L
• 通讯作者: Song L

Learning Loop Invariants for Program Verification

• 发表时间: 2018
• 作者: X. Si;H. Dai;Mukund Raghothaman;M. Naik;Le Song

Learning a Meta-Solver for Syntax-Guided Program Synthesis

• 发表时间: 2018-09
• 作者: X. Si;Yuan Yang;H. Dai;M. Naik;Le Song

Scallop: From Probabilistic Deductive Databases to Scalable Differentiable Reasoning

Scallop：从概率演绎数据库到可扩展可微分推理

• 发表时间: 2021
• 期刊: Advances in Neural Information Processing Systems
• 作者: Huang, Jiani;Li, Ziyang;Chen, Binghong;Samel, Karan;Naik, Mayur;Song, Le;Si, Xujie
• 通讯作者: Si, Xujie