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

Virginia Polytechnic Institute And State University, Blacksburg VA

Investigators

Abstract

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.