程序验证对于软件的正确性至关重要，但在实践中完全验证程序仍然十分困难。本文研究了实现结构是否影响自动化可验证性，特别是在多个生成程序旨在满足相同任务级语义的情况下。我们提出了 Diversify2Verify，这是一个基于 LLM 的分阶段管道，用于 Why3，能够推断特定表示的合约，生成和测试多样化的递归和命令式数组/列表实现，并尝试通过有界验证器引导的注释修复进行验证。
我们还构建了一个面向验证的基准，其中包含 73 个整数、数组和列表任务，产生了 292 种实现变体。Diversify2Verify 初步验证了 96 个工件，在经过两次修复后验证数量增至 154，工件级验证率从 32.9% 提升至 52.7%。在任务级别上，73 个任务中至少有一个变体通过验证的比例为 67.1%。这些结果表明，任务等效的实现在可验证性上存在显著差异，而实现的多样性有助于发现友好的验证工件。
博主点评： 本文通过 Diversify2Verify 展示了实现多样性在程序验证中的重要性，突出表明任务等效的程序在验证上可能有显著差异。这一研究方向为未来的自动化验证工具开发提供了新的思路。尤其是在软件工程日益复杂的背景下，探索不同实现的可验证性显得尤为重要。