SHF: Medium: Compositional Semantics-Guided Synthesis

SHF：媒介：组合语义引导合成

• 批准号: 2211968
• 负责人: Loris DAntoni
• 金额: $ 90万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2211968&HistoricalAwards=false
• 关键词: SHF; Medium; Compositional; Semantics; Guided

The field of program synthesis aims to create tools that can automatically create a program from a specification of desired behavior. Synthesis holds the promise of easing the burden on programmers (e.g., by finding solutions to tricky special cases automatically), and allowing non-programmers to create programs merely by indicating the outcome that they want the program to produce. Unfortunately, current synthesis tools do not scale up to large-scale programming problems, a situation that threatens to doom this promising technology to being a niche field. This project's novelties are ways to exploit compositionality in program synthesis in a way that allows one to create bigger programs out of smaller ones.The project builds on a recent framework called SemGuS (Semantics-Guided Synthesis), which offers a foothold on the expressibility and scalability problems of program synthesis. In principle, the framework can support the synthesis of software in layers, where implementation choices in one layer are hidden from other layers (and thus consistent with modular software design with information hiding). The goal of the project is to capitalize on the opportunity that SemGuS offers for extending synthesis to much larger systems than was possible heretofore. The work will lead to more scalable and general synthesis algorithms, with potential benefits to synthesis applications that are already in widespread use. Further development of the SemGuS framework has the potential to make synthesis more usable and programmable, and thereby allow users to carry out synthesis tasks without prior knowledge of existing synthesis tools. Most importantly, compositional synthesis will allow synthesis to scale to larger applications with more practical relevance.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.

程序综合领域的目标是创建可以根据所需行为规范自动创建程序的工具。综合有望减轻程序员的负担（例如，通过自动找到棘手的特殊情况的解决方案），并允许非程序员仅通过指示他们希望程序产生的结果来创建程序。不幸的是，当前的综合工具无法扩展到大规模编程问题，这种情况有可能使这项有前途的技术成为一个小众领域。该项目的新颖之处在于利用程序综合中的组合性，从而允许人们用较小的程序创建更大的程序。该项目建立在一个名为 SemGuS（语义引导综合）的最新框架之上，该框架在可表达性和可表达性方面提供了立足点。程序综合的可扩展性问题。原则上，该框架可以支持分层软件的综合，其中一层中的实现选择对其他层隐藏（因此与具有信息隐藏的模块化软件设计一致）。该项目的目标是利用 SemGuS 提供的机会将合成扩展到比以前更大的系统。这项工作将带来更具可扩展性和通用性的合成算法，对已经广泛使用的合成应用程序具有潜在的好处。 SemGuS 框架的进一步开发有可能使综合更加可用和可编程，从而允许用户在不事先了解现有综合工具的情况下执行综合任务。最重要的是，组合合成将允许合成扩展到具有更实际相关性的更大应用。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。