📄 Clover: Closed-Loop Verifiable Code Generation

Paper · 2024 · Chuyue Sun, Ying Sheng, Oded Padon et al.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

🏛️ Institutions

🎓Stanford UniversityStanford · United States567 works · 335,190 citations🏢VMwarePalo Alto · United States3 works · 56 citations

🧭 Fields, topics and concepts

Cite

Cite as Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. arXiv:2310.17807.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2310.17807 · arXiv 2310.17807

@misc{sun2024clover,
  title = {{Clover: Closed-Loop Verifiable Code Generation}},
  author = {Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett},
  year = {2024},
  doi = {10.48550/arxiv.2310.17807},
  eprint = {2310.17807},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.17807}
}

References

75 references, 26 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Rajeev Alur et al. “Syntax-guided synthesis”. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 2013, pp. 1–8. url: https://ieeexplore.ieee.org/document/6679385/. ↗
2. Jacob Austin et al. “Program Synthesis with Large Language Models”. In: CoRR abs/2108.07732 (2021). arXiv: 2108.07732. url: https://arxiv.org/abs/2108.07732. ↗
3. John Barnes. SPARK: The Proven Approach to High Integrity Software. Altran Praxis, 2012. find
4. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability. Vol. 185. IOS press, 2009. find
5. Matthew Bowers et al. “Top-Down Synthesis for Library Learning”. In: Proc. ACM Program. Lang. 7.POPL (2023), pp. 1182–1213. doi: 10.1145/3571234. url: https://doi.org/10.1145/3571234. ↗
6. David Brandfonbrener et al. “Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search”. In: arXiv preprint arXiv:2402.08147 (2024). — [arXiv:2402.08147](https://arxiv.org/abs/2402.08147) find
7. Sébastien Bubeck et al. “Sparks of artificial general intelligence: Early experiments with gpt-4”. In: arXiv preprint arXiv:2303.12712 (2023).
8. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. “KLEE: Unassisted 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.… find
9. Cristian Cadar and Koushik Sen. “Symbolic execution for software testing: three decades later”. In: Commun. ACM 56.2 (2013), pp. 82–90. doi: 10.1145/2408776.2408795. url: https://doi.org/10.1145/2408776.2408795. — [doi:10.1145/2408776.2408795](https://doi.org/10.1145/2408776.2408795) ↗
10. Yiannis Charalambous et al. “A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification”. In: CoRR abs/2305.14752 (2023). doi: 10 . 48550 / arXiv . 2305 . 14752. arXiv: 2305.14752. url: https://doi.org/10.48550/arXiv.2305.14752. — [doi:10.48550/arxiv.2305.14752](https://doi.org/10.48550/arxiv.2305.14752) ↗
11. Swarat Chaudhuri et al. “Neurosymbolic Programming”. In: Found. Trends Program. Lang. 7.3 (2021), pp. 158–243. doi: 10.1561/2500000049. url: https://doi.org/10.1561/2500000049. — [doi:10.1561/2500000049](https://doi.org/10.1561/2500000049) ↗
12. 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. ↗
13. Bei Chen et al. “Codet: Code generation with generated tests”. In: arXiv preprint arXiv:2207.10397 (2022). Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett find
14. Mark Chen et al. “Evaluating Large Language Models Trained on Code”. In: CoRR abs/2107.03374 (2021). arXiv: 2107 . 03374. url: https://arxiv.org/abs/2107.03374. ↗
15. Xinyun Chen et al. “Teaching large language models to self-debug”. In: arXiv preprint arXiv:2304.05128 (2023). find
16. Zhoujun Cheng et al. “Binding Language Models in Symbolic Languages”. 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=lH1PV42cbF. ↗
17. Aakanksha Chowdhery et al. “PaLM: Scaling Language Modeling with Pathways”. In: CoRR abs/2204.02311 (2022). doi: 10 . 48550 / arXiv . 2204 . 02311. arXiv: 2204 . 02311. url: https://doi.org/10 . 48550 / arXiv.2204.02311.
18. Berkeley R. Churchill et al. “Semantic program alignment for equivalence checking”. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. Ed. by Kathryn S. McKinley and Kathleen Fisher. ACM, 2019, pp. 1027… — [doi:10.1145/3314221.3314596](https://doi.org/10.1145/3314221.3314596) find
19. Karl Cobbe et al. “Training Verifiers to Solve Math Word Problems”. In: CoRR abs/2110.14168 (2021). arXiv: 2110.14168. url: https://arxiv.org/abs/2110.14168. ↗
20. Domenico Cotroneo et al. “Vulnerabilities in AI Code Generators: Exploring Targeted Data Poisoning Attacks”. In: CoRR abs/2308.04451 (2023). doi: 10 . 48550 / arXiv . 2308 . 04451. arXiv: 2308 . 04451. url: https : //doi.org/10.48550/arXiv.2308.04451. — [doi:10.48550/arxiv.2308.04451](https://doi.org/10.48550/arxiv.2308.04451) find
21. Yangruibo Ding et al. “TRACED: Execution-aware Pre-training for Source Code”. In: arXiv preprint arXiv:2306.07487 (2023). — [arXiv:2306.07487](https://arxiv.org/abs/2306.07487) find
22. Kevin Ellis et al. “DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning”. In: PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. Ed. by Stephen N. Freund and Eran Yahav. AC… — [doi:10.1145/3453483.3454080](https://doi.org/10.1145/3453483.3454080) find
23. Robert W. Floyd. “Assigning Meanings to Programs”. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967, pp. 19–32. find
24. Sayontan Ghosh et al. “SpecNFS: A Challenge Dataset Towards Extracting Formal Models from Natural Language Specifications”. In: Proceedings of the Thirteenth Language Resources and Evaluation Conference, LREC 2022, Marseille, France, 20-25 June 2022. Ed. by Nicoletta Calzolari et al. European Langua… find
25. Github Copilot. Github Copilot: Your AI Pair Programmer. https://github.com/features/copilot. Clover: Closed-Loop Verifiable Code Generation ↗
26. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. “Program Synthesis”. In: Found. Trends Program. Lang. 4.1-2 (2017), pp. 1–119. doi: 10.1561/2500000010. url: https://doi.org/10.1561/2500000010. ↗
27. Christopher Hahn et al. “Formal Specifications from Natural Language”. In: CoRR abs/2206.01962 (2022). doi: 10 . 48550 / arXiv . 2206 . 01962. arXiv: 2206 . 01962. url: https://doi.org/10 . 48550 / arXiv. 2206 . 01962. — [arXiv:2206.01962](https://arxiv.org/abs/2206.01962) find
28. James Hendler. “Understanding the limits of AI coding”. In: Science 379.6632 (2023), pp. 548–548. find
29. 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 Yeung. 2021. url: https://datas…
30. C. A. R. Hoare. “An Axiomatic Basis for Computer Programming”. In: Commun. ACM 12.10 (1969), pp. 576–580. doi: 10.1145/363235.363259. url: http://doi.acm.org/10.1145/363235.363259. — [doi:10.1145/363235.363259](https://doi.org/10.1145/363235.363259) ↗
31. Jeevana Priya Inala et al. “Fault-Aware Neural Code Rankers”. In: NeurIPS. 2022. url: http://papers.nips.cc/paper%5C_files/paper/2022/hash/5762c579d09811b7639be2389b3d07be-Abstract-Conference.html. ↗
32. Darren Key, Wen-Ding Li, and Kevin Ellis. “I Speak, You Verify: Toward Trustworthy Neural Program Synthesis”. In: CoRR abs/2210.00848 (2022). doi: 10 . 48550 / arXiv . 2210 . 00848. arXiv: 2210 . 00848. url: https://doi.org/10.48550/arXiv.2210.00848. — [doi:10.48550/arxiv.2210.00848](https://doi.org/10.48550/arxiv.2210.00848) ↗
33. James C. King. “Symbolic Execution and Program Testing”. In: Commun. ACM 19.7 (1976), pp. 385–394. doi: 10.1145/360248.360252. url: https://doi.org/10.1145/360248.360252. — [doi:10.1145/360248.360252](https://doi.org/10.1145/360248.360252) ↗
34. Yuhang Lai et al. “DS-1000: A Natural and Reliable Benchmark for Data Science 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. Proceedings of Machine Learning Research. PMLR, 2023, pp. 18319–… find
35. Andrea Lattuada et al. Verus: Verifying Rust Programs using Linear Ghost Types (extended version). 2023. arXiv: 2303.05491 [cs.LO]. find
36. K Rustan M Leino. “Dafny: An automatic program verifier for functional correctness”. In: International conference on logic for programming artificial intelligence and reasoning. Springer. 2010, pp. 348–370. find
37. Yifei Li et al. “On the Advance of Making Language Models Better Reasoners”. In: CoRR abs/2206.02336 (2022). doi: 10.48550/arXiv.2206.02336. arXiv: 2206.02336. url: https://doi.org/10.48550/arXiv.2206.02336. Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett — [doi:10.48550/arxiv.2206.02336](https://doi.org/10.48550/arxiv.2206.02336) ↗
38. Yujia Li et al. “Competition-level code generation with alphacode”. In: Science 378.6624 (2022), pp. 1092–1097.
39. Chang Liu et al. “Towards General Loop Invariant Generation via Coordinating Symbolic Execution and Large Language Models”. In: arXiv preprint arXiv:2311.10483 (2023). — [arXiv:2311.10483](https://arxiv.org/abs/2311.10483) find
40. Jiawei Liu et al. “Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation”. In: CoRR abs/2305.01210 (2023). doi: 10.48550/arXiv.2305.01210. arXiv: 2305.01210. url: https://doi.org/10.48550/arXiv.2305.01210. ↗
41. Aman Madaan et al. “Self-refine: Iterative refinement with self-feedback”. In: Advances in Neural Information Processing Systems 36 (2024). find
42. Zohar Manna and Richard Waldinger. “Knowledge and reasoning in program synthesis”. In: Artificial intelligence 6.2 (1975), pp. 175–208. find
43. Zohar Manna and Richard J Waldinger. “Toward automatic program synthesis”. In: Communications of the ACM 14.3 (1971), pp. 151–165. find
44. Md Rakib Hossain Misu et al. “Towards AI-Assisted Synthesis of Verified Dafny Methods”. In: arXiv preprint arXiv:2402.00247 (2024).
45. Nausheen Mohammed et al. “Enabling Memory Safety of C Programs using LLMs”. In: arXiv preprint arXiv:2404.01096 (2024). — [arXiv:2404.01096](https://arxiv.org/abs/2404.01096) find
46. Rajdeep Mondal et al. “What do LLMs need to Synthesize Correct Router Configurations?” In: Proceedings of the 22nd ACM Workshop on Hot Topics in Networks. 2023, pp. 189–195. find
47. Theo X Olausson et al. “Is Self-Repair a Silver Bullet for Code Generation?” In: The Twelfth International Conference on Learning Representations. 2023.
48. OpenAI. “GPT-4 Technical Report”. In: CoRR abs/2303.08774 (2023). doi: 10 . 48550 / arXiv . 2303 . 08774. arXiv: 2303 . 08774. url: https : //doi.org/10.48550/arXiv.2303.08774.
49. Liangming Pan et al. “Automatically correcting large language models: Surveying the landscape of diverse self-correction strategies”. In: arXiv preprint arXiv:2308.03188 (2023). find
50. Hammond Pearce et al. “Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions”. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 2022, pp. 754–768. doi: 10.1109/SP46214.2022.9833571. url: https://doi.org/10.1109/S… — [doi:10.1109/sp46214.2022.9833571](https://doi.org/10.1109/sp46214.2022.9833571) find
51. 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:… find
52. Neil Perry et al. “Do Users Write More Insecure Code with AI Assistants?” In: CoRR abs/2211.03622 (2022). doi: 10 . 48550 / arXiv . 2211 . 03622. Clover: Closed-Loop Verifiable Code Generation arXiv: 2211 . 03622. url: https://doi.org/10 . 48550 / arXiv. 2211 . 03622. — [arXiv:2211.03622](https://arxiv.org/abs/2211.03622) find
53. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. “Program synthesis from polymorphic refinement types”. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. Ed. by Chandra Krintz and Emery D… find
54. Gabriel Ryan et al. “Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM”. In: arXiv preprint arXiv:2402.00097 (2024). — [arXiv:2402.00097](https://arxiv.org/abs/2402.00097) find
55. Gustavo Sandoval et al. “Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants”. In: 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023. Ed. by Joseph A. Calandrino and Carmela Troncoso. USENIX Association, 2023. url: http… find
56. William Saunders et al. “Self-critiquing models for assisting human evaluators”. In: arXiv preprint arXiv:2206.05802 (2022).
57. 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. Ed. by Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang. Association fo…
58. Kensen Shi et al. “CrossBeam: Learning to Search in Bottom-Up Program Synthesis”. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. url: https://openreview.net/forum?id=qhC8mr2LEKq. ↗
59. Armando Solar-Lezama. Program synthesis by sketching. University of California, Berkeley, 2008.
60. Chuyue Sun, Christopher Hahn, and Caroline Trippel. “Towards Improving Verification Productivity with Circuit-Aware Translation of Natural Language to SystemVerilog Assertions”. In: First International Workshop on Deep Learning-aided Verification. 2023. find
61. Chuyue Sun et al. “Clover: Closed-Loop Verifiable Code Generation”. Version v2. In: (2024). arXiv: 2310.17807v2 [cs.AI]. — [arXiv:2310.17807](https://arxiv.org/abs/2310.17807)
62. Maxim Tabachnyk and Stoyan Nikolov. ML-Enhanced Code Completion Improves Developer Productivity. Blog. Accessed: 2022-07-26. 2022. url: https://blog.research . google / 2022 / 07 / ml - enhanced - code - completion-improves.html. ↗
63. Abhishek Udupa et al. “TRANSIT: specifying protocols with concolic snippets”. In: ACM SIGPLAN Conference on Programming Language Design Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013. Ed. by Hans-Juergen Boehm and Cormac Flanagan. A… find
64. Priyan Vaithilingam, Tianyi Zhang, and Elena L. Glassman. “Expectation vs. Experience: Evaluating the Usability of Code Generation Tools Powered by Large Language Models”. In: CHI ’22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Extended Ab… — [doi:10.1145/3491101.3519665](https://doi.org/10.1145/3491101.3519665) find
65. Richard J Waldinger and Richard CT Lee. “PROW: A step toward automatic program writing”. In: Proceedings of the 1st international joint conference on Artificial intelligence. 1969, pp. 241–252. find
66. Xuezhi Wang et al. “Self-consistency improves chain of thought reasoning in language models”. In: arXiv preprint arXiv:2203.11171 (2022).
67. Jason Wei et al. “Chain-of-Thought Prompting Elicits Reasoning in Large Language Models”. In: NeurIPS. 2022. url: http://papers.nips.cc/paper%5C_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html. ↗
68. Cheng Wen et al. “Enchanting program specification synthesis by large language models using static analysis and program verification”. In: arXiv preprint arXiv:2404.00762 (2024). — [arXiv:2404.00762](https://arxiv.org/abs/2404.00762) find
69. Haoze Wu, Clark Barrett, and Nina Narodytska. Lemur: Integrating Large Language Models in Automated Program Verification. 2023. arXiv: 2310. 04870 [cs.FL].
70. Frank F. Xu, Bogdan Vasilescu, and Graham Neubig. “In-IDE Code Generation from Natural Language: Promise and Challenges”. In: ACM Trans. Softw. Eng. Methodol. 31.2 (2022), 29:1–29:47. doi: 10 . 1145 / 3487569. url: https://doi.org/10.1145/3487569. ↗
71. Pengcheng Yin and Graham Neubig. “A Syntactic Neural Model for General-Purpose Code Generation”. In: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, Vancouver, Canada, July 30 - August 4, Volume 1: Long Papers. Ed. by Regina Barzilay and Min-Yen Kan…
72. Pengcheng Yin et al. “Natural Language to Code Generation in Interactive Data Science Notebooks”. In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023. Ed. by Anna Rogers, Jordan L. Boyd-Graber…
73. Eric Zelikman et al. “Parsel: A (de-) compositional framework for algorithmic reasoning with language models”. In: arXiv preprint arXiv:2212.10561 (2023).
74. 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. Proceedings of Machine Learning Research. PMLR, 2023, pp. 41832–41846. url: https://proceedi…
75. Baishun Zhou and Gangyi Ding. “Survey of intelligent program synthesis techniques”. In: International Conference on Algorithms, High Performance Computing, and Artificial Intelligence (AHPCAI 2023). Ed. by Sandeep Saxena and Cairong Zhao. Vol. 12941. International Society for Optics and Photonics. S… — [doi:10.1117/12.3011627](https://doi.org/10.1117/12.3011627) find

Updated 3 November 2026

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/sun-2024-clover-closed-loop-verifiable-code/