Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?

📄 arXiv: 2510.12702v1 📥 PDF

作者: Cedric Richter, Heike Wehrheim

分类: cs.SE, cs.AI, cs.PL

发布日期: 2025-10-14

备注: under submission

💡 一句话要点

提出NL2Contract，利用大语言模型推断形式化契约以提升软件自动验证效果

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 大语言模型 软件契约 前置条件 后置条件

📋 核心要点

  1. 现有软件验证方法依赖形式化规范，但实际代码中缺乏，阻碍了其应用。
  2. 提出NL2Contract任务，利用LLM将自然语言描述转化为包含前置条件和后置条件的形式化契约。
  3. 实验表明，LLM生成的契约能有效区分错误行为，并减少自动软件验证中的误报。

📝 摘要（中文）

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

🔬 方法详解

问题定义：现有自动软件验证工具依赖于形式化的软件规范（如前置条件和后置条件），但实际软件开发中往往缺乏这些规范。虽然可以使用LLM生成后置条件，但单独使用后置条件进行验证容易产生误报，影响验证效率和准确性。

核心思路：论文的核心思路是利用LLM同时推断前置条件和后置条件，形成完整的形式化契约。通过更全面的契约信息，可以更准确地描述函数的行为，从而减少验证过程中的误报，提高软件验证的可靠性。

技术框架：论文提出了NL2Contract框架，该框架使用LLM将自然语言描述（例如函数名、注释、文档）转换为形式化的功能契约，包括前置条件和后置条件。然后，将生成的契约提供给自动软件验证器，以验证软件的正确性。框架包含数据收集、模型训练、契约生成和验证等阶段。

关键创新：该论文的关键创新在于同时推断前置条件和后置条件，形成完整的形式化契约。与仅生成后置条件的方法相比，NL2Contract能够提供更全面的函数行为描述，从而提高软件验证的准确性和可靠性。此外，论文还提出了评估NL2Contract方法的指标，包括契约的可靠性、错误区分能力以及在自动软件验证中的可用性。

关键设计：论文使用了多种LLM进行实验，包括但不限于GPT系列模型。针对NL2Contract任务，论文可能采用了微调（fine-tuning）或提示工程（prompt engineering）等技术来优化LLM的性能。在评估方面，论文设计了多种指标来衡量生成契约的质量，例如，使用自动软件验证器验证生成的契约，并统计误报的数量。此外，论文还可能考虑了契约的表达能力和可理解性等因素。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，LLM在生成功能契约方面表现出色，生成的契约对所有可能的输入都具有可靠性。与仅使用后置条件相比，使用LLM推断的功能契约能够显著减少自动软件验证器产生的误报。此外，LLM推断的前置条件与开发人员的意图高度一致，有助于发现真实世界的软件错误。

🎯 应用场景

该研究成果可应用于软件开发和测试的各个阶段，例如在编码阶段自动生成函数契约，帮助开发者编写更可靠的代码；在测试阶段，利用生成的契约进行自动化测试，提高测试覆盖率和效率。此外，该技术还可用于遗留系统的代码理解和重构，帮助开发者更好地理解和维护现有代码。

📄 摘要（原文）

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.