ISEDA首發(fā)！大語言模型生成的代碼到底好不好使

本文內(nèi)容根據(jù)芯華章研究院入選ISEDA2024論文《FormalEval: a Formal Evaluation Tool for Code Generated by Large Language Models》梳理。感謝ISEDA評(píng)選委員會(huì)對(duì)芯華章相關(guān)研究的認(rèn)可。

ISEDA2024技術(shù)分享現(xiàn)場(chǎng)

在開始討論前，有必要先明確這個(gè)驗(yàn)證系統(tǒng)需要具備的兩個(gè)核心屬性：

第一，驗(yàn)證結(jié)果必須是足夠準(zhǔn)確且充分的；

第二，效率也非常重要。

基于這兩點(diǎn)，現(xiàn)有方法又是怎么評(píng)價(jià)模型生成結(jié)果的呢？有三種主流方式：

/ 02 / 基于近似指標(biāo)的自動(dòng)化評(píng)價(jià) 

給定標(biāo)準(zhǔn)答案, 有基于文本間相似度的(Rouge¹), 也有基于文本相似度結(jié)合代碼間結(jié)構(gòu)(抽象語法樹、數(shù)據(jù)依賴圖)相似度的方法(Code-Bleu²);

給定驗(yàn)證平臺(tái), 通過對(duì)比模型在各種不同測(cè)試用例下的輸出是否等于期望結(jié)果來評(píng)價(jià)模型的方法;

而第三種方法雖然準(zhǔn)確度最高, 且在滿足資源(平臺(tái)、用例、仿真器、標(biāo)準(zhǔn)答案)的情況下能實(shí)現(xiàn)自動(dòng)化評(píng)價(jià), 但是這些前置資源的構(gòu)造本身就需要花費(fèi)大量人力成本(編寫好的測(cè)試用例通常和編寫程序一樣困難), 所以該方法也無法實(shí)現(xiàn)真正的大規(guī)模自動(dòng)化驗(yàn)證。我們統(tǒng)計(jì)了四個(gè)廣泛使用的評(píng)估數(shù)據(jù)集，發(fā)現(xiàn)每個(gè)問題的平均測(cè)試用例量都非常少。這會(huì)導(dǎo)致測(cè)試不準(zhǔn)確的現(xiàn)象。

具體來說，當(dāng)前最廣泛被使用的是OpenAI在Codex論文中開源的HumanEval(上表第三行)。OpenAI的(HumanEval³)驗(yàn)證采用了第三種方法, 但僅提供了164個(gè)問題用作模型校驗(yàn), 與之對(duì)應(yīng)的是其提供了成百上千萬行的代碼資料供模型學(xué)習(xí)。

事實(shí)上，后續(xù)有學(xué)者發(fā)現(xiàn)(HumanEval+⁴ 上表第四行)由于平均每個(gè)問題僅包含約10個(gè)測(cè)試用例，即使只考察其提供的問題，該驗(yàn)證系統(tǒng)也不能確保生成的代碼是正確的：

下圖里模型能順利通過HumanEval里的測(cè)試用例(底部)，但由于其實(shí)現(xiàn)邏輯的問題(set是亂序的)，在研究者新給出用例上(頂部)會(huì)校驗(yàn)失敗。

從HumanEval到FormalEval

用形式化驗(yàn)證來替代動(dòng)態(tài)仿真

基于上述方法的局限性, 芯華章提出了 "FormalEval"。

其核心思想是利用形式化的等價(jià)驗(yàn)證方法來替換依賴 {仿真器+測(cè)試用例+測(cè)試平臺(tái)} 的功能性驗(yàn)證方法。

對(duì)比動(dòng)態(tài)仿真驗(yàn)證，形式化驗(yàn)證能通過系統(tǒng)性地覆蓋待校驗(yàn)程序的屬性空間，來確保其符合規(guī)范要求(下圖對(duì)比):

FormalEval的執(zhí)行分為兩個(gè)階段。

在第一階段里，結(jié)合“提示工程”和“檢索增強(qiáng)”等推理技術(shù)，我們對(duì)用戶的自然語言輸入進(jìn)行轉(zhuǎn)換，然后送入大模型里生成代碼。

在第二階段里，給定一組正確標(biāo)記的和模型預(yù)測(cè)的代碼對(duì)，系統(tǒng)會(huì)從語法檢查開始評(píng)估。如果檢查通過，這對(duì)代碼將被發(fā)送到功能檢查器和質(zhì)量檢查器。

如下圖右側(cè)所示，功能檢查器這個(gè)核心模塊，我們采用芯華章自研的 GalaxEC-SEC 工具來替換傳統(tǒng)的仿真工具，工具會(huì)給出一個(gè) {satisfied, violated} 的二值輸出作為驗(yàn)證結(jié)果，簡單明了。

來，上FormalEval實(shí)測(cè)結(jié)果

我們挑選了一個(gè)基于電路設(shè)計(jì)的數(shù)據(jù)集(RTLLM5)來驗(yàn)證FormalEval，該數(shù)據(jù)集里包含了難度不一的28個(gè)設(shè)計(jì)及對(duì)應(yīng)的仿真測(cè)試平臺(tái)。我們分別要求GPT-4 和 GPT-3.5針對(duì)每個(gè)設(shè)計(jì)規(guī)范生成5個(gè)候選答案，再提交給仿真測(cè)試平臺(tái)和FormalEval來檢驗(yàn)。

匯總檢驗(yàn)結(jié)果會(huì)得到如下表格，可以看到雖然語法校驗(yàn)?zāi)芘挪榈粢徊糠值腻e(cuò)誤，但依然存在很多通過了語法校驗(yàn)但功能性檢查失敗的生成代碼。

單獨(dú)對(duì)比功能性檢查的結(jié)果，可以看到FormalEval對(duì)GPT4的精度打分只有0.32，而原仿真測(cè)試則給出了0.63的高分。這是因?yàn)樵抡鏈y(cè)試不能有效識(shí)別大量的錯(cuò)誤結(jié)果。那這個(gè)比例有多高呢？

通過逐個(gè)分析FormalEval給出的錯(cuò)例，我們可以確認(rèn)原仿真測(cè)試工具給出了超出真實(shí)案例100%的假陽性評(píng)分，這是非常具有誤導(dǎo)性和危險(xiǎn)的。

當(dāng)然， 等價(jià)性校驗(yàn)除了在評(píng)估模型時(shí)至關(guān)重要，在提示技術(shù)選擇、數(shù)據(jù)自標(biāo)注、模型性能提升、線上推斷時(shí)也都有廣泛的使用場(chǎng)景。

而且，除了等價(jià)性校驗(yàn)，形式化方法學(xué)里的另一大分支模型檢測(cè)技術(shù)也能夠被應(yīng)用在大模型產(chǎn)品里。

以上這些方面，芯華章的工作也正在進(jìn)行中。