SHF CORE: Small: Hybrid NLP and Formal Techniques for Synthesizing Assertions and Identifying Ambiguities from English

复杂的高性能计算系统正在快速开发，但根据其规格验证这些设计变得越来越困难。规范通常是用自然语言编写的，这本身就不精确，模糊不清，而且可能不一致。虽然已经尝试使用模板和机器学习来处理自然语言规范文档，但它们不能充分处理文本中的不精确性和模糊性。该项目结合自然语言处理（NLP）和形式分析来解决这个难题。在这一领域取得进展将为利用自然语言的新设计策略打开大门。由于该项目涉及自然语言的处理和分析，因此其结果也适用于让K-12教师和学生用简单的英语理解计算概念。该项目旨在开发一个混合框架，通过结合NLP和规范文档文本的形式分析，将自然语言规范自动翻译为形式逻辑。与现有方法不同，混合模型旨在产生未能正确翻译文本（由于不精确或模糊）的原因，以便用户可以澄清原始文本。关于如何修正这种不精确、模棱两可或不一致的句子的建议也在产生中。这就需要理解句子的意图以及可能的纠正方法，使其准确和明确。具体的任务包括灵活的依赖语法，强大的语义框架解析器，严格的形式化分析，有意义的反馈生成，运行时的建议建设。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Complex, high-performance computing systems are being developed at a rapid rate, but it is becoming increasingly difficult to verify these designs against their specifications. The specifications are generally written in natural language, which are inherently imprecise, ambiguous and potentially inconsistent. Although attempts at processing natural-language specification documents have been made with templates and machine learning, they do not adequately deal with imprecision and ambiguity in the text. This project combines natural-language processing (NLP) and formal analysis to tackle this difficult problem. Making strides in in this domain will open doors to new design strategies that leverage natural language. Because this project involves the processing and analysis of natural language, the results are also applicable to engaging K-12 teachers and students in understanding computational concepts in plain English.This project aims to develop a hybrid framework for automatic translation of natural-language specifications into formal logic by combining NLP and formal analysis of the text in specification documents. Unlike existing methods, the hybrid model is intended to produce reasons for failing to properly translate the text (due to imprecision or ambiguity), so that the user can clarify the original text. Suggestions on how to fix such imprecise, ambiguous, or inconsistent sentences are also being produced. This requires the understanding of the intent of the sentence(s) and potential ways that they could be corrected to become precise and unambiguous. Specific tasks include the construction of flexible dependency grammars, robust semantic frame parsers, rigorous formal analyses, meaningful feedback generation, and run-time suggestions. The coherent set of tasks is offering insight on best strategies for synergizing NLP and formal analyses.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.