Title: Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? Show Chinese title

Title: 超越后条件：大型语言模型能否推断出形式化契约以实现自动软件验证？

Abstract: Automatic software verifiers have become increasingly effective at the task of checking software against (formal) specifications. Yet, their adoption in practice has been hampered by the lack of such specifications in real world code. Large Language Models (LLMs) have shown promise in inferring formal postconditions from natural language hints embedded in code such as function names, comments or documentation. Using the generated postconditions as specifications in a subsequent verification, however, often leads verifiers to suggest invalid inputs, hinting at potential issues that ultimately turn out to be false alarms. To address this, we revisit the problem of specification inference from natural language in the context of automatic software verification. In the process, we introduce NL2Contract, the task of employing LLMs to translate informal natural language into formal functional contracts, consisting of postconditions as well as preconditions. We introduce metrics to validate and compare different NL2Contract approaches, using soundness, bug discriminative power of the generated contracts and their usability in the context of automatic software verification as key metrics. We evaluate NL2Contract with different LLMs and compare it to the task of postcondition generation nl2postcond. Our evaluation shows that (1) LLMs are generally effective at generating functional contracts sound for all possible inputs, (2) the generated contracts are sufficiently expressive for discriminating buggy from correct behavior, and (3) verifiers supplied with LLM inferred functional contracts produce fewer false alarms than when provided with postconditions alone. Further investigations show that LLM inferred preconditions generally align well with developers intentions which allows us to use automatic software verifiers to catch real-world bugs. Show Chinese abstract

Abstract: 自动软件验证工具在检查软件是否符合（形式化）规范的任务上已经变得越来越有效。 然而，在实际应用中，由于现实世界代码中缺乏这样的规范，其采用受到了阻碍。 大型语言模型（LLMs）在从嵌入在代码中的自然语言提示（如函数名、注释或文档）中推断出形式化后置条件方面表现出潜力。 然而，将生成的后置条件作为后续验证的规范，通常会导致验证工具建议无效输入，这表明可能存在最终被证明是误报的问题。 为了解决这个问题，我们重新审视了在自动软件验证背景下从自然语言进行规范推断的问题。 在此过程中，我们引入了NL2Contract，即利用LLMs将非形式化的自然语言翻译成形式化的功能契约的任务，包括后置条件以及前置条件。 我们引入了度量标准来验证和比较不同的NL2Contract方法，使用正确性、生成契约的错误区分能力以及它们在自动软件验证背景下的可用性作为关键度量标准。 我们使用不同的LLMs对NL2Contract进行了评估，并将其与后置条件生成任务nl2postcond进行了比较。 我们的评估显示，（1）LLMs通常能够为所有可能的输入生成正确的功能契约，（2）生成的契约足够表达以区分有错误的行为和正确的行为，以及（3）提供LLMs推断的功能契约的验证工具比仅提供后置条件时产生的误报更少。 进一步的研究表明，LLMs推断的前置条件通常与开发人员的意图一致，这使我们能够使用自动软件验证工具来捕捉现实世界中的错误。