权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

SHF：小：用逻辑和语言学缩小规范差距

基本信息

批准号：
2220991
负责人：
Colin Gordon
金额：
$ 52.44万
依托单位：
Drexel University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2022
资助国家：
美国
起止时间：
2022-10-01 至 2025-09-30
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220991&HistoricalAwards=false
关键词：
SHF Small Closing Specification Gap

项目摘要

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.

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