PaperlayerView exact revision on arXiv

Source-linked AI summary

Clover: Closed-Loop Verifiable Code Generation

Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett

arXiv:2310.17807v4cs.AIcs.LGcs.SE

TL;DR

Generated code lacks a trustworthy correctness check, while human oversight limits scalability. Clover checks consistency among code, annotations, and docstrings; experiments report strong rejection of incorrect examples alongside high acceptance of correct ones.

  • Problem

    There is no trustworthy way to ensure AI-generated code is correct, and human oversight limits scalable curation.

    Source: §1 · pp. 1–2

  • Method

    Clover checks consistency among code, formal annotations, and docstrings, using LLM reconstruction alongside formal verification checks.

    Source: §1 · p. 3, §3.2 · p. 6

  • Results

    Clover accepts 87% of correct CloverBench examples and rejects 100% of adversarial incorrect examples, and detects 6 incorrect MBPP-DFY-50 programs while accepting 89% of correct ones.

    Source: §1 · p. 3, §6 · p. 18

  • Takeaways & Limitations

    Clover reduces checking code correctness to the more accessible problem of checking consistency among code, annotations, and docstrings.

    Source: §1 · p. 3, §6 · p. 18

    The initial dataset is restricted to single-method examples without helper functions, and requires precise inputs that determine a unique output.

    Source: §3.2 · p. 5, §4.2 · p. 11

Abstract

from arXiv · show

The use of large language models for code generation is a rapidly growing trend in software development. However, without effective methods for ensuring the correctness of generated code, this trend could lead to undesirable outcomes. In this paper, we introduce a new approach for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which uses consistency checking to provide a strong filter for incorrect code. Clover performs consistency checks among code, docstrings, and formal annotations. The checker is implemented using a novel integration of formal verification tools and large language models. We provide a theoretical analysis to support our thesis that Clover should be effective at consistency checking. We also empirically investigate its performance on a hand-designed dataset (CloverBench) featuring annotated Dafny programs at a textbook level of difficulty. Experimental results show that for this dataset: (i) LLMs are reasonably successful at automatically generating formal specifications; and (ii) our consistency checker achieves a promising acceptance rate (up to 87%) for correct instances while maintaining zero tolerance for adversarial incorrect ones (no false positives). Clover also discovered 6 incorrect programs in the existing human-written dataset MBPP-DFY-50.

1 Introduction

Clover addresses the challenge of checking generated-code correctness by pairing code with formal annotations and natural-language docstrings, then testing their consistency. Initial evaluations report strong rejection of incorrect examples alongside substantial acceptance of correct ones.

1 Introduction

  • The paper identifies specification creation as a bottleneck because formal annotations require expertise to ensure they are consistent and accurately express intended functionality.Existing formal verification tools can automate other steps, but the specification step remains difficult to automate.Source: §1 · p. 2
  • Clover’s verification phase checks consistency among code, formal annotations, and docstrings, aiming to ensure the code matches both its annotations and natural-language description.The paper’s hypothesis is that passing checks also indicates the annotations capture the code’s full functionality.Source: §1 · p. 3
  • The authors introduce Clover and CloverBench, evaluate GPT-4 generation and consistency checking, and report finding 6 incorrect programs in MBPP-DFY-50.CloverBench contains manually annotated Dafny programs with docstrings, ground-truth examples, and adversarial incorrect examples.Source: §1 · pp. 3–4
  • Clover accepts 87% of correct CloverBench examples while rejecting 100% of adversarial incorrect examples.The authors also report detecting 6 incorrect programs and accepting 89% of correct programs in MBPP-DFY-50.Source: §1 · p. 3

2 Preliminaries: Deductive Program Verification

Deductive verification checks whether code satisfies a formal specification expressed through annotations. Dafny is the verification language and tool used in the paper’s evaluation.

2 Preliminaries: Deductive Program Verification

  • Deductive verification checks that code satisfies annotations, typically by automatically validating logical verification conditions with SMT solvers.The annotations include preconditions, postconditions, and loop invariants.Source: §2 · p. 4
  • A precondition describes valid starting states, while a postcondition describes the required state after execution.The paper assumes function-level annotations and notes that loops require invariants for induction over iterations.Source: §2 · p. 4
  • Dafny provides a compiler and a verifier that formally checks whether code conforms to its specification.The section illustrates this with a maximum-array function and annotations specifying that its result is an array maximum.Source: §2 · pp. 4–5

3 Clover

Clover uses LLM reconstruction and equivalence checks to test whether code, annotations, and docstrings agree. Its generation phase can produce different components, while its verification phase requires all consistency checks to pass.

3.1 Clover Generation Phase

  • The generation-phase feasibility study covers generating code from annotations, annotations from code, or both from a natural-language description.These evaluations are intended to demonstrate feasibility, not to chart new research directions.Source: §3.1 · p. 5

3.2 Clover Verification Phase

  • Clover tests consistency by reconstructing one component from another and checking equivalence, alongside a formal code-to-annotations soundness check.An instance passes only if all six directed checks pass; reconstruction uses an LLM, while equivalence checks use formal tools, text comparison, or sampled code outputs.Source: §3.2 · p. 6
  • The code-to-annotations checks verify soundness with a deductive tool and completeness by reconstructing equivalent code from the annotations.The paper says its formal soundness and annotation-equivalence checks are exact, while code equivalence is strong but not perfect.Source: §3.2 · pp. 6, 8

3.3 Consistency Checking Example

  • The maxArray example illustrates reconstruction checks, including generating annotations from a docstring and checking them against the original annotations.The example also describes reconstructing docstrings from annotations and using code generation and output comparisons for other checks.Source: §3.3 · pp. 9–10

4 Evaluation

The evaluation tests GPT-4-based Clover using hand-crafted Dafny examples, an external Dafny dataset, adversarial mutations, and a preliminary Verus study. Results show high acceptance of correct examples and rejection of incorrect ones, with scope and generation constraints noted.

4 Evaluation

  • The evaluation prototype uses GPT-4 with Dafny, and the ground-truth examples are restricted to one method without helper functions.The study also requires precise docstrings and annotations that determine a unique result for each input.Source: §4 · p. 10, §4.2 · p. 11

4.1.1 Dafny

  • CloverBench contains 60 hand-crafted Dafny examples with verified ground-truth variants and four adversarial incorrect variants per program.The dataset requires precise specifications that determine a unique output for every input; code equivalence is approximated using five input tests.Source: §4.1.1 · p. 11

4.2 Generation Phase

  • GPT-4 generated code for 53 of 60 examples from specifications and annotations for 41 of 60 with three tries and maximal Dafny feedback.The generation study used 60 CloverBench examples and manually checked generated code for correctness.Source: §4.2 · pp. 11–12
  • From docstrings, GPT-4 generated both code and annotations for 39 of 60 programs after 20 tries, and Clover accepted a correct answer for 39 of 41 eligible cases without accepting an incorrect answer.The authors describe these results as early and say more complicated examples must be tried.Source: §4.2 · p. 12

4.3 Verification Phase: Results on Ground-Truth Examples

  • At k = 10, Clover accepts 52 of 60 correct examples and rejects all incorrect examples.With one run, it accepts 45 of 60 correct examples; the authors attribute most failures to incorrect or imprecise reconstruction.Source: §4.3 · p. 13, Table 1 · p. 13

4.4 Verification Phase: Results on MBPP-DFY-50

  • On MBPP-DFY-50, Clover identifies 6 incorrect programs and accepts 89% of correct programs while rejecting all incorrect programs in the in-scope set.Seventeen of 50 programs are out of scope: two have imprecise docstrings and 15 require auxiliary functions or predicates.Source: §4.4 · pp. 14–15

4.5 Verification Phase: Results on Adversarial Examples

  • Clover rejects all tested adversarial examples that pass Dafny verification, with no incorrect example passing all six consistency checks.The paper notes that a Dafny-only approach would accept the constructed adversarial examples because they pass its verification check.Source: §4.5 · pp. 15–16, Table 4 · p. 16

4.6 A Preliminary Study with Verus

  • In a preliminary Verus study, Clover accepts 32 of 41 examples at k = 1 and 36 of 41 at k = 10.The authors present this as early evidence that Clover can be used with other languages and deductive verification tools.Source: §4.6 · p. 16

5 Related Work

Prior work spans LLM code generation, specification synthesis, self-correction, and verification. Clover differs from closely related Dafny-generation work by emphasizing verification through six consistency checks rather than generation or soundness alone.

5 Related Work

  • Prior code-generation research includes LLM-based generation [14] [16] [38], neural program synthesis [2] [5] [71], task decomposition [73] [5], and execution traces [21] [58].Other work synthesizes programs from specifications [53], studies natural-to-formal translation [27], or predicts invariants with LLMs [39].Source: §5 · pp. 16–17
  • Self-correction approaches include self-consistency [66], self-debugging [15] [56], and self-improvement [41], while one study finds self-debugging limited relative to human-level debugging.Source: §5 · p. 17
  • Verification research includes test-based checking [40], generated assertions [32], generated unit tests [12] [14] [54] [13], learned correctness verification [19] [31] [37] [74], reranking [31] [38] [57] [67], and LLM-assisted bounded model checking [10].Source: §5 · p. 17
  • Clover contrasts with Dafny-generation work [6] [44] by focusing on verification and using six consistency checks rather than generation or soundness alone.The related works use Monte Carlo Tree Search for multi-step annotated Dafny synthesis or explore prompting techniques for Dafny programs.Source: §5 · p. 17

6 Conclusion

Clover reframes code correctness checking as consistency checking among code, docstrings, and formal annotations. Initial GPT-4 experiments report strong acceptance of correct examples, rejection of incorrect examples, and detection of errors in an existing dataset.

6 Conclusion

  • CloverBench yields an 87% acceptance rate for ground-truth examples and a 100% rejection rate for incorrect examples.Source: §6 · p. 18
  • On MBPP-DFY-50 [44], Clover detects 6 incorrect samples and accepts 89% of correct ones.Source: §6 · p. 18
  • Clover introduces a dataset of 60 hand-crafted Dafny examples and reduces correctness checking to the more accessible task of checking consistency.Source: §6 · p. 18
  • The authors identify future work in improving verification tools and LLM capabilities, and scaling evaluation to more challenging examples.The specified capability areas include generating code, annotations, and docstrings, and understanding Dafny and Verus syntax.Source: §6 · p. 18

A.1 An Analytical Model for Clover Reconstruction Tests

The analysis models one directed reconstruction edge, where a transfer model reconstructs one component and a check accepts when the reconstruction is equivalent to the input component. Under alignment and concentration assumptions, the check has a lower bound on accepting consistent pairs and an upper bound on accepting inconsistent pairs; the analysis does not establish corresponding guarantees for the full six-check procedure.

A.1 An Analytical Model for Clover Reconstruction Tests

  • The model assumes semantic equivalence within each domain and a ground-truth consistency relation preserved under equivalent substitutions, with each object consistent with at most one equivalence class in the other domain.The analysis places a distribution D over input pairs and assumes the transfer model is transfer-rational.Source: §A.1 · p. 26
  • The transfer model M assigns each input x a probability distribution over destination outputs, and transfer-rationality requires a unique most-probable equivalence class.The induced transfer function maps x to that maximizing class; in Clover, GPT-4 supplies the transfer model, sometimes combined with Dafny feedback.Source: §A.1 · pp. 26–27
  • The single-edge check samples a reconstruction y′ from M(x, ·) and accepts exactly when y′ is equivalent to y.Equivalence must be checkable in the destination domain.Source: §A.1 · p. 27
  • Consistency alignment assumes the transfer model favors the correct equivalence class with probability c1 near 1 and favors it for inconsistent pairs with probability c0 near 0.Source: §A.1 · p. 27
  • Concentration assumes that with probability at least pc, correct reconstructions receive substantial probability mass l, while incorrect reconstructions assign at most negligible mass u to competing equivalence classes.The stated intuition is that sampling usually follows the model’s most likely equivalence class, with the second-most-likely class much less probable.Source: §A.1 · p. 27
  • For consistent pairs, Theorem 3 lower-bounds acceptance by l · pc · c1; for inconsistent pairs, it upper-bounds acceptance by u · pc · (1 − c0) + (1 − pc)(1 − c0) + c0.These bounds assume consistency alignment and concentration; repeating reconstruction tests can increase the gap between the probabilities.Source: §A.1 · pp. 27–28
  • The analysis simplifies equivalence checking by assuming a perfect checker, although practical equivalence tests can be imprecise.Source: §A.1 · p. 27
  • The theorem analyzes one edge, whereas full Clover combines five reconstruction edges and one verification edge without assuming independence; real GPT-4 and Dafny may violate the model’s assumptions.The authors note that empirical end-to-end results remain promising and that the model guides which reconstruction properties support accuracy.Source: §A.1 · p. 28

A.2 Explaining the Evaluation

The appendix estimates acceptance rates for individual reconstruction edges and the combined checks. Correct ground-truth inputs have a measured aggregate acceptance of 0.75, while several incorrect categories have zero aggregate acceptance despite nonzero rates on individual edges.

A.2 Explaining the Evaluation

  • Table 6 reports empirically measured A and R values for k = 1, with percentages of reconstructed components passing equivalence checks across five categories.Entries are omitted where a category-check pair violates the analytical model’s assumptions.Source: Table 6 · p. 28, §A.2 · pp. 28–29
  • The first-column doc2anno acceptance rate is 0.85, partly because correct generated annotations can fail the annotation equivalence-checking template.The reported discrepancy also includes reconstruction failures.Source: §A.2 · p. 29
  • 0.75 is the measured aggregate acceptance rate for ground-truth inputs, above the 0.59 product expected under independent checks.The authors attribute the difference to dependence: examples passing one edge tend to pass other edges too.Source: §A.2 · p. 29
  • C1, C2, C3, and C6 each have zero overall acceptance, including C1 and C3 where no individual edge has zero acceptance.Docstring equivalence checking detects contradictions well but is less effective for additions or omissions caused by slightly strengthened or weakened annotations.Source: §A.2 · p. 29

A.3 Proof of Theorem 3

The proof bounds acceptance separately for examples inside and outside G, and notes that the incorrect-example construction may inflate measured R.

A.3 Proof of Theorem 3

  • For (x, y) in G, the accept probability is at least l · pc · c1, denoted A.The bound follows from Assumptions 1 and 2 and a perfect equivalence oracle.Source: §A.3 · p. 29
  • For (x, y) outside G, the accept probability is at most c0 + (1 − c0) · pc · u + (1 − c0)(1 − pc).The bound aggregates three cases, including cases where the bounds in Assumption 2 do not hold.Source: §A.3 · p. 29
  • Because incorrect examples were selected only from cases that pass Dafny verification, measured R is likely higher than under a more natural distribution.Source: §A.3 · p. 29

A.4.1 Limitations

The limitations include bounded LLM and specification-generation capabilities, functional-only checking, and cases where shared errors or oracle misalignment evade correction.

A.4.1 Limitations

  • The approach is limited by LLM capabilities and by inherent limitations in generating docstrings, annotations, and code.Source: §A.4.1 · p. 30
  • Annotations specify functionality rather than implementation details, and this first step checks functional correctness rather than implementation performance.For example, an annotation can require a sorted array but cannot easily constrain the sorting algorithm.Source: §A.4.1 · p. 30
  • If the consistency oracle misreads the intended behavior or all three artifacts share an omitted edge case, human intervention is needed to correct the issue.The authors say they have not detected these issues in their experiments and expect oracle misalignment to be rare.Source: §A.4.1 · p. 30
  • The authors expect additional breakthroughs, human-in-the-loop steps, or both may be needed to achieve Clover’s eventual vision.Source: §A.4.1 · p. 30

A.4.2 Clover Variants

This section discusses Clover’s variants and limitations, with examples and reports on Dafny-task performance, incorrect ground-truth programs, checker outcomes, and ablation configurations.

A.4.2 Clover Variants

  • Clover could check code against docstrings, but docstrings alone are too imprecise to ensure implementation correctness.Unit tests may offer quick sanity checks, but can be harder to generate, opaque, and less robust than annotations for assuring correctness.Source: §A.4.2 · p. 30

A.4.3 Future Research

  • Clover’s verification cannot compensate for poor generation, and improvements are needed in docstring, annotation, and code equivalence checking.The authors identify solver improvements, fuzzing, concolic testing, and formal equivalence checking as possible approaches.Source: §A.4.3 · p. 31

A.4.4 Data Contamination

  • CloverBench’s textbook-level, hand-crafted examples may still face indirect training-data contamination, which generic function names were used to mitigate.The authors plan more sophisticated examples; GPT-4 sometimes produces correct code from incomplete specifications, and descriptive signatures may reveal behavior.Source: §A.4.4 · p. 31

A.4.5 Reasons for Reconstruction Failure using GPT-4

  • GPT-4 often misses Dafny 4.0.0 memory-access clauses, but compiler errors can help it add them; it also retains deprecated syntax conventions.The authors suggest training or fine-tuning on Dafny 4.0.0 could improve acceptance.Source: §A.4.5 · p. 31, §A.6 · p. 32

A.5 Open Model Results

  • CodeLlama-34b is incapable of handling Dafny code and verification logic, highlighting open models’ knowledge-coverage gap on low-resource languages.The authors contrast this with GPT-4’s potential for verification tasks.Source: §A.5 · pp. 31–32, Table 7 · p. 32

A.7 Supplimentary Template and Examples

  • The annotation-equivalence template uses Dafny verification to check whether generated and original preconditions and postconditions are equivalent, while input/output tests compare program outputs.The template is sound but incomplete: Dafny may fail to prove genuinely equivalent predicates.Source: §A.7 · pp. 32–33, §A.8 · p. 35

A.9 Wrong Ground-Truth programs in MBPP-DFY-50 [44]

  • Clover identified MBPP-DFY-50 inconsistencies including array-length requirements that contradict docstrings and annotations that omit behavior for false returns.Examples include tasks 472, 567, and 632, plus task 576’s missing false-return condition.Source: §A.9 · pp. 38–40
  • Tasks 644 and 803 expose MBPP-DFY-50 ground-truth mismatches: an incorrect k lower bound and a false-case perfect-square postcondition made tautological by unnecessary bounds.Task 644’s docstring allows k from 0 to the array length, but its annotation requires k ≥ 2; Task 803’s annotation adds bounds that make its false-case postcondition tautological.Source: §A.9 · pp. 42–43

A.10 More Detailed Experiment Results

  • The appendix also presents code-generation ablations across verifier-feedback, compiler-only, docstring, and Claude configurations, plus an annotation-generation ablation from pure code.The code-generation table compares the named configurations; the annotation-generation table counts loop invariants and defines acceptance as annotation equivalence plus sufficient invariants for Dafny verification.Source: Table 13 · p. 49, Table 14 · p. 50
  • All examples are rejected in the reported C1 and C6 checks at k=1 and k=10.The C1 results are identified in Tables 15–16, and the C6 results in Tables 21–22.Source: Table 15 · p. 51, Table 16 · p. 52, Table 21 · p. 57
  • The per-example C2 and C3 tables likewise report all examples rejected at k=1 and k=10.The tables show directed-edge outcomes for individual examples; an example is accepted only if all its edges are accepted.Source: §A.10 · pp. 53–56
Loading 2310.17807v4…