CoChat
Sign Up
Cited by 43Logic, programming, and type systemsSoftware Engineering ResearchSoftware Testing and Debugging Techniques

Clover: Closed-Loop Verifiable Code Generation

Open access
Sun, Chuyue, Sheng, Ying, Padon, Oded, Barrett, Clark·2024·Lecture Notes in Computer Science
DOI 10.1007/978-3-031-65112-0_7
Open this paper in CoChat — free accountOpen PDF

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1007/978-3-031-65112-0_7

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Iteratively refining LLM outputs with formal verification can substantially improve their reasoning quality.

    “Recent studies have shown that iteratively refining LLM outputs with formal verification can substantially improve their reasoning quality [10], [11].”

    From ADVENT: LLM-Driven Automatic Predicate Invention for ILP (2026) · cites this paper as [10]

    Section 4.2 (Generation Phase; page unavailable) reports that GPT-4 generated correct Dafny code most successfully when given multiple tries and feedback from the Dafny compiler and verifier. This supports iterative improvement in code-generation correctness, but the paper does not establish a substantial improvement in LLM reasoning quality generally. (LLM, conf=0.88)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

No citation lists for this paper

No citation lists for this paper yet — checked again daily.

References 51 · Cited by 43

Research works printed but not linked: 21

  1. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfia- bility. Vol. 185. IOS press, 2009.
  2. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. "KLEE: Unas- sisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs". In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. Ed. by Richard Draves and Robbert van Re- nesse. USENIX Association, 2008, pp. 209-224. url: http://www.usenix. org/events/osdi08/tech/full%5C_papers/cadar/cadar.pdf.
  3. Bei Chen et al. "CodeT: Code Generation with Generated Tests". In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. url: https:// openreview.net/pdf?id=ktrw68Cmu9c.
  4. Berkeley R. Churchill et al. "Semantic program alignment for equivalence checking". In: Proceedings of the 40th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019.
  5. Kevin Ellis et al. "DreamCoder: bootstrapping inductive program synthe- sis with wake-sleep library learning". In: PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Imple- mentation, Virtual Event, Canada, June 20-25, 2021.
  6. Robert W. Floyd. "Assigning Meanings to Programs". In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathe- matics. American Mathematical Society, 1967, pp. 19-32.
  7. Ed. by Nicoletta Calzolari et al. European Language Resources Association, 2022, pp. 2166-2176. url: https://aclanthology.org/2022.lrec-1.233.
  8. James Hendler. "Understanding the limits of AI coding". In: Science 379.6632 (2023), pp. 548-548.
  9. Dan Hendrycks et al. "Measuring Coding Challenge Competence With APPS". In: Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual. Ed. by Joaquin Vanschoren and Sai-Kit Ye- ung. 2021. url: https://datasets-benchmarks-proceedings.neurips. cc/paper/2021/hash/c24cd76e1ce41366a4bbe8a49b02a028-Abstract- round2.html.
  10. Yuhang Lai et al. "DS-1000: A Natural and Reliable Benchmark for Data Science Code Generation". In: International Conference on Machine Learn- ing, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 18319-18345. url: https://proceedings.mlr.press/v202/ lai23b.html.
  11. Kexin Pei et al. "Can Large Language Models Reason about Program Invariants?" In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Proceedings of Machine Learning Research. PMLR, 2023, pp. 27496-27520. url: https://proceedings.mlr.press/v202/pei23a. html.
  12. Ed. by Chandra Krintz and Emery D. Berger. ACM, 2016, pp. 522-538. doi: 10 . 1145 / 2908080 . 2908093. url: https : / / doi . org / 10 . 1145 / 2908080.2908093. · DOI
  13. Ed. by Joseph A. Calandrino and Carmela Troncoso. USENIX Association, 2023. url: https://www.usenix.org/conference/usenixsecurity23/ presentation/sandoval.
  14. Freda Shi et al. "Natural Language to Code Translation with Execution". In: Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022.
  15. Kensen Shi et al. "CrossBeam: Learning to Search in Bottom-Up Program Synthesis". In: The Tenth International Conference on Learning Represen- tations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. url: https://openreview.net/forum?id=qhC8mr2LEKq.
  16. Chuyue Sun, Christopher Hahn, and Caroline Trippel. "Towards Improv- ing Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions". In: First International Workshop on Deep Learning-aided Verification. 2023.
  17. Ed. by Hans-Juergen Boehm and Cormac Flanagan. ACM, 2013, pp. 287-296. doi: 10 . 1145 / 2491956 . 2462174. url: https : / / doi . org / 10 . 1145 / 2491956.2462174. · DOI
  18. Richard J Waldinger and Richard CT Lee. "PROW: A step toward au- tomatic program writing". In: Proceedings of the 1st international joint conference on Artificial intelligence. 1969, pp. 241-252.
  19. Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating Large Language Models in Automated Program Verification. 2023. arXiv: 2310. 04870 [cs.FL].
  20. Ed. by Anna Rogers, Jor- dan L. Boyd-Graber, and Naoaki Okazaki. Association for Computational Linguistics, 2023, pp. 126-173. doi: 10 . 18653 / v1 / 2023 . acl -long . 9. url: https://doi.org/10.18653/v1/2023.acl-long.9. · DOI
  21. Tianyi Zhang et al. "Coder Reviewer Reranking for Code Generation". In: International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA. Ed. by Andreas Krause et al. Vol. 202. Pro- ceedings of Machine Learning Research. PMLR, 2023, pp. 41832-41846. url: https://proceedings.mlr.press/v202/zhang23av.html.

Authors
Sun, C., Sheng, Y., Padon, O., & Barrett, C.
Affiliations
  • Stanford University (US)
  • VMware (United States) (US)
Corresponding author
Sun, Chuyue
ORCID
Venue
Lecture Notes in Computer Science
Publisher
Springer Nature Switzerland
Published
2024
Pages
134-155
ISSN
  • 0302-9743 (ISSN-L)
  • 1611-3349
DOI
10.1007/978-3-031-65112-0_7
OpenAlex
W4400675892
Cited by
43
References
51
Citations by year
2026: 16 · 2025: 22 · 2024: 5
FWCI
12.71
Type
conference paper
Language
en
Open access
Licence
Locations
  • Lecture notes in computer science (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
large language models, code generation, consistency checking, formal verification, Dafny, formal specification, docstrings, program correctness

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review