123,123,123

最新預(yù)測(cè)：人工智能將使形式化驗(yàn)證成為主流

2025-12-17 14:25

關(guān)于人工智能將如何改變軟件開(kāi)發(fā)，人們已經(jīng)討論了太多維度：效率提升、代碼生成、自動(dòng)測(cè)試、低代碼乃至“人人都是程序員”。

但有一個(gè)關(guān)鍵變化，卻長(zhǎng)期被忽視——人工智能正在把形式化驗(yàn)證這一曾經(jīng)高度學(xué)術(shù)化、門(mén)檻極高的技術(shù)，推向軟件工程的現(xiàn)實(shí)主流。

近日，一篇由劍橋大學(xué)分布式系統(tǒng)研究員 Martin Kleppmann 撰寫(xiě)的博客講述了人工智能對(duì)形式化驗(yàn)證的推動(dòng)。

他在博客中表示，目前正有三個(gè)趨勢(shì)同時(shí)發(fā)生：

形式化驗(yàn)證的成本正在快速下降；
AI 生成的代碼迫切需要一種可替代人工審查的可靠機(jī)制；
形式化驗(yàn)證的確定性恰好彌補(bǔ)了大模型本身的概率性與不精確性。

這三者的疊加，很可能會(huì)把形式化方法從小眾研究領(lǐng)域，推向軟件工程的主流實(shí)踐。

真正的瓶頸，或許不再是技術(shù)，而是行業(yè)是否愿意更新認(rèn)知，接受一個(gè)全新的軟件開(kāi)發(fā)范式。

形式化驗(yàn)證的困境

形式化驗(yàn)證并不是新概念。數(shù)十年來(lái)，研究者已經(jīng)開(kāi)發(fā)出一系列證明助手和面向證明的編程語(yǔ)言，如 Rocq、Isabelle、Lean、F*、Agda 等。

這些工具允許開(kāi)發(fā)者為代碼寫(xiě)出精確定義的形式化規(guī)范，并通過(guò)嚴(yán)格的數(shù)學(xué)推理，證明程序在所有情況下都滿足這些規(guī)范——包括那些幾乎不可能通過(guò)測(cè)試覆蓋到的極端邊界條件。

借助這些工具，人類(lèi)已經(jīng)完成過(guò)一些“里程碑式”的工程實(shí)踐：例如經(jīng)過(guò)形式化驗(yàn)證的操作系統(tǒng)微內(nèi)核、C 語(yǔ)言編譯器以及密碼學(xué)協(xié)議棧。這些成果充分說(shuō)明，形式化驗(yàn)證在技術(shù)上是可行的，甚至在理論上近乎完美。

但問(wèn)題從來(lái)不在“能不能”，而在“值不值”。

長(zhǎng)期以來(lái)，形式化驗(yàn)證幾乎只存在于研究機(jī)構(gòu)和少數(shù)高安全等級(jí)項(xiàng)目中。即便是在醫(yī)療設(shè)備、航空航天等傳統(tǒng)意義上的高可靠軟件領(lǐng)域，工業(yè)界對(duì)形式化方法的采用也極為有限。根本原因在于：證明本身太難、太慢、太貴。

一個(gè)經(jīng)典案例是 seL4 微內(nèi)核。到 2009 年為止，該內(nèi)核的實(shí)現(xiàn)代碼只有約 8700 行 C 代碼，但為了完成形式化驗(yàn)證，卻投入了大約 20 人/年的時(shí)間，編寫(xiě)了超過(guò) 20 萬(wàn)行 Isabelle 證明腳本。

平均下來(lái)，每一行實(shí)現(xiàn)代碼，需要配套 20 多行證明，并耗費(fèi)接近半個(gè)工作日的人工成本。更重要的是，全球真正掌握這類(lèi)證明技能的人可能只有幾百人，這種知識(shí)高度依賴(lài)經(jīng)驗(yàn)與“行話”，幾乎無(wú)法規(guī)�；�。

從經(jīng)濟(jì)學(xué)角度看，這是一筆算不過(guò)來(lái)的賬。對(duì)絕大多數(shù)軟件系統(tǒng)而言，軟件缺陷帶來(lái)的預(yù)期損失，往往低于采用形式化驗(yàn)證所需的成本。更現(xiàn)實(shí)的一點(diǎn)是，軟件缺陷的代價(jià)往往由用戶承擔(dān)，而非開(kāi)發(fā)者本身。這使得形式化驗(yàn)證長(zhǎng)期處于“理論正確、實(shí)踐不劃算”的尷尬位置。

AI 改寫(xiě)形式化驗(yàn)證

這種格局，正在被人工智能打破。

近幾年，基于大模型的編程助手不僅在生成實(shí)現(xiàn)代碼方面突飛猛進(jìn)，也開(kāi)始在證明腳本的編寫(xiě)上展現(xiàn)出驚人的潛力。目前，這一過(guò)程仍然需要具備專(zhuān)業(yè)背景的人類(lèi)工程師進(jìn)行引導(dǎo)，但趨勢(shì)已經(jīng)十分清晰：隨著模型能力的提升，證明生成本身有望在未來(lái)幾年內(nèi)高度自動(dòng)化。

一旦證明的主要成本從“人類(lèi)專(zhuān)家”轉(zhuǎn)移到“機(jī)器計(jì)算”，形式化驗(yàn)證的經(jīng)濟(jì)學(xué)基礎(chǔ)將被徹底改寫(xiě)。驗(yàn)證不再是一項(xiàng)奢侈品，而可能成為軟件開(kāi)發(fā)流程中的常規(guī)步驟。

更重要的是，AI 不僅降低了形式化驗(yàn)證的成本，也制造了對(duì)形式化驗(yàn)證的剛性需求。當(dāng)越來(lái)越多的代碼由人工智能生成時(shí)，傳統(tǒng)的人工代碼審查將迅速成為瓶頸。相比讓人類(lèi)逐行檢查 AI 寫(xiě)出的程序，更合理的路徑是：讓 AI 為自己生成的代碼提供可驗(yàn)證的正確性證明。

如果一段代碼能夠被形式化地證明滿足其規(guī)范，那么它是否由人類(lèi)“手寫(xiě)”已經(jīng)不再重要。相比那些看似精巧、卻暗藏缺陷的“手工代碼”，一段附帶嚴(yán)格證明的 AI 生成代碼，反而更值得信任。

從這個(gè)角度看，證明腳本本身，可能正是大模型最理想的應(yīng)用場(chǎng)景之一。即便模型在推理過(guò)程中產(chǎn)生“幻覺(jué)”，也不會(huì)造成實(shí)質(zhì)性風(fēng)險(xiǎn)——因?yàn)槿魏尾怀闪⒌淖C明都會(huì)被證明檢查器拒絕，迫使模型重新嘗試。而證明檢查器本身是一小段經(jīng)過(guò)嚴(yán)格驗(yàn)證的核心代碼，幾乎不可能被繞過(guò)。

當(dāng)然，這并不意味著軟件世界將從此“零缺陷”。隨著證明過(guò)程被自動(dòng)化，真正的挑戰(zhàn)將前移到規(guī)范本身的定義：如何確保我們證明的，正是我們真正關(guān)心的屬性？形式化規(guī)范的書(shū)寫(xiě)依然需要經(jīng)驗(yàn)、判斷力與嚴(yán)謹(jǐn)思維。但即便如此，定義規(guī)范的成本，仍然遠(yuǎn)低于手工完成完整證明。

未來(lái)，人工智能甚至有可能參與規(guī)范的編寫(xiě)本身，在自然語(yǔ)言需求與形式化語(yǔ)言之間進(jìn)行轉(zhuǎn)換。雖然這一過(guò)程存在語(yǔ)義細(xì)節(jié)丟失的風(fēng)險(xiǎn)，但相較于當(dāng)前軟件工程中的不確定性，這是一種可管理、可校驗(yàn)的風(fēng)險(xiǎn)。

如果這一切成為現(xiàn)實(shí)，軟件開(kāi)發(fā)的范式將發(fā)生根本變化。開(kāi)發(fā)者只需要用高層次、聲明式的方式描述“代碼應(yīng)該具備什么性質(zhì)”，剩下的實(shí)現(xiàn)與證明過(guò)程交由 AI 完成。就像今天的程序員早已不關(guān)心編譯器生成的機(jī)器碼一樣，未來(lái)我們或許也不再需要閱讀具體實(shí)現(xiàn)代碼。

參考資料：

https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html