同一任务的不同代码实现，验证难易程度差异大，多样性提升验证成功率。
Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
- 用大模型生成多种数组/链表实现，测试不同结构对验证的影响。
- 修复两次后，96个初始可验证，154个最终可验证，整体验证率从32.9%升至52.7%。
- 适合关注程序验证、自动化修复与代码多样性研究的读者。
程序验证对保障软件正确性至关重要，但实际中仍难以实现完全验证。本文研究在满足相同任务语义的前提下，不同实现结构是否影响自动化验证难度。提出Diversify2Verify，一个基于大模型的分阶段流程，针对Why3系统推导特定表示的契约，生成并测试多样化的递归与迭代数组/链表实现，并通过有限验证器引导的注解修复尝试完成验证。构建了一个面向验证的基准数据集，覆盖整数、数组和列表共73个任务，生成292个实现变体。Diversify2Verify初始验证成功96个，经两轮修复后达154个，整体验证率从32.9%提升至52.7%。在任务层面，73个任务中有49个至少有一个变体可验证，成功率67.1%。结果表明，语义等价的实现之间验证难度差异显著，且实现多样性有助于发现更易验证的代码。
原文摘要 · Abstract (English)
Program verification is crucial for software correctness, but producing fully verified programs remains difficult in practice. This paper studies whether implementation structure affects automated verifiability when multiple generated programs are intended to satisfy the same task-level semantics. We present Diversify2Verify, a staged LLM-based pipeline for Why3 that infers representation-specific contracts, generates and tests diverse recursive and imperative array/list implementations, and attempts verification with bounded verifier-guided annotation repair. We also construct a verification-oriented benchmark of 73 tasks over integers, arrays, and lists, yielding 292 implementation variants. Diversify2Verify verifies 96 artifacts initially and 154 after two repair passes, improving artifact-level verification from 32.9% to 52.7%. At the task level, at least one variant verifies for 49 of 73 tasks, a 67.1% success rate. These results show that task-equivalent implementations can differ substantially in verifiability and that implementation diversity helps find verification-friendly artifacts.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。