【ZiDongHua 之設(shè)計(jì)自動化收錄關(guān)鍵詞：芯華章  EDA 電子設(shè)計(jì)自動化 】
　　
　　ISEDA首發(fā)！大語言模型生成的代碼到底好不好使
　　
　　在大模型席卷一切、賦能百業(yè)的浪潮里，“碼農(nóng)”也沒能獨(dú)善其身。各種代碼自動生成的大模型，似乎描繪了一個人人都能像資深工程師一樣寫代碼的美好未來。
　　
　　但在這個理想成為現(xiàn)實(shí)之前，有一個不能回避的問題 — 這些自動生成的代碼真的有效嗎？大模型也會犯錯，我們肯定不希望把看似正確的錯誤結(jié)果交給用戶，所以需要一個能精確驗(yàn)證模型生成答案的考官。
　　
　　近期，芯華章提出了一種對大模型生成代碼形式化評估的方法，稱為FormalEval。它能自動化檢査生成代碼的質(zhì)量，無需手動編寫測試用例。經(jīng)過測試，F(xiàn)ormalEval不僅能夠識別出現(xiàn)有 RTL 基準(zhǔn)數(shù)據(jù)集中潛藏的約50% 的評估錯誤，還能通過測試用例增強(qiáng)的方式來修復(fù)這些錯誤。
　　
　　本文共計(jì)2680字，預(yù)計(jì)閱讀時間7分鐘，希望能夠幫助您更好了解：
　　
　　• 如何快速驗(yàn)證大模型自動生成的代碼？
　　
　　• 新的方式和傳統(tǒng)方法有什么不一樣？
　　
　　本文內(nèi)容根據(jù)芯華章研究院入選ISEDA2024論文《FormalEval: a Formal Evaluation Tool for Code Generated by Large Language Models》梳理。感謝ISEDA評選委員會對芯華章相關(guān)研究的認(rèn)可。
　　
　　
　　
　　ISEDA2024技術(shù)分享現(xiàn)場
　　
　　現(xiàn)有驗(yàn)證方法
　　
　　要么費(fèi)時費(fèi)力，要么不夠準(zhǔn)確
　　
　　在開始討論前，有必要先明確這個驗(yàn)證系統(tǒng)需要具備的兩個核心屬性：
　　
　　第一，驗(yàn)證結(jié)果必須是足夠準(zhǔn)確且充分的；
　　
　　第二，效率也非常重要。
　　
　　基于這兩點(diǎn)，現(xiàn)有方法又是怎么評價模型生成結(jié)果的呢？有三種主流方式：
　　
　　
　　
　　/ 01 / 
　　
　　人類專家評價 
　　
　　給定問題, 大模型生成代碼, 人類工程師來判斷結(jié)果是否正確;
　　
　　/ 02 / 
　　
　　基于近似指標(biāo)的自動化評價 
　　
　　給定標(biāo)準(zhǔn)答案, 有基于文本間相似度的(Rouge1), 也有基于文本相似度結(jié)合代碼間結(jié)構(gòu)(抽象語法樹、數(shù)據(jù)依賴圖)相似度的方法(Code-Bleu2);
　　
　　/ 03 / 
　　
　　基于驗(yàn)證平臺和測試用例的自動化評價
　　
　　給定驗(yàn)證平臺, 通過對比模型在各種不同測試用例下的輸出是否等于期望結(jié)果來評價模型的方法;
　　
　　顯然, 第一種方法的評價精度受限于專家自身的能力, 而成本也受限于專家的時間資源。
　　
　　第二種方法, 雖然自動化程度高, 依賴的資源不多(只需要一份標(biāo)準(zhǔn)答案), 但因?yàn)榻柚氖墙浦笜?biāo)的關(guān)系, 無法保證在指標(biāo)上表現(xiàn)理想的模型，在功能上也能真正符合預(yù)期。從下例可以看出，明明模型生成的代碼給出的答案和正例是完全相反的，但是code-bleu得分卻接近1(滿分)，這顯然是不合理的。
　　
　
　　
　　而第三種方法雖然準(zhǔn)確度最高, 且在滿足資源(平臺、用例、仿真器、標(biāo)準(zhǔn)答案)的情況下能實(shí)現(xiàn)自動化評價, 但是這些前置資源的構(gòu)造本身就需要花費(fèi)大量人力成本(編寫好的測試用例通常和編寫程序一樣困難), 所以該方法也無法實(shí)現(xiàn)真正的大規(guī)模自動化驗(yàn)證。我們統(tǒng)計(jì)了四個廣泛使用的評估數(shù)據(jù)集，發(fā)現(xiàn)每個問題的平均測試用例量都非常少。這會導(dǎo)致測試不準(zhǔn)確的現(xiàn)象。
 
　　具體來說，當(dāng)前最廣泛被使用的是OpenAI在Codex論文中開源的HumanEval(上表第三行)。OpenAI的(HumanEval3)驗(yàn)證采用了第三種方法, 但僅提供了164個問題用作模型校驗(yàn), 與之對應(yīng)的是其提供了成百上千萬行的代碼資料供模型學(xué)習(xí)。
　　
　　事實(shí)上，后續(xù)有學(xué)者發(fā)現(xiàn)(HumanEval+4 上表第四行)由于平均每個問題僅包含約10個測試用例，即使只考察其提供的問題，該驗(yàn)證系統(tǒng)也不能確保生成的代碼是正確的：
　　
　　下圖里模型能順利通過HumanEval里的測試用例(底部)，但由于其實(shí)現(xiàn)邏輯的問題(set是亂序的)，在研究者新給出用例上(頂部)會校驗(yàn)失敗。
　
　　從HumanEval到FormalEval
　　
　　用形式化驗(yàn)證來替代動態(tài)仿真
　　
　　基于上述方法的局限性, 芯華章提出了 "FormalEval"。
　　
　　其核心思想是利用形式化的等價驗(yàn)證方法來替換依賴 {仿真器+測試用例+測試平臺} 的功能性驗(yàn)證方法。
　　
　　對比動態(tài)仿真驗(yàn)證，形式化驗(yàn)證能通過系統(tǒng)性地覆蓋待校驗(yàn)程序的屬性空間，來確保其符合規(guī)范要求(下圖對比):
　　
　　FormalEval的執(zhí)行分為兩個階段。
　　
　　在第一階段里，結(jié)合“提示工程”和“檢索增強(qiáng)”等推理技術(shù)，我們對用戶的自然語言輸入進(jìn)行轉(zhuǎn)換，然后送入大模型里生成代碼。
　　
　　在第二階段里，給定一組正確標(biāo)記的和模型預(yù)測的代碼對，系統(tǒng)會從語法檢查開始評估。如果檢查通過，這對代碼將被發(fā)送到功能檢查器和質(zhì)量檢查器。
　　
　　如下圖右側(cè)所示，功能檢查器這個核心模塊，我們采用芯華章自研的 GalaxEC-SEC 工具來替換傳統(tǒng)的仿真工具，工具會給出一個 {satisfied, violated} 的二值輸出作為驗(yàn)證結(jié)果，簡單明了。
　　
　　來，上FormalEval實(shí)測結(jié)果
　　
　　我們挑選了一個基于電路設(shè)計(jì)的數(shù)據(jù)集(RTLLM5)來驗(yàn)證FormalEval，該數(shù)據(jù)集里包含了難度不一的28個設(shè)計(jì)及對應(yīng)的仿真測試平臺。我們分別要求GPT-4 和 GPT-3.5針對每個設(shè)計(jì)規(guī)范生成5個候選答案，再提交給仿真測試平臺和FormalEval來檢驗(yàn)。
　　
　　匯總檢驗(yàn)結(jié)果會得到如下表格，可以看到雖然語法校驗(yàn)?zāi)芘挪榈粢徊糠值腻e誤，但依然存在很多通過了語法校驗(yàn)但功能性檢查失敗的生成代碼。
　　
　　單獨(dú)對比功能性檢查的結(jié)果，可以看到FormalEval對GPT4的精度打分只有0.32，而原仿真測試則給出了0.63的高分。這是因?yàn)樵抡鏈y試不能有效識別大量的錯誤結(jié)果。那這個比例有多高呢？
　　
　　通過逐個分析FormalEval給出的錯例，我們可以確認(rèn)原仿真測試工具給出了超出真實(shí)案例100%的假陽性評分，這是非常具有誤導(dǎo)性和危險的。
 
　　同時，因?yàn)镕ormalEval無需人工編寫測試用例，我們可以方便地翻倍原測試數(shù)據(jù)，以確保模型在不同測試數(shù)據(jù)集上的一致性表現(xiàn)。
　　
　　示例：
　　
　　Prompt：
　　
　　The concatenation of signal and should have only 1 bit high.
　　
　　LLM：
　　
　　($onehot({rbF,rbE}))
　　
　　結(jié)果：
　　
　　當(dāng)然， 等價性校驗(yàn)除了在評估模型時至關(guān)重要，在提示技術(shù)選擇、數(shù)據(jù)自標(biāo)注、模型性能提升、線上推斷時也都有廣泛的使用場景。
　　
　　而且，除了等價性校驗(yàn)，形式化方法學(xué)里的另一大分支模型檢測技術(shù)也能夠被應(yīng)用在大模型產(chǎn)品里。
　　
　　以上這些方面，芯華章的工作也正在進(jìn)行中。
　　
　　總結(jié)
　　
　　近年來大模型徹底顛覆了學(xué)界里AI的研究方向，基于大模型的各種應(yīng)用也如雨后春筍般涌現(xiàn)，但要真正形成成熟的產(chǎn)品，大模型的幻覺問題和輸出不可控問題等都是不得不解決的挑戰(zhàn)。
　　
　　擁有一個準(zhǔn)確、自動、高效的驗(yàn)證工具能夠保證您的應(yīng)用在用戶側(cè)安全，穩(wěn)定地輸出符合預(yù)期的結(jié)果。如果您對FormalEval這款工具感興趣，歡迎點(diǎn)擊閱讀原文，申請下載論文全篇內(nèi)容，我們將與您取得進(jìn)一步聯(lián)系。
　　
　　關(guān)于ISEDA
　　
　　ISEDA由EDA開放創(chuàng)新合作機(jī)制（EDA²）和中國電子學(xué)會電子設(shè)計(jì)自動化專委會共同主辦，由中國科學(xué)院院士、東南大學(xué)校長黃如，中國科學(xué)院院士、西安電子科技大學(xué)教授郝躍擔(dān)任執(zhí)行委員會主席；魏少軍、曾璇、Patrick Girard為指導(dǎo)委員會主席；朱樟明、王潤聲、楊軍為大會共同主席；游海龍、梁云、閆浩為技術(shù)委員會共同主席。
　　
　　關(guān)于芯華章研究院
　　
　　作為企業(yè)驅(qū)動型創(chuàng)研平臺，芯華章研究院旨在凝聚國內(nèi)外學(xué)界和行業(yè)中堅(jiān)力量，從數(shù)字產(chǎn)業(yè)需求出發(fā)，推動異構(gòu)計(jì)算、云原生、人工智能等EDA共性技術(shù)創(chuàng)新研究，以更智能易用的下一代EDA 2.0作為應(yīng)用系統(tǒng)和芯片設(shè)計(jì)之間的橋梁，讓芯片設(shè)計(jì)更簡單、更普惠。
　　
　　注釋：
　　
　　1:Lin, Chin-Yew. “ROUGE: A Package for Automatic Evaluation of Summaries,” 2004.
　　
　　2:Ren, Shuo, Daya Guo, Shuai Lu, Long Zhou, Shujie Liu, Duyu Tang, Neel Sundaresan, Ming Zhou, Ambrosio Blanco, and Shuai Ma. “CodeBLEU: A Method for Automatic Evaluation of Code Synthesis.” arXiv, September 27, 2020. 
　　
　　http://arxiv.org/abs/2009.10297.
　　
　　3:Chen, Mark, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, et al. “Evaluating Large Language Models Trained on Code.” arXiv, July 14, 2021.
　　
　　http://arxiv.org/abs/2107.03374.
　　
　　4:Liu, Jiawei, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. “Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation.” arXiv, June 12, 2023.
　　
　　http://arxiv.org/abs/2305.01210.
　　
　　5:Lu, Yao, Shang Liu, Qijun Zhang, and Zhiyao Xie. “RTLLM: An Open-Source Benchmark for Design RTL Generation with Large Language Model.” arXiv, November 11, 2023. 
　　
　　http://arxiv.org/abs/2308.05345.