原创 岱军 云云众生s
UMass Amherst的Baldur方法能夠自動產生用於驗證程式碼、防範漏洞的證明。

譯自Debugging Software Using Generative AI，作者 Jeffrey Burt 是一位資深記者，擁有三十多年的新聞工作經驗，過去二十多年專注於科技領域。 在過去的16年多里，他曾在eWEEK工作，並在之後成為自由科技記者。

自從OpenAI於2022年11月底推出其ChatGPT聊天機器人以來，生成式人工智慧工具和大型語言模型（LLM）的採用只有加速，深入滲透到各種形狀、大小和行業的組織中，而軟體開發人員並 未對其產生免疫。

生成式人工智慧的用例，如內容創作、對話式人工智慧和語言翻譯，在軟體開發中是多樣化且不斷增長的，涉及程式碼優化和生成、錯誤修復、文件編寫以及持續整合等方面。

根據卡內基美隆大學SEI部落格中的AI專家在2023年10月的一篇文章稱，開發人員越來越認為生成式人工智慧是一個有用的工具。

作者寫道：“關於使用LLM進行軟體開發的最初炒作已經開始冷卻，現在的期望更加現實。”，“對話已經從期望LLM取代軟體開發人員（即人工智慧）轉變為將LLM視為合作夥伴， 並集中在最佳應用它們的地方（即增強型智能）。”

LLM和軟體驗證
上個月，由馬薩諸塞大學阿默斯特分校的電腦科學家領導的一組人表示，他們正在利用生成式人工智慧和LLM的力量來解決驗證程式碼的棘手挑戰，以幫助防止軟體中的漏洞。

具體而言，該團隊專注於利用人工智慧開發一種方法，自動產生完整的證明以用於驗證軟體程式碼。 這是一項費時、昂貴且耗時的過程，通常透過手動程序完成。 更困難的過程是機器檢查：創建一個數學證明來展示程式碼是否符合預期，然後使用定理提供者確保證明的正確性。

Emily First在完成她的電腦科學博士學位後成為加州大學聖迭戈分校的博士後研究員，而她在馬薩諸塞大學阿默斯特分校攻讀博士學位期間的研究涉及LLM和軟體驗證，並成為她博士論文的一部分。 她指出，手動編寫證明所需的時間可能比編寫軟體程式碼本身還要多。

因此，根據馬薩諸塞大學阿默斯特分校資訊與電腦科學曼寧學院的教授、本文的高級作者Yuriy Brun的說法，實際上經過正式驗證的系統數量相當有限。

「這很難，」Brun告訴The New Stack。 “這就是我們介入的地方。我們試圖解決的問題是自動產生這些證明。”

不應該接受有錯誤的軟體
這樣做將有助於解決一個更大的問題：軟體中存在缺陷，這可能是煩人的，或者——如果被網路攻擊者利用或存在於可能對廣泛產生負面影響的複雜系統中——是危險 的。

「軟體是我們日常生活中重要的一部分，」布倫說。 「你什麼都做不了。你不能開車，不能坐電梯，都離不開軟體。不幸的是，今天的軟體通常是有漏洞的。我們幾乎期望在商店購買的任何軟體都會有一些錯誤。這只是 一個難以解決的問題，因此有很多不同的方法來嘗試提高軟體的品質。”

其中一個方法是證明軟體是正確的。 這是一種有效的方法，但也是最困難的方法之一。 在某些領域，這已經被實踐，例如在醫療領域用於某些醫療設備或由NASA使用，「因為如果你的太空船上有一個錯誤，你的軟體崩潰了，那將是代價高昂的， 所以實際上有開發人員和軟體工程師正式證明函數的正確性是值得的。」他說。

一些研究人員已經創建了能夠一行一行地寫證明的模型，先寫證明的前10行，然後讓模型基於已經寫的內容以及試圖證明的內容搜索，找出下一行最有可能是什麼。

建構Baldur
馬薩諸塞大學阿默斯特分校的研究人員將目光投向LLM，作為自動產生證明的可能解決方案。 然而，即使這也帶來了挑戰，最大的挑戰之一是這些模型並不總是正確的。 與其崩潰——從而讓開發人員知道有些事情出錯了——它們會“悄悄失敗”，生成一個錯誤的答案但將其呈現為正確的。 悄悄失敗通常是最糟糕的事情，布倫說。

EnterBaldur，這是馬薩諸塞大學阿默斯特分校團隊創建的一種新的基於人工智慧的證明方法。 研究人員使用了Google的Minerva LLM，該模型經過大量自然語言文本的訓練。 然後，它進一步在118GB的數學科學論文和包含數學表達式的網頁上進行訓練，然後在Isabell/HOL上進行了更多的訓練，這是一種用於編寫數學證明的語言。

然後，Baldur產生了整個證明，使用Isabelle，一個定理證明器，對整個世界進行檢查。 如果檢查器發現錯誤，有關錯誤的資訊會回饋到LLM中，以便讓它從錯誤中學習，然後產生另一個證明，減少或——希望是沒有錯誤。

這樣做給了Baldur「一些上下文訊息，以說，『關於狀態，關於你正在回答我的問題的問題，這裡有更多的信息，』」布倫說。 「當我們給它額外的資訊時，它能夠更好地回答問題。我們只修復了一次，但你可以想像多次修復，對於這些一次只能預測一個步驟的模型來說，即使它們使用大型語言 模型逐步預測，這也更加低效。”

Enter Thor
布倫及其團隊（當時還包括在Google工作的Markus Rabe和伊利諾伊大學厄巴納-香檳分校的助理教授Talia Ringer）研究了Thor，一個用於整合語言模型和自動定理證明器的框架。 獨立運作時，Thor能夠在57%的情況下產生證明，他說。

將其與 Baldur 結合——在北歐神話中是托爾的兄弟——他們成功地在65.7%的時間內創建了證明。 這兩種方法互相補充。

Thor「使用大型語言模型嘗試預測證明的下一個可能步驟，但它也使用了一些被稱為『錘子』的東西，」布倫說。 「錘子是這些數學工具，它們說，『我知道一堆數學標籤。讓我嘗試一下。讓我試試這個，試試這個，試試這個。』就像用錘子敲擊問題，嘗試不同的方法 ，看看是否有效。它同時嘗試所有這些方法。”

Baldur方法不同之處在於它創建整個證明而不是逐行進行，儘管存在重疊，他說：「有一些它們都能證明的事情。但透過嘗試一次性生成整個證明，我們能夠證明一組不同的事情 ，而不是嘗試逐步生成一件事。”

仍有更多工作要做
布倫承認錯誤程度仍然很大，但稱Baldur仍然代表了驗證軟體程式碼正確性的最有效和高效的方式。 AI技術不斷改進，因此他預期Baldur的能力也會提升。

在未來，研究人員計劃透過調整LLM訓練的數據來提高65.7%的數字。 對於驗證而言，目前並沒有太多的數據，因此建立數據集並不容易。 他們正在努力創建一個資料集，以便對模型進行微調。

他們還希望使開發人員能夠向模型提供回饋，這將進一步幫助模型在產生證明的過程中不斷成長。

「開發人員說，『好的，運作得很好，』」布倫說。 「但如果它沒有運行，開發人員通常可以查看[然後說]，『我看到你在這裡嘗試了歸納，但你把它用在了錯誤的地方。』 它可以向模型提供一些反饋，然後模型 可以再次嘗試。這種迭代的方法很可能真正簡化開發人員的工作，但也使模型能夠證明它自己無法完成的事情。”

這創造了一種半自動化的方法。

「原始的迭代方法不涉及開發人員，」他說。 「它是在自己進行迭代，一次只做一件事，因為它是……自己進行所有操作，自己檢查。我們試圖重新引入軟體工程師到這個循環中，因此這是一種半自動化的方法，我們 在很多自動化方面做了很多工作，但然後我們從工程師那裡得到了一些反饋，以引導在我們無法自行完成整個過程的情況下進行處理。”

研究人員從2020年開始致力於這個挑戰，但Baldur的工作始於2023年5月，從在Google內部建構到評估和確保科學正確性，歷時約五個月。 該計畫得到了國防高級研究計劃局（DARPA）和國家科學基金會的支持。