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

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

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

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

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

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

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

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

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

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

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

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

Dafny

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

Clover 第一階段：生成

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

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

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

具體而言，總共有六個檢查：

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

重構(gòu)測試

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

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

等價(jià)性檢查

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

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

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

評估一致性檢查算法

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

結(jié)論

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

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

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

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

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