SHF:Small:Closing the Specification Gap with Logic and Linguistics

近年来，在利用软件行为的正式或半正式规范来发现软件错误或建立对软件正确性的信心的能力方面取得了巨大的进步。然而，这些规范通常以逻辑公式（用于正式验证）或附加代码（用于典型的软件测试）的形式给出，而预期行为的原始描述通常是用自然语言（如英语散文）编写的。目前，这些（半）正式规范是从自然语言手动翻译过来的，在翻译过程中留下了误解或错误的重大机会，这可能导致验证软件满足无用或不正确的属性。翻译的手工性质意味着很难事后审核。这个项目追求新的方法来连接软件行为的自然语言规范，在单句的层次上，到目前被许多软件质量工具所接受的（半）正式规范，包括基于属性的测试框架，证明助手，以及使用时态逻辑规范的各种工具。该项目的新颖之处在于使用语言学文献中提取的技术将自然规范和正式规范联系起来，这些技术是模块化的（使它们能够扩展或局部修复）和证据生成（使其能够审核翻译以理解或调试翻译错误）；创新系统使用的词知识结构，实现不同半正式规范形式之间的高度直接重用；并通过使用所涉及的数据类型信息来改进语言词汇推理技术。这些都是主流机器学习技术难以实现的，该项目将与之进行比较。该项目将产生用于将英语句子翻译成基于属性的测试的新技术，用于正式正确性证明的证明辅助规范，以及用于正确性证明和自动查找错误的多重时态逻辑；该项目将在一个开源工具中实现它们。项目的影响被期望成为将行为的英语描述与软件质量专家使用的正式描述联系起来的工具（改进需求跟踪，软件专家和非技术客户之间的沟通，以及教育），在重要领域应用中对经典语言学理论的广泛验证，以及计算语言学和软件质量研究之间的技术和应用的交叉授粉。此外，该项目期望提高对该项目所研究的规范的单个软件块的信心。该项目将范畴语法作为其关键构建块，这是一种研究自然语言组合语义的方法，语言学家已经对它进行了广泛的审查，以涵盖来自不同语系的许多自然语言中各种微妙的语法现象。因此，与之前将形式规范和自然规范联系起来的方法不同，范畴语法预计不会对句子结构或语法灵活性施加先验限制。范畴语法还被用于将自然语言解析成各种逻辑，以处理各种语言现象（例如除了当前事实之外的时间和/或地点），它们还可以针对项目感兴趣的所有规范形式。该项目的关键新颖见解是，通过将给定逻辑中的单词的语义转换为针对其他逻辑的语义，能够跨不同逻辑共享语法的词法条目，并专注于可以深度嵌入到一个高表达逻辑（依赖类型理论）中的一系列规范，以改善共享。同时也从语言学研究中获益，并通过实验验证了这种逻辑更适合自然语言意义的表征。该项目将产生一个公开可用的原型系统，用于将英语与基于属性的测试、依赖类型理论的证明辅助规范和时间逻辑联系起来。该项目还将产生用于象征性地学习特定于项目或问题领域的单词的语法角色和语义的工具，仅从几个示例中。其他人可以对框架进行调整，以针对其他规范逻辑。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Recent years have seen dramatic advances in the ability to exploit formal or semi-formal specifications of software behavior for finding software bugs or building confidence in software correctness. However, these specifications are typically given in the form of logical formulae (for formal verification) or additional code (for typical software testing), while the original description of expected behavior is typically written in natural language such as English prose. Currently, these (semi)formal specifications are manually translated from natural language, leaving significant opportunities for misunderstandings or mistakes during translation, which can lead to validating that software satisfies useless or actively incorrect properties. The manual nature of the translation means it is difficult to audit after the fact. This project pursues new approaches to connecting natural language specifications of software behavior, at the level of single sentences, to the (semi)formal specifications currently accepted by many varieties of software quality tools, including property-based testing frameworks, proof assistants, and various tools using temporal logic specifications. The project's novelties are connecting natural and formal specifications using techniques drawn from the linguistics literature, which are modular (making them possible to extend or locally repair) and evidence-producing (making it possible to audit the translation for understanding or debugging translation errors); innovating on the structure of word knowledge used by the system to allow high degrees of direct reuse across different semi-formal specification forms; and improving techniques for linguistic lexicon inference by using information about the datatypes involved. These are all difficult to attain with mainstream machine learning techniques, against which the project will compare. The project will produce new techniques for translating English sentences into property-based tests for testing, proof assistant specifications for formal proofs of correctness, and multiple temporal logics for both correctness proofs and automated bug finding; and the project will implement them in an open source tool. The project's impacts are expected to be tools for connecting English descriptions of behavior to the formal descriptions used by software quality experts (improving requirement tracing, communication between software experts and non-technical clients, and education), extensive validation of classic linguistic theories in an important domain application, and cross-pollination of techniques and applications between computational linguistics and software quality research. Additionally, the project is expected to improve confidence in individual pieces of software whose specifications are studied by this project.The project takes categorial grammars as its key building block, an approach to compositional semantics of natural language that has been extensively vetted by linguists to cover a wide variety of subtle grammatical phenomena in many natural languages from different language families. Categorial grammars are therefore expected to impose no a priori restrictions on sentence structure or grammatical flexibility, unlike prior approaches to relating formal and natural specifications. Categorial grammars have also been used to parse natural language into enough various logics addressing varied linguistic phenomena (such as time and/or place in addition to current facts) that they can also target all of the specification forms of interest to the project. Key novel insights for the project are the ability to share lexical entries of the grammar across different logics by transporting the semantics of a word in a given logic into semantics targeting other logics, and focusing on a family of specifications that can be deeply embedded in one highly-expressive logic (dependent type theory) to improve sharing, as well as benefiting from and experimentally validating linguistics research positing that such logics are more appropriate representations of natural language meaning. The project will produce a publicly-available prototype system for relating English to property-based tests, proof assistant specifications in dependent type theory, and temporal logics. The project will also produce tools for symbolically learning the grammatical roles and semantics of words that are specific to a project or problem domain, from only a few examples. The framework will be adaptable by others to target other specification logics.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.