ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
本文介绍了 ConVer，这是一种自上而下的组合式验证工具，它利用大语言模型合成函数契约，并通过 CEGAR-CEGIS 循环对其进行迭代优化，以克服在验证大型 C 程序及转换后的 LF 模型时面临的状态空间爆炸问题。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图证明一个庞大而复杂的工厂运转完美。这家工厂拥有成千上万台机器、传送带和工人，它们全部交织在一个巨大的网络中。如果你试图在同一时刻观察每一台机器、每一个齿轮和每一位工人以找出错误，你会感到不堪重负。海量的信息会让你的大脑在找到错误之前就“爆炸”。这正是软件工程师在验证大型计算机程序时面临的问题：计算机的状态数量太多，无法一次性全部检查。
本文介绍了CONVER，这是一款旨在通过改变我们检查代码的方式来解决这种“不堪重负”问题的新工具。与其盯着整个工厂，CONVER 更像一位明智的自上而下的管理者，将问题分解为微小、可管理的部分。
以下是 CONVER 的工作原理，使用简单的类比说明：
1. “自上而下”策略：蓝图与砖块
通常，要验证一个程序，你必须在检查整个系统之前，为每一个函数（每一台小机器）编写详细的规则手册（“契约”）。这就像在宣称汽车安全之前，试图为汽车上的每一颗螺丝编写手册。这不仅耗时漫长，而且需要专家参与。
CONVER 颠覆了这一做法。
- 类比：假设你的目标是：“工厂绝不能生产出红色的 Widget。”
- 旧方法：你询问每一位工人：“你们的规则是什么？”并试图自下而上地构建系统。
- CONVER 方法：你从大目标（“没有红色 Widget"）开始。然后，你请求一个 AI 助手（大型语言模型，或 LLM）去猜测每位工人的规则，以确保大目标得以实现。这就像说：“如果装配线工人遵循这些简单的规则，最终产品就是安全的。”你无需了解工人的大脑如何运作，只需确认他们遵循规则即可。
2. “智能循环”：侦探与 AI
一旦 AI 猜测出规则（契约），CONVER 就会通过一个两步循环来测试它们，就像侦探和嫌疑人在玩“猜规则”的游戏。
- 步骤 A：系统检查（管理者）：CONVER 检查如果所有人遵循猜测的规则，整个工厂是否运转正常。它不查看机器内部，只是信任这些规则。
- 步骤 B：函数检查（检查员）：CONVER 随后检查实际机器是否真的能遵循这些规则。
- "CEGAR"循环：如果机器未能遵循规则，CONVER 不会轻易放弃。它会获取具体的错误（“反例”）并将其展示给 AI。
- 类比：AI 说：“我以为工人能举起 50 磅。”检查员说：“不，工人丢下了一箱 50 磅的货物。”AI 从这个具体的失败中学习，并写出一条新的、更好的规则：“工人最多能举起 40 磅。”
- 这个过程会不断重复，直到规则完美无缺。
3. "SMART ICE"学习：过滤噪音
有时，AI 犯错是因为它误解了问题，而不是规则本身有误。为了解决这个问题，CONVER 使用了一种称为SMART ICE 学习的技术。
- 类比：想象你在教一只狗做把戏。如果当你说“定住”时狗坐下了，你知道这是一个好把戏。但如果狗坐下是因为它看到了一只松鼠，那就是误报。
- 工作原理：CONVER 过滤掉“误报”（噪音），只保留“真实错误”（信号）。它将错误分类为“正例”（这成功了）、“负例”（这肯定失败了）和“蕴含”（如果发生这个，那么那个必须发生）。这有助于 AI 更快地学习，并避免被自己的错误搞糊涂。
4. “预抽象”技巧：卡通版本
代码的某些部分过于复杂（例如包含无限循环的工厂），以至于即使检查规则也变得太难。
- 类比：如果一台机器太复杂而无法详细绘制，CONVER 会先画出一个简单的卡通版本。它检查这个卡通版本是否有效。如果有效，它就用真实机器替换卡通版本并再次检查。
- 这使得 CONVER 能够处理那些通常会导致计算机内存崩溃的程序。
他们发现了什么？
研究人员在四个不同的代码“健身房”中测试了 CONVER，范围从简单的数学谜题到复杂的现实世界文件解析器和递归循环。
- 简单程序：在一组 45 个标准程序上，CONVER 取得了巨大成功，验证了82% 到 96%的程序。其中大多数仅在一轮检查中就解决了，这意味着 AI 几乎在第一次就完美地猜出了规则。
- 更难的程序：在更困难的集合上（如解析安全证书或复杂的递归循环），成功率下降到33% 到 64%。这是可以预期的，因为这些程序更难理解。
- "AI"因素：他们测试了三种不同的 AI 模型（Qwen、Claude 和 GPT）。AI 模型越智能，CONVER 的表现就越好。最智能的 AI（GPT-OSS 120b）解决了最多的问题，证明了 AI“猜测”的质量是成功的关键。
核心结论
CONVER 是一款利用 AI 编写软件“规则手册”的工具，然后利用智能的迭代过程修正这些规则手册，直到它们完美无缺。它将一个庞大且无法解决的谜题转化为一系列可解决的小步骤。
- 它并没有取代验证的需求；它自动化了最困难的部分（编写规则）。
- 它并不能保证在每一个复杂的程序上都达到 100% 的成功，但它解决了许多以前无法自动检查的问题。
- 它通过倾听失败来工作：每次软件失败时，该工具都会确切地学习原因，并请求 AI 用更好的猜测再次尝试。
简而言之，CONVER 就像一位不知疲倦、超级聪明的管理者，他将巨大的问题分解为小任务，从每一次错误中学习，并不断完善计划，直到工作完成。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。