该论文介绍了 Diversify2Verify，这是一种针对 Why3 的分阶段基于 LLM 的流水线，用于生成多样化的递归和命令式数组/列表实现，以增强自动可验证性。该方法推断特定于表示的契约，并采用有界验证器引导的注释修复来处理验证失败。

  • 作者构建了一个包含 73 个任务的基准测试，涉及整数、数组和列表，产生了 292 种实现变体。
  • Diversify2Verify 最初验证了 96 个工件，经过两轮修复后增加到 154 个。
  • 工件级别的验证率从 32.9% 提高到 52.7%。
  • 在任务级别，73 个任务中有 49 个至少有一个变体通过验证，成功率达到 67.1%。

这些结果表明，实现多样性有助于在任务等效的程序中找到有利于验证的工件。