mlsanityData to 7 Oct 2026

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability

arXiv 2607.09366 ↗First posted 10 Jul 2026cs.SE cs.AI cs.LOcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 21 of its 29 references that are in the map. First posted on arXiv 10 Jul 2026.

Builds on

21 of 29 references.

References · 21

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2021Program Synthesis with Large Language Modelscited by 3,509
  3. 2022Competition-Level Code Generation with AlphaCodecited by 1,427
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  5. 2022Autoformalization with Large Language Modelscited by 252
  6. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  7. 2025LeetCodeDataset: A Temporal Dataset for Robust Evaluation and Efficient Training of Code LLMscited by 67
  8. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  9. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  10. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  11. 2023Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?cited by 53
  12. 2024SpecGen: Automated Generation of Formal Program Specifications via Large Language Modelscited by 51
9 more
  1. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 50
  2. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  3. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  4. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
  5. 2023Ranking LLM-Generated Loop Invariants for Program Verificationcited by 33
  6. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  7. 2024dafny-annotator: AI-Assisted Verification of Dafny Programscited by 8
  8. 2025Inferring multiple helper Dafny assertions with LLMscited by 3
  9. 2025Can Large Language Models Autoformalize Kinematics?cited by 1

Built on by

Not cited yet.