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 any number of undesirable outcomes. In this paper, we lay out a vision for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which reduces correctness checking to the more accessible problem of consistency checking. At the core of Clover lies a checker that 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 feasibility 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 incorrect ones (no false positives).

翻译：大语言模型在代码生成领域的应用是软件开发中快速增长的趋势。然而，若缺乏确保生成代码正确性的有效方法，这一趋势可能导致各种不良后果。本文提出了应对该挑战的愿景：Clover范式，即"闭环可验证代码生成"（Closed-Loop Verifiable Code Generation）的缩写，其将正确性校验简化为更易处理的一致性校验问题。Clover的核心在于一个执行代码、文档字符串与形式化标注之间一致性校验的检查器。该检查器通过形式化验证工具与大语言模型的新型集成实现。我们提供了理论分析以支持"Clover在一致性校验中应具备有效性"的论点，并基于手工设计的基准数据集CloverBench（包含教科书级难度的带标注Dafny程序）进行了实证可行性研究。实验结果表明：（i）大语言模型在自动生成形式化规约方面表现出合理成功率；（ii）即便对错误实例保持零容忍（无假阳性），我们的一致性校验器对正确实例的接受率仍可达87%。