ISEDA首發(fā)！大語(yǔ)言模型生成的代碼到底好不好使
加入技術(shù)交流群
在大模型席卷一切、賦能百業(yè)的浪潮里，“碼農”也沒(méi)能獨善其身。各種代碼自動(dòng)生成的大模型，似乎描繪了一個(gè)人人都能像資深工程師一樣寫(xiě)代碼的美好未來(lái)。
本文引用地址：http://dyxdggzs.com/article/202405/458824.htm但在這個(gè)理想成為現實(shí)之前，有一個(gè)不能回避的問(wèn)題 — 這些自動(dòng)生成的代碼真的有效嗎？大模型也會(huì )犯錯，我們肯定不希望把看似正確的錯誤結果交給用戶(hù)，所以需要一個(gè)能精確驗證模型生成答案的考官。
近期，芯華章提出了一種對大模型生成代碼形式化評估的方法，稱(chēng)為FormalEval。它能自動(dòng)化檢査生成代碼的質(zhì)量，無(wú)需手動(dòng)編寫(xiě)測試用例。經(jīng)過(guò)測試，FormalEval不僅能夠識別出現有 RTL 基準數據集中潛藏的約50% 的評估錯誤，還能通過(guò)測試用例增強的方式來(lái)修復這些錯誤。
本文內容根據芯華章研究院入選ISEDA2024論文《FormalEval: a Formal Evaluation Tool for Code Generated by Large Language Models》梳理。感謝ISEDA評選委員會(huì )對芯華章相關(guān)研究的認可。
ISEDA2024技術(shù)分享現場(chǎng)
現有驗證方法
要么費時(shí)費力，要么不夠準確
在開(kāi)始討論前，有必要先明確這個(gè)驗證系統需要具備的兩個(gè)核心屬性：
第一，驗證結果必須是足夠準確且充分的；
第二，效率也非常重要。
基于這兩點(diǎn)，現有方法又是怎么評價(jià)模型生成結果的呢？有三種主流方式：
/ 02 / 基于近似指標的自動(dòng)化評價(jià)
給定標準答案, 有基于文本間相似度的(Rouge1), 也有基于文本相似度結合代碼間結構(抽象語(yǔ)法樹(shù)、數據依賴(lài)圖)相似度的方法(Code-Bleu2);
給定驗證平臺, 通過(guò)對比模型在各種不同測試用例下的輸出是否等于期望結果來(lái)評價(jià)模型的方法;
而第三種方法雖然準確度最高, 且在滿(mǎn)足資源(平臺、用例、仿真器、標準答案)的情況下能實(shí)現自動(dòng)化評價(jià), 但是這些前置資源的構造本身就需要花費大量人力成本(編寫(xiě)好的測試用例通常和編寫(xiě)程序一樣困難), 所以該方法也無(wú)法實(shí)現真正的大規模自動(dòng)化驗證。我們統計了四個(gè)廣泛使用的評估數據集，發(fā)現每個(gè)問(wèn)題的平均測試用例量都非常少。這會(huì )導致測試不準確的現象。
從HumanEval到FormalEval
用形式化驗證來(lái)替代動(dòng)態(tài)仿真
基于上述方法的局限性, 芯華章提出了 "FormalEval"。
FormalEval的執行分為兩個(gè)階段。
在第一階段里，結合“提示工程”和“檢索增強”等推理技術(shù)，我們對用戶(hù)的自然語(yǔ)言輸入進(jìn)行轉換，然后送入大模型里生成代碼。
在第二階段里，給定一組正確標記的和模型預測的代碼對，系統會(huì )從語(yǔ)法檢查開(kāi)始評估。如果檢查通過(guò)，這對代碼將被發(fā)送到功能檢查器和質(zhì)量檢查器。
如下圖右側所示，功能檢查器這個(gè)核心模塊，我們采用芯華章自研的 GalaxEC-SEC 工具來(lái)替換傳統的仿真工具，工具會(huì )給出一個(gè) {satisfied, violated} 的二值輸出作為驗證結果，簡(jiǎn)單明了。
來(lái)，上FormalEval實(shí)測結果
匯總檢驗結果會(huì )得到如下表格，可以看到雖然語(yǔ)法校驗能排查掉一部分的錯誤，但依然存在很多通過(guò)了語(yǔ)法校驗但功能性檢查失敗的生成代碼。
單獨對比功能性檢查的結果，可以看到FormalEval對GPT4的精度打分只有0.32，而原仿真測試則給出了0.63的高分。這是因為原仿真測試不能有效識別大量的錯誤結果。那這個(gè)比例有多高呢？
通過(guò)逐個(gè)分析FormalEval給出的錯例，我們可以確認原仿真測試工具給出了超出真實(shí)案例100%的假陽(yáng)性評分，這是非常具有誤導性和危險的。
示例：
Prompt：
The concatenation of signal and should have only 1 bit high.LLM：
($onehot({rbF,rbE}))
結果：
當然， 等價(jià)性校驗除了在評估模型時(shí)至關(guān)重要，在提示技術(shù)選擇、數據自標注、模型性能提升、線(xiàn)上推斷時(shí)也都有廣泛的使用場(chǎng)景。
而且，除了等價(jià)性校驗，形式化方法學(xué)里的另一大分支模型檢測技術(shù)也能夠被應用在大模型產(chǎn)品里。
以上這些方面，芯華章的工作也正在進(jìn)行中。
總結
近年來(lái)大模型徹底顛覆了學(xué)界里AI的研究方向，基于大模型的各種應用也如雨后春筍般涌現，但要真正形成成熟的產(chǎn)品，大模型的幻覺(jué)問(wèn)題和輸出不可控問(wèn)題等都是不得不解決的挑戰。
擁有一個(gè)準確、自動(dòng)、高效的驗證工具能夠保證您的應用在用戶(hù)側安全，穩定地輸出符合預期的結果。如果您對FormalEval這款工具感興趣，歡迎點(diǎn)擊閱讀原文，申請下載論文全篇內容，我們將與您取得進(jìn)一步聯(lián)系。
評論