從一鍵生成操作系統(tǒng)內(nèi)核，到從零手搓一個(gè) C 編譯器，編程智能體（Coding Agent）的能力邊界正在瘋狂擴(kuò)張。

但一個(gè)更棘手的問(wèn)題是：這些代碼，真的對(duì)嗎？當(dāng)自動(dòng)生成的代碼規(guī)模迅速膨脹，一個(gè)幽靈般的挑戰(zhàn)始終揮之不去：代碼能跑，但邏輯深處的 bug 多到令人頭皮發(fā)麻。

對(duì)于大語(yǔ)言模型（LLM）來(lái)說(shuō)，寫出語(yǔ)法正確的“磚塊”輕而易舉，但距離用這些磚塊搭建一座安全穩(wěn)固的“摩天大樓”仍有顯著的差距。因此，如何更好地保障大規(guī)模代碼的正確性，正成為一個(gè)日益重要的問(wèn)題。

近日，上海交通大學(xué) IPADS 研究團(tuán)隊(duì)打造了形式化方法智能體 FM-Agent，首次實(shí)現(xiàn)了面向大規(guī)模系統(tǒng)的全自動(dòng)正確性推理。

在 Anthropic、NVIDIA 等用頂尖編程智能體生成的多個(gè)大規(guī)模系統(tǒng)（單個(gè)系統(tǒng)規(guī)模高達(dá) 14.3 萬(wàn)行）中，F(xiàn)M-Agent 成功找到了 522 個(gè)隱藏 bug。值得關(guān)注的是，這些 bug 經(jīng)過(guò)單元測(cè)試、差分測(cè)試、多智能體交叉審查等手段都未能發(fā)現(xiàn)。

圖丨相關(guān)論文（來(lái)源：arXiv）

相關(guān)論文以《FM-Agent：通過(guò)基于大語(yǔ)言模型的霍爾邏輯推理將形式化方法擴(kuò)展至大規(guī)模系統(tǒng)軟件》（FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning）為題發(fā)表在預(yù)印本網(wǎng)站 arXiv[1]。

論文作者包括上海交通大學(xué) IPADS 團(tuán)隊(duì)的陳海波教授、王肇國(guó)教授和丁浩然博士。目前，研究團(tuán)隊(duì)已推出 FM-Agent 源碼和網(wǎng)站[2,3]，提供 FM-Agent 在線服務(wù)，用戶提供代碼壓縮包、API Key 和模型名稱后即可開(kāi)始驗(yàn)證。

圖丨從左至右分別是：王肇國(guó)、陳海波和丁浩然（來(lái)源：受訪者）

跳出“將錯(cuò)就錯(cuò)”：AI 開(kāi)始從需求驗(yàn)證代碼

那么，F(xiàn)M-Agent 是如何將形式化方法用于大規(guī)模系統(tǒng)的？要理解這個(gè)問(wèn)題，我們得先回溯到圖靈獎(jiǎng)得主托尼·霍爾（Tony Hoare）早在 20 世紀(jì) 60 年代為代碼驗(yàn)證指明的方向——組合式推理（Compositional Reasoning）。

組合式推理的基本思想非常優(yōu)雅：為了驗(yàn)證復(fù)雜系統(tǒng)的正確性，首先把它拆解成一個(gè)個(gè)獨(dú)立的小函數(shù)。然后，給每個(gè)函數(shù)寫一份精確的形式化規(guī)約（Formal Specification），即一份用數(shù)學(xué)語(yǔ)言寫成的“說(shuō)明書”，說(shuō)明執(zhí)行函數(shù)前程序狀態(tài)需要滿足什么條件（前置條件），執(zhí)行后函數(shù)保證輸出什么樣的結(jié)果（后置條件）。最后，只要分別證明每個(gè)函數(shù)的實(shí)現(xiàn)（Implementation）和規(guī)約一致，就能直接推理出整個(gè)系統(tǒng)滿足正確性。

盡管組合式推理的愿景很美好，但一個(gè)關(guān)鍵的現(xiàn)實(shí)問(wèn)題是，形式化規(guī)約需要靠人類專家用極其嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)公式手寫，人力成本高昂。在 LLM 生成代碼的時(shí)代，迅速放大了這個(gè)痛點(diǎn)。

陳海波對(duì) DeepTech 表示：“當(dāng)編程智能體可以生成 10 萬(wàn)行以上代碼時(shí)，開(kāi)發(fā)者對(duì)內(nèi)部的函數(shù)行為本就一知半解，為成百上千個(gè)函數(shù)編寫形式化規(guī)約更不可行。因此，盡管相關(guān)工作在自動(dòng)生成證明方面取得了長(zhǎng)足的進(jìn)步，但是從本質(zhì)上來(lái)看形式化方法仍然是‘屠龍之術(shù)’，難以推廣至大規(guī)模系統(tǒng)軟件?！?/p>

此前，也有研究工作嘗試用 LLM 自動(dòng)生成規(guī)約，但卻掉入了“將錯(cuò)就錯(cuò)”的陷阱：通過(guò)分析函數(shù)本身的實(shí)現(xiàn)來(lái)反推規(guī)約。但如果函數(shù)實(shí)現(xiàn)本身就有 bug，那么反推出來(lái)的規(guī)約也容易被誤導(dǎo)。

這就像是鸚鵡學(xué)舌（復(fù)述函數(shù)的工作流程），把 bug 當(dāng)成正確行為寫進(jìn)去，會(huì)直接導(dǎo)致后續(xù)的驗(yàn)證無(wú)法發(fā)現(xiàn) bug。關(guān)鍵在于，函數(shù)本身可能不可靠，但調(diào)用它的上下文往往更接近真實(shí)需求。

為了解決這一問(wèn)題，F(xiàn)M-Agent 提出了新方法：既然函數(shù)自己的實(shí)現(xiàn)可能會(huì)騙人，那就去問(wèn)函數(shù)的“上級(jí)”——那些調(diào)用它的函數(shù)。下圖展示了調(diào)用者驅(qū)動(dòng)的規(guī)約自動(dòng)生成方法，基本思想是結(jié)合函數(shù)實(shí)現(xiàn)、調(diào)用者期望和領(lǐng)域背景知識(shí)，讓 LLM 為函數(shù)生成規(guī)約。

圖丨調(diào)用者驅(qū)動(dòng)的函數(shù) F 規(guī)約自動(dòng)生成（來(lái)源：arXiv）

王肇國(guó)對(duì) DeepTech 解釋：這就像是甲方（調(diào)用方）交給乙方（被調(diào)用函數(shù)）一個(gè)任務(wù)，要求輸入合格的材料（前置條件），必須交付合格的產(chǎn)品（后置條件）。哪怕乙方在內(nèi)部施工時(shí)偷工減料、走了彎路（bug），甲方對(duì)這份工作的原始要求依然是清晰且正確的。

從本質(zhì)來(lái)看，F(xiàn)M-Agent 做了兩件事：一是重新定義規(guī)約的來(lái)源，二是用 LLM 完成推理過(guò)程。FM-Agent 就是那個(gè)拿著甲方原始合同，去驗(yàn)收乙方成果的質(zhì)檢員。

（來(lái)源：arXiv）

如下圖所示，F(xiàn)M-Agent 提出了一種創(chuàng)新的自上而下規(guī)約生成范式：從用戶對(duì)系統(tǒng)整體正確行為的期望出發(fā)，逐步推導(dǎo)出每個(gè)函數(shù)應(yīng)滿足的規(guī)約。這樣做可以避免被具體實(shí)現(xiàn)誤導(dǎo)，生成的規(guī)約描述的是函數(shù)“應(yīng)該做什么”，而不是“怎么做”。

圖丨自上而下的規(guī)約生成新范式（來(lái)源：arXiv）

在推理過(guò)程的可靠性方面，研究團(tuán)隊(duì)并不是直接讓 LLM 判斷代碼是否正確，而是將思維鏈（Chain of Thought）與霍爾邏輯的推理規(guī)則相結(jié)合，引導(dǎo) LLM 逐步推導(dǎo)每個(gè)代碼塊執(zhí)行后程序狀態(tài)所滿足的性質(zhì)，最終檢查程序狀態(tài)是否符合“說(shuō)明書”的要求。

此外，對(duì)于可能存在 bug 的函數(shù)，LLM 會(huì)基于推理過(guò)程嘗試生成測(cè)試用例來(lái)觸發(fā) bug，只有成功觸發(fā)的 bug 才會(huì)被最終報(bào)告給開(kāi)發(fā)者，進(jìn)一步提升了 bug 上報(bào)的準(zhǔn)確性。

那么，如何在絕對(duì)嚴(yán)謹(jǐn)與工程可用之間取得平衡呢？FM-Agent 的基本思路是：先分析 LLM 擅長(zhǎng)什么，然后將其與傳統(tǒng)形式化驗(yàn)證流程進(jìn)行對(duì)照，判斷哪些步驟可以適當(dāng)放寬對(duì)“絕對(duì)嚴(yán)謹(jǐn)”的要求，從而換取“工程可用”。

這一平衡的關(guān)鍵在于利用 LLM 的兩項(xiàng)能力：一是在提供函數(shù)調(diào)用上下文的前提下，能夠理解每個(gè)函數(shù)的意圖；二是在處理較短程序時(shí)，能根據(jù)輸入準(zhǔn)確推導(dǎo)輸出。它們分別支撐了 FM-Agent 自動(dòng)生成規(guī)約和自動(dòng)推理程序正確性的能力。

在層層測(cè)試之后，AI 依然挖出最隱蔽的 Bug

盡管已有規(guī)約，但新的問(wèn)題接踵而至?！坝脩敉ǔＪ褂米匀徽Z(yǔ)言描述系統(tǒng)設(shè)計(jì)，F(xiàn)M-Agent 生成的規(guī)約也是自然語(yǔ)言，而傳統(tǒng)形式化驗(yàn)證器只支持基于數(shù)學(xué)公式的推理，二者存在巨大的語(yǔ)義鴻溝?！倍『迫槐硎尽?/p>

針對(duì)這一問(wèn)題，研究團(tuán)隊(duì)發(fā)現(xiàn)了一個(gè)關(guān)鍵事實(shí)：LLM 對(duì)于小段代碼的執(zhí)行結(jié)果預(yù)測(cè)極其精準(zhǔn)。結(jié)合 LLM 對(duì)代碼和自然語(yǔ)言的理解能力，F(xiàn)M-Agent 大膽泛化了霍爾邏輯中的推理規(guī)則，讓 LLM 直接基于自然語(yǔ)言規(guī)約對(duì)函數(shù)的正確性進(jìn)行邏輯推理。

圖丨基于自然語(yǔ)言的代碼正確性推理示例（來(lái)源：arXiv）

如上圖所示，F(xiàn)M-Agent 逐段推理代碼執(zhí)行后的程序狀態(tài)描述（注釋部分），即后置條件，一直推理到函數(shù)返回，檢查最終的程序狀態(tài)描述是否違背了規(guī)約里對(duì)最終程序狀態(tài)的要求。

這種方法結(jié)合了霍爾邏輯的推理規(guī)則和 LLM 強(qiáng)大的語(yǔ)義理解能力，實(shí)現(xiàn)了對(duì)大規(guī)模代碼的“找茬”。

表丨智能體自動(dòng)生成的大規(guī)模系統(tǒng)（來(lái)源：arXiv）

為了驗(yàn)證 FM-Agent 的實(shí)戰(zhàn)能力，研究團(tuán)隊(duì)對(duì)四款由 Claude Opus、GPT Codex 等頂尖編程智能體生成的大規(guī)模系統(tǒng)進(jìn)行了正確性推理。

表丨FM-Agent 在大規(guī)模軟件中找到的 bug 數(shù)量（來(lái)源：arXiv）

這些系統(tǒng)此前已經(jīng)過(guò)開(kāi)發(fā)者的單元測(cè)試、集成測(cè)試、差分測(cè)試甚至多智能體交叉代碼審查等。然而，F(xiàn)M-Agent 在這些“層層設(shè)防”的堅(jiān)固堡壘中，依然挖出了 522 個(gè)新 bug。

除了導(dǎo)致系統(tǒng)崩潰、結(jié)果錯(cuò)誤這種顯性問(wèn)題，F(xiàn)M-Agent 還發(fā)現(xiàn)一些更深層的邏輯隱患。例如，編譯器 CCC 中發(fā)現(xiàn)的一些 bug 會(huì)導(dǎo)致代碼雖然可以正常編譯，但是代碼的執(zhí)行結(jié)果卻是錯(cuò)的。這種“無(wú)聲無(wú)息”的 bug 不會(huì)導(dǎo)致系統(tǒng)崩潰或任何明顯異常，但危害極大且難以被察覺(jué)。

（來(lái)源：arXiv）

當(dāng)前編程智能體之所以會(huì)引入這種“細(xì)思極恐”型 bug，很可能與其訓(xùn)練數(shù)據(jù)中包含了類似的錯(cuò)誤代碼有關(guān)。陳海波指出，未來(lái)若想進(jìn)一步提升編程智能體生成代碼的可靠性，一個(gè)關(guān)鍵方向是對(duì)訓(xùn)練數(shù)據(jù)進(jìn)行更嚴(yán)格的篩選，盡可能使用正確無(wú)誤的代碼來(lái)訓(xùn)練智能體，這或許也是未來(lái) FM-Agent 的應(yīng)用場(chǎng)景之一。

此外，F(xiàn)M-Agent 還會(huì)基于推理過(guò)程提供的信息，自動(dòng)生成能觸發(fā) bug 的測(cè)試用例。例如對(duì)于編譯器 CCC，F(xiàn)M-Agent 會(huì)生成 C 程序作為測(cè)試用例，并將 CCC 的編譯結(jié)果與參考實(shí)現(xiàn)（例如 GCC）比較?！斑@種可復(fù)現(xiàn)的證據(jù)鏈，對(duì)于輔助理解和修復(fù) bug 非常重要。”王肇國(guó)表示。

在 LLM 時(shí)代，如何讓形式化方法的腳步快速跟上編程智能體的發(fā)展速度變得越發(fā)重要。FM-Agent 并非追求傳統(tǒng)形式化驗(yàn)證那種絕對(duì)完美的數(shù)學(xué)證明，而是利用 LLM 的推理能力在絕對(duì)嚴(yán)謹(jǐn)與工程可用之間找到一個(gè)絕佳平衡點(diǎn)。

隨著 FM-Agent 這類技術(shù)成熟，未來(lái)的軟件工程范式可能會(huì)發(fā)生根本性變化。人類開(kāi)發(fā)者的核心工作流有可能會(huì)變?yōu)椋菏紫扔扇擞米匀徽Z(yǔ)言對(duì)整個(gè)系統(tǒng)編寫設(shè)計(jì)文檔，之后由 AI 根據(jù)設(shè)計(jì)文檔生成代碼，然后 AI 對(duì)代碼找 bug 并自動(dòng)修復(fù)。

人將從“編寫-調(diào)試-修復(fù)”的循環(huán)中解放出來(lái)，轉(zhuǎn)移到需求分析與系統(tǒng)設(shè)計(jì)上，設(shè)計(jì)文檔的質(zhì)量直接決定了 AI 生成代碼的準(zhǔn)確性和可維護(hù)性。

新的軟件開(kāi)發(fā)流程可能給軟件工程的教育和人才培養(yǎng)領(lǐng)域帶來(lái)顛覆性的改變。當(dāng)前的培養(yǎng)課程重點(diǎn)是編程語(yǔ)言、數(shù)據(jù)結(jié)構(gòu)、算法實(shí)現(xiàn)、調(diào)試技巧等，在“AI 生成+驗(yàn)證”的范式下，這些傳統(tǒng)能力大部分可能不再是核心的培養(yǎng)目標(biāo)。因此，抽象建模能力、領(lǐng)域知識(shí)深度、系統(tǒng)思維、思辨能力等將變得越來(lái)越重要。

研究團(tuán)隊(duì)認(rèn)為，隨著形式化方法的不斷進(jìn)步，形式化驗(yàn)證的下一個(gè)“圣杯”是貫穿軟硬件全棧的端到端保證。這涉及多個(gè)大規(guī)模系統(tǒng)的正確性保障，而操作系統(tǒng)內(nèi)核正是全棧中的關(guān)鍵一環(huán)。完全自動(dòng)化的操作系統(tǒng)內(nèi)核驗(yàn)證，可以視作通往軟硬件全棧端到端保證的重要里程碑。

在 20 世紀(jì) 60 年代，托尼·霍爾提出了今天形式化驗(yàn)證的重要基石——霍爾邏輯，然而直到他今年逝世前，形式化驗(yàn)證仍然囿于人力成本，難以擴(kuò)展至大規(guī)模軟件中。

FM-Agent 提出了首個(gè)面向大規(guī)模系統(tǒng)的全自動(dòng)組合式推理框架，回應(yīng)了這份夙愿，也為形式化方法卸下“屠龍術(shù)”的沉重鎧甲，大步走向千行百業(yè)開(kāi)辟了一條全新的道路。當(dāng) AI 負(fù)責(zé)寫代碼，另一個(gè) AI 負(fù)責(zé)證明它是對(duì)的，軟件工程的核心問(wèn)題，正在被重新定義。

參考資料：

1.相關(guān)論文：https://arxiv.org/abs/2604.11556

2.FM-Agent源碼：https://github.com/haoran-ding/FM-Agent

3.FM-Agent網(wǎng)站：https://fm-agent.ai/

排版：劉雅坤