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

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

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

正式驗證和人工智能是一對良好的搭檔

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

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

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

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

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

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

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

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

Dafny

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

Clover 第一階段：生成

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

Clover 第二階段：驗證

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

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

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

重構測試

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

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

等價性檢查

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

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

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

評估一致性檢查算法

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

結論

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

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

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

本文轉載自公眾號AIGC最前線   

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