Collaborative Research: SHF: Medium: Semantics-Aware Neural Models of Code

在大量代码上训练的大型神经模型仍然经常产生质量差的代码，包括未初始化的变量，类型不正确的表达式和永远不会完成的循环等基本错误。 这些错误可能是潜在的软件漏洞的来源。 这些问题的根本原因是模型在训练和生成过程中将程序视为语法而不是语义工件。 该项目的新奇在于将这种模型与形式方法社区开发的符号化、语义感知的程序合成方法相结合。 该项目开发了一个神经符号程序合成框架，将深度学习和经典符号方法紧密结合起来进行程序合成。 该研究探索了新的学习算法，其中代码的神经模型（特别是变压器）暴露于有关程序语义的明确知识，使用变压器来指导规范指导合成器的机制，以及经典合成和学习模型的组合来构建神经生成程序的新组合。该项目的影响是语义感知程序合成的统一框架，产生更好的自动创建程序的工具。该项目开发了一个跨机构的本科生研究经验（REU）计划，特别注重招募女性，西班牙裔和黑人学生参加。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

Large neural models trained on massive amounts of code still often produce code of poor quality, with such elementary errors as uninitialized variables, type-incorrect expressions, and loops that never finish. Such errors can be a source of insidious software vulnerabilities. The root cause of these issues is that the models treat programs as syntactic rather than semantic artifacts, both during training and generation. The project's novelty is to couple such models with symbolic, semantics-aware methods for program synthesis developed in the formal-methods community. The project develops a neurosymbolic program-synthesis framework that closely couples deep learning and classical symbolic methods for program synthesis. The research explores new learning algorithms in which neural models of code (specifically, transformers) are exposed to explicit knowledge about program semantics, mechanisms that use transformers to direct specification-directed synthesizers, and combinations of classical synthesis and learned models to construct novel compositions of neurally generated programs. The project's impact are a unified framework for semantics-aware program synthesis, yielding better tools for automatically creating programs. The project develops a cross-institution Research Experiences for Undergraduates (REU) program, with a special focus on recruiting women, Hispanic, and Black students to participate.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.