Pith. sign in

REVIEW 3 major objections 6 minor 29 references

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

T0 review · 3 major / 6 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Task-equivalent programs differ in how hard they are for automated verifiers, so generating several implementations raises the chance that at least one fully verifies.

desk verdict Solid empirical systems paper: diversity under frozen contracts measurably helps Why3 verification on a filtered 73-task benchmark; the cross-representation equivalence claim is softer than the recursive-vs-imperative gap. read the letter →

arxiv 2607.09366 v1 pith:NRTJLIEU submitted 2026-07-10 cs.SE cs.AIcs.LO

Shirley Yu , Ruben Martins This is my paper
classification cs.SEcs.AIcs.LO
keywords programverificationimplementationdiversityspecificationgenerationlargelanguagemodelsWhy3verifier-guidedrepairdeductive
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Producing software that a machine can prove correct is harder than producing code that merely passes tests: the program must also come with a formal contract and enough proof structure for a verifier to discharge. This paper argues that the shape of the implementation itself matters for that second step. Given the same programming task, recursive versus imperative code and array versus list representations create different proof obligations, so some variants are much easier for a verifier to accept than others. The authors build a staged pipeline that freezes a representation-specific contract, generates four structural families of candidates, filters them with tests, and then adds and repairs proof annotations under a fixed budget. On a 73-task benchmark of integer and sequence problems, verification rises from about a third of artifacts to just over half after two repair passes, and at least one variant verifies for two-thirds of the tasks—more than the best single family alone. The practical claim is that diversity of implementation structure is a useful lever for LLM-assisted verified programming, not only a way to hunt for a test-passing sample.

What carries the argument

Diversify2Verify: a three-stage pipeline that freezes a representation-specific contract after example-lemma validation, generates four implementation families (array/list × recursive/imperative) under a no-cross-family repair rule, and adds only proof scaffolding—invariants, variants, ghost code, lemmas—while preserving the frozen contract and executable behavior.

What would settle it

On a controlled set of tasks where array and list contracts are independently formalized and then proved equivalent, measure whether the same diversity gain disappears or shrinks when every variant is checked against one shared, machine-checked semantic target rather than representation-specific contracts.

Watch

Extended reading notes

Core claim

Task-equivalent implementations intended for the same natural-language problem can differ substantially in automated deductive verifiability. Generating recursive and imperative variants over both arrays and lists, then verifying them against fixed representation-specific contracts with bounded annotation repair, raises artifact-level success from 32.9% to 52.7% and yields at least one verified artifact for 49 of 73 tasks (67.1%), outperforming the strongest individual family (44 tasks).

Load-bearing premise

The accepted representation-specific contracts are treated as faithful enough stand-ins for the original task even though the paper does not prove that the array and list contracts are equivalent to each other or fully capture the natural-language intent.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. This paper studies whether implementation structure affects automated deductive verifiability for programs intended to solve the same task. It presents Diversify2Verify, a staged LLM pipeline for Why3 that (1) infers representation-specific contracts with example-derived test lemmas, freezes them, (2) generates and tests four families of implementations per task (array/list × recursive/imperative), and (3) adds proof annotations with two bounded verifier-guided repair passes. On a filtered 73-task benchmark (292 artifacts) drawn from LeetCode-style problems over integers, arrays, and lists, 96 artifacts verify initially and 154 after repair (32.9% → 52.7%); at least one variant verifies for 49/73 tasks (67.1%), versus 44 for the strongest single family. Recursive variants outperform imperative ones; array and list rates are similar. The authors conclude that task-equivalent implementations can differ substantially in verifiability and that diversity helps find verification-friendly artifacts.

Significance. If the empirical picture holds, the paper makes a useful systems contribution to LLM-assisted formal verification: it isolates implementation structure as a first-class factor in automated Why3 success, rather than treating verified synthesis as one-shot code-plus-spec generation. Strengths include a clear frozen-contract discipline that separates specification from proof repair, a public release of the 73-task benchmark, generated Why3 artifacts, and verification logs, and a transparent audit of specification match/preservation (291/292 preservation; limited manual follow-up of flagged mismatches). The recursive-vs-imperative gap and the repair analysis (many failures are localized bridge obligations) are actionable for future invariant/annotation tools. The absolute diversity gain is modest (49 vs 44 tasks), so the result is more a careful empirical demonstration than a large leap, but it is still a solid, reproducible contribution for the formal-methods and SE communities working on LLM+verifier pipelines.

major comments (3)
  1. Abstract, §1, and §4.1: The central claim uses “task-equivalent” for array and list variants verified against representation-specific contracts that are only intended to express the same task-level semantics. The paper correctly states that it does not prove logical equivalence of those contracts, and acceptance is only well-formedness plus discharge of example-derived lemmas (§4.1, §5). Cross-representation diversity gains can therefore be confounded by unequal contract strength or fidelity, not only by implementation structure. Please reframe the headline claims to separate (i) within-representation recursive vs imperative comparisons (cleaner) from (ii) cross-representation comparisons, and state explicitly in the abstract and conclusion that task-level 67.1% mixes both axes under unproved contract equivalence.
  2. §5 and Table 6: Benchmark construction retains only tasks for which Stage 1 accepts both array and list contracts, after type-based and LLM triage filters. The 49/73 (67.1%) task success rate is therefore conditional on a non-random, SMT-friendly subset with dual accepted contracts, not on a representative LeetCode sample. This conditioning is disclosed in §5 and §7.4 but is not reflected in the abstract or the main success-rate framing. Please add explicit conditioning language wherever the 67.1% figure is presented as the primary outcome, and consider reporting how many tasks were dropped at each filter stage so readers can assess selection effects.
  3. Table 7 and §7.2: The strongest single family (array-recursive) verifies 44 tasks; all four families together reach 49. The diversity benefit is thus +5 tasks over the best family. The text calls this “modest but measurable,” which is fair, but the abstract and conclusion lead with 67.1% without that comparison. Please elevate the best-family baseline next to the multi-variant rate in the abstract and discussion, and briefly address whether the +5 gain is robust (e.g., sensitivity to repair budget or to the particular four-family design) so the diversity claim is not overstated relative to simply preferring recursive array implementations.
minor comments (6)
  1. §7.4: The specification audit (GPT-5.5 judge + manual inspection of 10 flagged mismatches, one genuinely weak spec) is valuable; consider putting a short summary table of mismatch categories in the main text or appendix for reproducibility of the audit protocol.
  2. Table 1 is a helpful conceptual summary of proof burdens; a brief pointer from Table 7 back to Table 1 would tighten the link between predicted obligation shape and observed verification rates.
  3. §6: Solver versions (Z3 4.8.6, Alt-Ergo 2.4.0, CVC4 1.8) and Why3 1.8.2 are dated relative to current releases; a short note on whether results are expected to be sensitive to newer solvers would help future replication.
  4. Figure 1 is clear; ensure the repair arrows for Stage 1 vs Stage 2 vs Stage 3 match the budgets in Table 4 exactly (one vs five vs two) so the figure and table cannot be misread as open-ended repair.
  5. Related work (§8) is appropriately scoped; a one-sentence contrast with pass@k diversity in test-based code generation is already present—consider also citing any concurrent multi-implementation verification efforts if space allows.
  6. Minor wording: “find one a verifier can prove correct” (Conclusion) should be “find one that a verifier can prove correct.”

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: empirical verification rates measured by external Why3+SMT portfolio against frozen contracts, not derived by construction from inputs.

full rationale

This is an empirical systems paper whose central claims (artifact-level verification rising from 96/292 to 154/292 after repair; task-level success of 49/73 when using four variants) are observed outcomes of running a fixed Why3 1.8.2 + Z3/Alt-Ergo/CVC4 portfolio on generated artifacts. The pipeline freezes Stage-1 contracts before Stage-2/3, counts only fully discharged VCs, and reports comparative rates across representation/control-structure families. There is no fitted parameter renamed as a prediction, no self-definitional identity (X defined via Y then claimed to predict Y), no uniqueness theorem imported from the authors, and no load-bearing self-citation that forces the result. The acknowledged limitations (representation-specific contracts are only example-lemma-validated and not proved equivalent; the 73-task set is Stage-1-filtered) are validity/selection issues, not circular reductions of the measured rates to their inputs. The derivation chain is therefore self-contained against an external verifier.

Assumptions & free parameters 5 free parameters · 4 assumptions · 2 invented entities

The central claim rests on experimental design choices (budgets, models, solver portfolio, Stage 1 acceptance filter) and domain assumptions about Why3 contracts and task-level semantic equivalence, not on free physical constants or new particles. Invented entities are methodological constructs (pipeline stages, benchmark filter, four implementation families).

free parameters (5)
  • Stage 1 contract repair budget = 1
    Fixed at one repair attempt; directly affects which contracts and thus which tasks enter the evaluation set.
  • Stage 2 implementation attempt budget = 5
    Fixed at five attempts per family; determines which tested implementations reach Stage 3.
  • Stage 3 annotation repair budget = 2
    Fixed at two repair passes; the reported 52.7% rate is defined after exactly this budget.
  • Why3 solver timeout and portfolio = 10s; Z3/Alt-Ergo/CVC4
    10-second timeout per call with Z3 4.8.6, Alt-Ergo 2.4.0, CVC4 1.8 plus split/inline transformations; verification outcomes depend on this configuration.
  • Stage 2 executable test sample size = 20
    20 tests selected from each suite filter candidates before verification; not a full correctness proof.
assumptions (4)
  • domain assumption Accepted Stage 1 contracts plus discharged example lemmas are adequate semantic targets for the natural-language LeetCode-style tasks.
    Stated in Sections 4.1 and 5; acceptance is well-formedness plus example lemmas, not full semantic completeness.
  • ad hoc to paper Array and list representation-specific contracts express the same task-level semantics without a formal equivalence proof.
    Explicitly acknowledged in the introduction and Section 4.1; task-equivalence is operational, not proved.
  • domain assumption Why3 verification conditions discharged by the chosen SMT portfolio constitute full deductive verification of the artifact against its contract.
    Standard for Why3-based work; used as the success criterion throughout Section 7.
  • domain assumption LeetCodeDataset tasks over integers/arrays/lists that pass Stage 1 for both representations form a suitable controlled benchmark for studying diversity effects.
    Section 5 construction pipeline; authors note contamination risk and selection bias toward SMT-friendly tasks.
invented entities (2)
  • Diversify2Verify staged pipeline independent evidence
    purpose: Separate contract inference, diverse implementation generation, and bounded proof-annotation repair under a frozen-contract discipline.
    Core method introduced in Sections 3–4; evaluated empirically rather than derived from prior theory.
  • 73-task verification-oriented benchmark with four families per task independent evidence
    purpose: Provide controlled artifacts to measure how representation and control structure affect Why3 verifiability.
    Constructed in Section 5 from LeetCodeDataset via type filters, LLM triage, and Stage 1 acceptance; released publicly.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability." pith.science (2026). https://pith.science/paper/NRTJLIEU

@misc{pith2026260709366,
  author       = {Pith},
  title        = {Pith review of: Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NRTJLIEU}},
  note         = {Machine review of arXiv:2607.09366}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.09366 by the authors.

Figure 1
Figure 1. Overview of the Diversify2Verify staged verification pipeline. Why3 is used after Stage 1 to check the generated specification and test lemmas, during Stage 2 to exe￾cute test cases against candidate implementations, and after Stage 3 to discharge the verification conditions for the final annotated artifact. Running example. We use Maximum Distance Between a Pair of Values as a running example. The function takes tw… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

29 extracted references · 7 linked inside Pith

  1. [1]

    CoRRabs/2108.07732(2021)

    Austin,J.,Odena,A.,Nye,M.I.,Bosma,M.,Michalewski,H.,Dohan,D.,Jiang,E., Cai, C.J., Terry, M., Le, Q.V., Sutton, C.: Program Synthesis with Large Language Models. CoRRabs/2108.07732(2021)

    arXiv 2021

  2. [2]

    In: ICSE

    Chakraborty,S.,Ebner,G.,Bhat,S.,Fakhoury,S.,Fatima,S.,Lahiri,S.K.,Swamy, N.: Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. In: ICSE. pp. 1755–1767. IEEE (2025)

    2025

  3. [3]

    CoRRabs/2310.09342(2023)

    Chakraborty, S., Lahiri, S.K., Fakhoury, S., Musuvathi, M., Lal, A., Rastogi, A., Senthilnathan, A., Sharma, R., Swamy, N.: Ranking LLM-Generated Loop Invari- ants for Program Verification. CoRRabs/2310.09342(2023)

    arXiv 2023

  4. [4]

    CoRRabs/2107.03374(2021)

    Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H.P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, P., Such, F.P., Cummings, D., Plappert, M., Chan...

    arXiv 2021

  5. [5]

    ACM Softw

    Endres, M., Fakhoury, S., Chakraborty, S., Lahiri, S.K.: Can Large Language Mod- els Transform Natural Language Intent into Formal Method Postconditions? Proc. ACM Softw. Eng.1(FSE), 1889–1912 (2024)

    1912

  6. [6]

    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Com- put. Program.69(1-3), 35–45 (2007)

    2007

  7. [7]

    In: ESOP

    Filliâtre, J.C., Paskevich, A.: Why3—where programs meet provers. In: ESOP. pp. 125–128. Springer (2013)

    2013

  8. [8]

    First, E., Rabe, M.N., Ringer, T., Brun, Y.: Baldur: Whole-proof generation and repair with large language models. In: FSE. pp. 1229–1241. ACM (2023)

    2023

Show all 29 references
  1. [9]

    TU Wien Aca- demic Press (2025)

    Kabra, A., Laurent, J., Bharadwaj, S., Martins, R., Mitsch, S., Platzer, A.: Can Large Language Models Autoformalize Kinematics? In: FMCAD. TU Wien Aca- demic Press (2025)

    2025

  2. [10]

    CoRRabs/2311.07948(2023)

    Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. CoRRabs/2311.07948(2023)

    2023 arXiv

  3. [11]

    Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying rust programs using linear ghost types. Proc. ACM Program. Lang.7(OOPSLA1), 286–315 (2023)

    2023

  4. [12]

    In: LPAR

    Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: LPAR. pp. 348–370. LNCS, Springer (2010) 20 Yu and Martins

    2010

  5. [13]

    CoRRabs/2203.07814(2022)

    Li, Y., Choi, D.H., Chung, J., Kushman, N., Schrittwieser, J., Leblond, R., Ec- cles, T., Keeling, J., Gimeno, F., Lago, A.D., Hubert, T., Choy, P., de Mas- son d’Autume, C., Babuschkin, I., Chen, X., Huang, P., Welbl, J., Gowal, S., Cherepanov, A., Molloy, J., Mankowitz, D.J....

    2022 arXiv

  6. [14]

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M.R.H., Amin, N., Tegmark, M.: DafnyBench: A Benchmark for Formal Software Verification. Trans. Mach. Learn. Res.2025(2025)

    2025

  7. [15]

    Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: Automated generation of formal programspecificationsvialargelanguagemodels.In:ICSE.pp.16–28.IEEE(2025)

    2025

  8. [16]

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng.1(FSE), 812–835 (2024)

    2024

  9. [17]

    In: CADE

    de Moura, L., Ullrich, S.: The Lean 4 Theorem Prover and Programming Language. In: CADE. pp. 625–635. LNCS, Springer (2021)

    2021

  10. [18]

    Mugnier, E., Gonzalez, E.A., Polikarpova, N., Jhala, R., Zhou, Y.: Laurel: Unblock- ing Automated Verification with Large Language Models. Proc. ACM Program. Lang.9(OOPSLA1), 1519–1545 (2025)

    2025

  11. [19]

    In: Dependable Software Systems Engineering, pp

    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A Verification Infrastructure for Permission-Based Reasoning. In: Dependable Software Systems Engineering, pp. 104–125. IOS Press (2017)

    2017

  12. [20]

    In: Tools for Practical Software Verification, LASER

    Paulin-Mohring, C.: Introduction to the Coq Proof-Assistant for Practical Soft- ware Verification. In: Tools for Practical Software Verification, LASER. pp. 45–95. LNCS, Springer (2011)

    2011

  13. [21]

    Pirzada,M.A.A.,Reger,G.,Bhayat,A.,Cordeiro,L.C.:LLM-GeneratedInvariants for Bounded Model Checking Without Loop Unrolling. In: ASE. pp. 1395–1407. ACM (2024)

    2024

  14. [22]

    CoRRabs/2411.15143(2024)

    Poesia, G., Loughridge, C., Amin, N.: dafny-annotator: Ai-assisted verification of dafny programs. CoRRabs/2411.15143(2024)

    2024 arXiv

  15. [23]

    CoRRabs/2511.00125(2025)

    Silva, Á.F., Mendes, A., Martins, R.: Inferring multiple helper dafny assertions with llms. CoRRabs/2511.00125(2025)

    2025

  16. [24]

    In: AI Verification

    Sun, C., Sheng, Y., Padon, O., Barrett, C.W.: Clover: Closed-Loop Verifiable Code Generation. In: AI Verification. pp. 134–155. LNCS, Springer (2024)

    2024

  17. [25]

    In: ICLR

    Wu, H., Barrett, C.W., Narodytska, N.: Lemur: Integrating large language models in automated program verification. In: ICLR. OpenReview.net (2024)

    2024

  18. [26]

    In: NeurIPS (2022)

    Wu, Y., Jiang, A.Q., Li, W., Rabe, M.N., Staats, C., Jamnik, M., Szegedy, C.: Autoformalization with Large Language Models. In: NeurIPS (2022)

    2022

  19. [27]

    CoRRabs/2504.14655(2025)

    Xia, Y., Shen, W., Wang, Y., Liu, J.K., Sun, H., Wu, S., Hu, J., Xu, X.: Leetcode- dataset: A temporal dataset for robust evaluation and efficient training of code llms. CoRRabs/2504.14655(2025)

    2025 arXiv

  20. [28]

    Yang, C., Li, X., Misu, M.R.H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S.K., Lorch, J.R., Lu, S., Yang, F., Zhou, Z., Lu, S.: Autoverus: Automated proof generation for rust code. Proc. ACM Program. Lang.9(OOPSLA2), 3454–3482 (2025)

    2025

  21. [29]

    In: NeurIPS (2023)

    Yang, K., Swope, A.M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R.J., Anandkumar, A.: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In: NeurIPS (2023)

    2023

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.