盡管近年來(lái)大型語(yǔ)言模型（LLM）在代碼生成方面取得了驚人的成功，但這種由人工智能生成的代碼的可信性仍然是一個(gè)問題。為了解決這個(gè)問題，研究人員提出了Clover模式，即閉環(huán)可驗(yàn)證代碼生成，通過檢查代碼、文檔字符串和注釋之間的一致性，強(qiáng)制執(zhí)行AI生成的代碼的正確性。

在軟件開發(fā)中，利用大型語(yǔ)言模型（LLM）進(jìn)行代碼生成是一個(gè)快速發(fā)展的趨勢(shì)。然而，如果沒有有效的方法來(lái)確保AI生成的代碼的正確性，這一趨勢(shì)可能導(dǎo)致不可取的結(jié)果。在這項(xiàng)工作中，研究人員引入了一種名為Clover的模式，即閉環(huán)可驗(yàn)證代碼生成，以解決這一挑戰(zhàn)。Clover將正確性檢查降低到更容易解決的一致性檢查問題，并保護(hù)LLM驅(qū)動(dòng)的代碼生成免受可能造成昂貴錯(cuò)誤的影響。

Clover的核心是一個(gè)檢查器，它在代碼、文檔字符串和形式注釋之間執(zhí)行一致性檢查。該檢查器使用形式驗(yàn)證工具和大型語(yǔ)言模型的新穎集成實(shí)現(xiàn)。研究人員通過實(shí)證研究在一個(gè)手工設(shè)計(jì)的數(shù)據(jù)集（CloverBench）上驗(yàn)證了其可行性，該數(shù)據(jù)集包含在教科書水平的帶注釋語(yǔ)言中的注釋程序。實(shí)驗(yàn)結(jié)果表明，對(duì)于該數(shù)據(jù)集，（i）LLM在自動(dòng)生成形式規(guī)范方面取得了合理的成功；（ii）一致性檢查器在正確實(shí)例上實(shí)現(xiàn)了一個(gè)有希望的接受率（高達(dá)87%），同時(shí)對(duì)于錯(cuò)誤實(shí)例保持零容忍（沒有誤報(bào)）。

正式驗(yàn)證和人工智能是一對(duì)良好的搭檔

大語(yǔ)言模型（LLM）最近展示了令人矚目的能力。它們可以進(jìn)行對(duì)話、檢索和總結(jié)大量信息、生成和解釋文本和代碼等等。在眾多可能的應(yīng)用中，它們基于自然語(yǔ)言描述合成代碼的能力令人驚嘆，有可能極大地提高程序員的生產(chǎn)效率。

然而，在實(shí)現(xiàn)這一未來(lái)之前，必須克服一個(gè)根本性的挑戰(zhàn)。目前還沒有一種可靠的方法來(lái)確保AI生成的代碼的正確性。目前對(duì)于AI生成的產(chǎn)物的最佳實(shí)踐是讓人參與其中，例如Copilot。雖然這比沒有人工參與要好，但人工監(jiān)督是昂貴且效率低下的，長(zhǎng)期來(lái)看難以擴(kuò)展。

可以預(yù)見，在未來(lái)幾年中，策劃AI生成內(nèi)容的質(zhì)量將成為最關(guān)鍵的研究問題之一。首先，生成的代碼必須在功能上是正確和可靠的。代碼中的錯(cuò)誤或漏洞可能導(dǎo)致軟件故障，尤其是在醫(yī)療軟件、金融系統(tǒng)或自動(dòng)駕駛車輛等關(guān)鍵系統(tǒng)中，這可能具有成本高昂、危險(xiǎn)或兩者兼而有之的后果。此外，如果生成的代碼不可信，可能會(huì)在軟件中無(wú)意中引入安全漏洞。這可能被惡意實(shí)體利用，導(dǎo)致數(shù)據(jù)泄露、侵犯隱私和其他安全事件。幸運(yùn)的是，在代碼生成的特定情況下，正式驗(yàn)證可以對(duì)任意代碼的質(zhì)量和正確性提供數(shù)學(xué)上嚴(yán)格的保證。如果有一種方法可以自動(dòng)將正式驗(yàn)證應(yīng)用于生成的代碼，這不僅提供了可擴(kuò)展的解決方案，還有可能為AI生成的代碼比人工編寫的代碼更可靠的未來(lái)鋪平道路。

目前，正式驗(yàn)證只能依靠人類專業(yè)知識(shí)實(shí)現(xiàn)。本研究的主要假設(shè)是，LLM能夠生成所需的附屬信息，以幫助正式驗(yàn)證成功，同時(shí)不損害正式方法提供的形式保證。

目前，正式驗(yàn)證只能在耗時(shí)的人類專業(yè)知識(shí)的幫助下實(shí)現(xiàn)。在典型的正式驗(yàn)證過程中，構(gòu)建系統(tǒng)的數(shù)學(xué)模型后，人類專家提供了系統(tǒng)的正式規(guī)范（見清單1），該模型滿足規(guī)范。對(duì)于代碼，已經(jīng)存在一些工具（例如Dafny），可以證明某個(gè)輸入規(guī)范滿足某個(gè)輸入代碼。傳統(tǒng)上，需要大量的人類專業(yè)知識(shí)來(lái)創(chuàng)建正式規(guī)范，并確保規(guī)范在內(nèi)部一致且準(zhǔn)確捕捉到預(yù)期的功能。

基于基于AI的代碼生成技術(shù)的輸出應(yīng)該包括代碼、正式規(guī)范和自然語(yǔ)言文檔字符串。然后，可以使用形式工具與生成的AI技術(shù)相結(jié)合，確保它們是一致的。這種方法被稱為Clover，即閉環(huán)可驗(yàn)證代碼生成。

Clover模式包括兩個(gè)階段。在第一階段（生成階段），創(chuàng)建帶有正式規(guī)范（注釋）和自然語(yǔ)言文檔字符串（文檔字符串）的代碼。在第二階段（驗(yàn)證階段），對(duì)代碼、注釋和文檔字符串進(jìn)行了六個(gè)一致性檢查。如果一致性檢查通過，則表示（i）代碼在功能上與其注釋一致；（ii）注釋完整地捕捉了代碼的功能；（iii）文檔字符串也準(zhǔn)確地反映了代碼的功能（見圖1）。

這個(gè)想法是可以利用越來(lái)越強(qiáng)大的生成式AI技術(shù)在生成階段，然后使用驗(yàn)證階段作為一個(gè)強(qiáng)大的過濾器，只批準(zhǔn)經(jīng)過形式驗(yàn)證、文檔準(zhǔn)確、內(nèi)部一致的代碼。

Dafny

Dafny是評(píng)估中使用的編程語(yǔ)言。Dafny的后端包括一個(gè)編譯器，能夠生成可運(yùn)行的二進(jìn)制文件，以及一個(gè)驗(yàn)證器，可以形式化地檢查代碼是否符合其規(guī)范。清單1列出了一個(gè)用于找到自然數(shù)平方根的Dafny函數(shù)，包括三個(gè)組成部分（文檔字符串、注釋和代碼）。

Clover 第一階段：生成

研究人員首先展示了 Clover 中生成階段可以生成帶有注釋和文檔字符串的代碼。具體而言，研究人員使用 OpenAI 的 GPT-4 進(jìn)行實(shí)驗(yàn)。圖2a展示了在不同條件下，當(dāng) GPT-4 被要求為 CloverBench 中的每個(gè)例子生成代碼時(shí)的結(jié)果。第一個(gè)柱狀圖（"one try"）顯示了單次嘗試的結(jié)果。下一個(gè)柱狀圖允許 GPT-4 嘗試三次，每次提供 Dafny 編譯器和驗(yàn)證器的輸出作為反饋。第三個(gè)柱狀圖類似，但只使用了 Dafny 編譯器的輸出。在最后一個(gè)柱狀圖中，允許三次嘗試，并且還提供了文檔字符串。圖2b展示了當(dāng)提供代碼時(shí)，要求 GPT-4 生成注釋的結(jié)果。雖然不是完美的，但 GPT-4 在大多數(shù)程序中可以生成正確的注釋。這表明使用 LLM 進(jìn)行規(guī)范生成是可行的。

Clover 第二階段：驗(yàn)證

Clover 期望生成階段的輸出包含三個(gè)組成部分：代碼、注釋和文檔字符串。它還期望每個(gè)組成部分提供足夠的細(xì)節(jié)，以明確確定在任何給定輸入上運(yùn)行代碼的唯一結(jié)果。驗(yàn)證階段檢查每對(duì)組成部分的一致性，如圖1所示，只有當(dāng)所有檢查都通過時(shí)才會(huì)成功。

具體而言，總共有六個(gè)檢查：

• （1）anno-sound：一種演繹驗(yàn)證工具（評(píng)估使用 Dafny）檢查代碼是否滿足注釋。
• （2）anno-complete：根據(jù)注釋，使用 LLM 生成新的代碼，然后檢查生成的代碼與原始代碼的等價(jià)性。
• （3）anno2doc：要求 LLM 根據(jù)注釋生成新的文檔字符串，然后使用 LLM 檢查新的文檔字符串與原始文檔字符串的語(yǔ)義等價(jià)性。
• （4）doc2anno：要求 LLM 根據(jù)文檔字符串生成新的注釋，然后使用形式工具檢查新的注釋與原始注釋的邏輯等價(jià)性。
• （5）code2doc：要求 LLM 根據(jù)代碼生成新的文檔字符串，然后檢查新的文檔字符串與原始文檔字符串的語(yǔ)義等價(jià)性。
• （6）doc2code：要求 LLM 根據(jù)文檔字符串生成代碼，然后檢查新的代碼與原始代碼的功能等價(jià)性。

重構(gòu)測(cè)試

在每個(gè)檢查中，重構(gòu)原始構(gòu)件是關(guān)鍵。給定三個(gè)組成部分（代碼、文檔字符串、注釋）作為輸入，研究人員嘗試從一個(gè)構(gòu)件中重構(gòu)出另一個(gè)構(gòu)件，然后檢查重構(gòu)結(jié)果是否等價(jià)于原始構(gòu)件。

在下圖中，將屏蔽的函數(shù)簽名和注釋提供給 GPT4，并解析生成的代碼。

等價(jià)性檢查

用于代碼的標(biāo)準(zhǔn)等價(jià)性檢查包括輸入輸出比較、符號(hào)執(zhí)行測(cè)試，甚至是完整的形式等價(jià)性檢查。評(píng)估使用作為 CloverBench 數(shù)據(jù)集的一部分包含的單元測(cè)試。檢查文檔字符串的等價(jià)性是具有挑戰(zhàn)性的，因?yàn)樽匀徽Z(yǔ)言不是數(shù)學(xué)上精確的。在評(píng)估中，要求 GPT-4 檢查兩個(gè)文檔字符串是否語(yǔ)義上等價(jià)。為了檢查兩個(gè)注釋的等價(jià)性，將兩個(gè)注釋的等價(jià)性寫成一個(gè)形式引理，并要求 Dafny 證明該引理。

在下圖中，測(cè)試文檔字符串的等價(jià)性。

在不同領(lǐng)域中有幾個(gè)受歡迎的代碼生成數(shù)據(jù)集，但沒有一個(gè)包含注釋或使用 Dafny 語(yǔ)言。研究人員引入了一個(gè)新的手工制作的數(shù)據(jù)集，稱為 CloverBench。在撰寫本文時(shí)，它基于60個(gè)小型手寫示例程序，類似于標(biāo)準(zhǔn)計(jì)算機(jī)科學(xué)教科書中的示例，例如選擇排序。對(duì)于每個(gè)程序，有四個(gè)變體：一個(gè)地面真實(shí)的變體，其代碼、注釋和文檔字符串都是正確和一致的（經(jīng)手工驗(yàn)證）；以及三個(gè)不正確的變體。

評(píng)估一致性檢查算法

主要實(shí)驗(yàn)評(píng)估了 Clover 一致性檢查算法的能力。對(duì)于 CloverBench 中的每個(gè)示例，研究人員運(yùn)行上述描述的所有6個(gè)檢查。評(píng)估多次獨(dú)立運(yùn)行的效果，這意味著將每個(gè)6個(gè)檢查重復(fù) k 次。端到端的結(jié)果總結(jié)在表1中。當(dāng) k=1 時(shí)， Clover 實(shí)現(xiàn)接受了60個(gè)正確（地面真實(shí)）示例中的45個(gè)，并拒絕了所有不正確的示例。當(dāng) k=10 時(shí)，Clover 接受了60個(gè)正確示例中的52個(gè)，并拒絕了所有不正確的示例。

結(jié)論

本文介紹了 Clover，一個(gè)用于閉環(huán)可驗(yàn)證代碼生成的框架。研究人員將檢查正確性的問題簡(jiǎn)化為檢查一致性的更容易解決的問題。

使用 GPT-4、Dafny 和一組簡(jiǎn)單的教科書示例的初步實(shí)驗(yàn)結(jié)果是令人鼓舞的。本文展示了87%的地面真實(shí)示例接受率和100%的不正確示例拒絕率。未來(lái)的工作可能集中在設(shè)計(jì)更好的驗(yàn)證工具、改進(jìn)代碼/注釋/文檔字符串生成質(zhì)量、改進(jìn) LLM 對(duì) Dafny 語(yǔ)法的理解，或者擴(kuò)展到更具挑戰(zhàn)性的示例上。

?譯自（有刪改）：????https://ai.stanford.edu/blog/clover???

本文轉(zhuǎn)載自公眾號(hào)AIGC最前線   

原文鏈接：?https://mp.weixin.qq.com/s/FnBCCe-7tpkKAFtcmWLzqw??