麻薩諸塞大學阿默斯特分校的 Baldur 方法會自動生成用於驗證**和防範漏洞的證明。
本文譯自 Jeffrey Burt 的《使用生成式 AI 除錯軟體》 是一位資深記者，擁有三十多年的新聞經驗，二十多年來一直專注於技術。 在過去的 16 年裡，他一直在 eWeek 工作，然後成為一名自由科技記者。 自 OpenAI 於 2022 年 11 月下旬推出 ChatGPT 聊天機械人以來，生成式 AI 工具和大型語言模型 （LLM） 的採用只會加速，深入到各種形式、規模和行業的組織中，軟體開發人員也無法倖免。 生成式 AI 用例（例如內容建立、對話式 AI 和語言翻譯）在軟體開發中是多種多樣且不斷增長的，涉及優化和生成、錯誤修復、文件和持續整合。 根據 AI 專家 2023 年 10 月在卡內基梅隆大學 SEI 部落格上發表的一篇文章，開發人員越來越多地將生成式 AI 視為一種有用的工具。 作者寫道：“最初關於使用LLM進行軟體開發的炒作已經開始降溫，現在的期望更加現實。 人們的對話已經從期望LLM取代軟體開發人員（即AI）轉變為將LLM視為合作夥伴，並專注於它們的最佳應用領域（即增強智慧型）。 “上個月，由麻薩諸塞大學阿默斯特分校（University of Massachusetts Amherst）的計算機科學家領導的一群人表示，他們正在利用生成式人工智慧和LLM的力量來解決驗證的棘手挑戰**，以幫助防止軟體中的漏洞。 具體來說，該團隊專注於使用人工智慧來開發一種自動生成可用於驗證軟體的完整證明的方法**。 這是乙個耗時、昂貴且耗時的過程，通常通過手動程式完成。 乙個更困難的過程是機器檢查：建立乙個數學證明來顯示**是否符合預期，然後使用定理提供程式來確保證明是正確的。 Emily First在完成電腦科學博士學位後成為加州大學聖地牙哥分校的博士後研究員，而她在麻薩諸塞大學阿默斯特分校攻讀博士學位期間的研究涉及法學碩士和軟體驗證，這是她博士學位的一部分**。 她指出，手動編寫校樣可能比編寫軟體本身花費更多的時間。 因此，根據麻薩諸塞大學阿默斯特分校曼寧資訊與電腦科學學院教授、該論文的資深作者尤里·布倫（Yuriy Brun）的說法，官方驗證的系統數量實際上非常有限。 “這很難，”布倫告訴The New Stack。 “這就是我們介入的地方。 我們試圖解決的問題是自動生成這些證明。 ”
這樣做將有助於解決乙個更大的問題：軟體中的缺陷可能很煩人，或者如果被網路攻擊者利用或存在於可能對廣泛的人產生負面影響的複雜系統中，則很危險。
軟體是我們日常生活的重要組成部分，“布倫說。 “你什麼都做不了。 你不能開車，你不能坐電梯，你不能沒有軟體。 不幸的是，今天的軟體往往容易受到攻擊。 我們幾乎希望在商店中購買的任何軟體都存在一些錯誤。 這只是乙個很難解決的問題，因此有很多不同的方法可以嘗試提高軟體質量。 ”
執行此操作的方法之一是證明軟體是正確的。 這是一種有效的方法，但也是最困難的方法之一。 在某些領域，這種做法已經得到實踐，例如在某些醫療裝置的醫療領域或美國宇航局，“因為如果你的宇宙飛船上有錯誤並且你的軟體崩潰，那將是昂貴的，所以實際上值得讓開發人員和軟體工程師正式證明該功能的正確性。 他說。
一些研究人員已經建立了能夠逐行編寫證明的模型，從證明的前 10 行開始，然後讓模型根據已經寫好的內容和它試圖證明的內容進行搜尋，以找出下一行最有可能是什麼。
麻薩諸塞大學阿默斯特分校的研究人員將目光投向了LLMs，將其作為自動生成證明的可能解決方案。 然而，即使這樣也帶來了挑戰，其中最大的挑戰之一是這些模型並不總是正確的。 他們沒有崩潰，從而讓開發人員知道出了問題，而是“默默地失敗”，生成錯誤的答案，但將其呈現為正確。 悄悄地失敗通常是可能發生的最糟糕的事情，布倫說。
Enterbaldur，一種由麻薩諸塞大學阿默斯特分校團隊建立的基於人工智慧的新型證明方法。 研究人員使用了谷歌的Minerva LLM，它經過了大量自然語言文字的訓練。 然後，它進一步訓練了 118GB 的數學科學**和包含數學表示式的網頁，然後又訓練了 Isabell Hol（一種用於編寫數學證明的語言）。 然後，博德生成了整個證明，使用定理證明者伊莎貝爾來檢查整個世界。 如果檢查員發現錯誤，有關錯誤的資訊將被反饋回 LLM，以便它可以從錯誤中學習，然後生成另乙個證明，從而減少或 - 希望沒有錯誤。 這樣做給了博德“一些上下文資訊，可以說，'這裡有更多關於國家的資訊，關於你正在回答我的問題，'”布倫說。 “當我們給它額外的資訊時，它能夠更好地回答問題。 我們只修復了一次，但正如你可以想象的那樣，對於這些一次只能一步一步的模型來說，即使它們使用大型語言模型來逐步修復，它的效率甚至更低。 ”
布倫和他的團隊（當時還包括在谷歌工作的馬庫斯·拉貝（Markus Rabe）和伊利諾大學厄巴納-香檳分校的助理教授塔利亞·林格（Talia Ringer））研究了Thor，這是乙個整合語言模型和自動定理證明器的框架。 他說，當獨立執行時，Thor能夠在57%的時間內生成證明。 再加上博德——在北歐神話中是托爾的兄弟——他們在 65 年取得了成功證明是在 7% 的時間內建立的。 這兩種方法相輔相成。
Thor“使用乙個大型語言模型來嘗試下乙個可能的證明步驟，但它也使用了一種叫做'錘子'的東西，”布倫說。 “錘子就是這些數學工具，他們說，'我知道一堆數學標籤。 讓我試一試。 讓我試試這個，試試這個，試試這個。 這就像用錘子敲擊乙個問題，然後嘗試不同的方法，看看它是否有效。 它同時嘗試所有這些。 ”
巴爾杜爾方法的不同之處在於，它建立了整個證明，而不是逐行證明，儘管存在重疊，他說：“有些事情他們都可以證明。 但是，通過嘗試一次生成整個證明，我們能夠證明一組不同的東西，而不是試圖一步一步地生成一件事。 ”
Bren 承認錯誤率仍然很高，但他說 Baldur 仍然是驗證軟體正確性的最有效和最高效的方法**。 人工智慧技術在不斷進步，所以他預計博德的能力也會得到提公升。
未來，研究人員計畫將LLM培訓提高657%的數字。 對於驗證，目前資料不多，因此建立資料集並不容易。 他們正在努力建立乙個資料集，以便他們可以微調模型。
他們還希望使開發人員能夠向模型提供反饋，這將進一步幫助模型在生成證明時成長。
開發人員說，'好吧，它工作得很好，'“布倫說。 “但是，如果它不起作用，開發人員通常可以檢視[並說]，'我看到你在這裡嘗試了感應，但你在錯誤的地方使用了它。 它可以向模型提供一些反饋，然後模型可以重試。 這種迭代方法可能會真正簡化開發人員的工作，但也使模型能夠證明它自己無法做到的事情。 ”
這創造了一種半自動化的方法。
最初的迭代方法不涉及開發人員，“他說。 “它自己迭代，一次只做一件事，因為它很......自己做所有事情，自己檢查。 我們正試圖將軟體工程師重新引入到迴圈中，所以這是一種半自動化的方法，我們在很多自動化方面做了很多工作，但後來我們從工程師那裡得到了一些反饋，以指導我們無法自己完成整個過程的情況。 ”
自 2020 年以來，研究人員一直在研究這一挑戰，但博德的工作始於 2023 年 5 月，持續了大約五個月，從在谷歌內部構建到評估和確保科學正確性。 該專案得到了國防高階研究計畫局（DARPA）和美國國家科學學會的支援。