Natural Language based Specification and Verification
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在试图证明一台庞大而复杂的机器（比如汽车发动机或计算机程序）永远不会损坏或引发事故。
问题：那台“大得读不完”的机器
在计算机代码的世界里，尤其是在 C 和 C++ 等语言中，出错的方式多种多样。指针可能指向空值，内存可能在被释放后仍被使用，或者缓冲区可能太小。这些错误就像大坝上的微小裂缝；它们通常是由于机器不同部分之间的相互作用而产生的。
传统上，要证明一台机器是安全的，你需要一本严格、数学化的规则手册（形式化规范）。但编写这本规则手册极其困难且枯燥。这就像在检查发动机是否运转之前，试图为发动机的每一个齿轮都写一份法律合同。
最近，我们拥有了强大的 AI 模型（大型语言模型或 LLM），它们擅长阅读代码并发现漏洞。然而，要求这些 AI 一次性审视整个“发动机”并回答“这安全吗？”通常会失败。发动机太大了，AI 会感到困惑，从而错过活塞与阀门之间微妙的联系。
解决方案：NLForge（“摘要笔记”方法）
这篇论文介绍了一种名为 NLForge 的新工具。NLForge 没有要求 AI 一次性阅读整台机器，而是采用了一种称为组合验证的策略。
把它想象成一群检查员在检查一座巨大的摩天大楼：
- 旧方法（整体式）： 你雇佣一名检查员站在屋顶，试图一次性审视整栋大楼。他们会被压垮，错过细节，无法看到 10 楼的管道如何影响 2 楼的电梯。
- NLForge 方法（组合式）： 你将大楼分解为楼层。
- 首先，你派一名检查员去地下室。他们检查地基，并写下一份关于地下室功能的简单、纯英文的笔记（摘要）（例如：“这一层容纳水，但前提是管道已连接”）。
- 接下来，你派一名检查员去 1 楼。他们阅读地下室的笔记。他们不需要查看地下室的蓝图；他们只需要知道规则。他们检查 1 楼，写下自己的笔记，然后将其向上传递。
- 这个过程一直持续到屋顶。每位检查员只需担心自己的楼层，并信任来自下方楼层的笔记。
秘密武器：纯英文笔记
这里有个转折：大多数之前的尝试都使用严格的数学语言来撰写这些笔记。但 AI 在理解和撰写自然语言（如英语）方面，比处理复杂的数学符号更擅长。
NLForge 要求 AI 用纯英文撰写这些“笔记”。
- 与其使用复杂的公式，AI 会写道：“这个函数会给你一个全新的内存块，但它可能是空的（null）。”
- 下一个阅读这条笔记的 AI 能完美理解它，并利用该信息检查代码的下一部分。
他们的发现
研究人员在一组来自 SV-COMP 竞赛的困难代码挑战上测试了这种方法。
- AI 能成为验证器吗？ 可以，但有个条件。AI 非常擅长发现漏洞（高召回率），意味着它很少遗漏问题。然而，有时它会在没有狼的情况下大喊“狼来了”（误报）。它尚未完美到可以取代严格的数学证明，但在快速发现潜在问题方面表现出色。
- “记笔记”的方法有效吗？ 有效！当 AI 使用“摘要笔记”方法（组合式）时，它发现的漏洞数量明显多于试图一次性阅读整个代码时。这对于那些难以记住长上下文的小型 AI 模型来说尤其如此。这些笔记就像作弊小抄，帮助它们更好地进行推理。
结论
这篇论文认为，我们不应仅仅利用 AI 为其他工具生成严格的数学规则以供检查。相反，我们应该让 AI 本身成为推理者，利用简单、人类可读的摘要，将庞大而可怕的问题分解为小块、可管理的部分。
这就像拼一幅巨大的拼图：与其盯着整个盒子看得头晕目眩，不如将拼图块分成小堆（摘要），然后逐一解决，并相信前一堆的拼图块能完美地契合下一堆。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。