Clover: Closed-Loop Verifiable Code Generation

要約

コード生成に大規模な言語モデルを使用する傾向は、ソフトウェア開発において急速に高まっている。しかし、生成されたコードの正しさを保証する効果的な方法がなければ、この傾向は望ましくない結果を招く可能性がある。本論文では、この課題に対処するためのビジョンとして、Cloverパラダイム（Closed-Loop Verifiable Code Generationの略）を提示する。Cloverの核となるのは、コード、ドキュメント、形式的注釈の一貫性チェックを行うチェッカーである。このチェッカーは、形式検証ツールと大規模言語モデルの新しい統合を用いて実装されている。我々は、Cloverが一貫性チェックに有効であるという我々の論文を支持する理論的分析を提供する。また、教科書的な難易度の注釈付きDafnyプログラムを含む、手作業で設計されたデータセット（CloverBench）を用いて、その実現可能性を実証的に調査する。実験結果は、このデータセットにおいて、(i)LLMは形式仕様の自動生成にそこそこ成功していること、(ii)我々の一貫性検査器は、正しくないインスタンスに対する許容度をゼロ（誤検出なし）に維持しながら、正しいインスタンスに対する有望な受理率（最大87％）を達成していることを示している。

要約(オリジナル)

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).

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL