在人工智能開始嘗試編寫核電站控制代碼和自動(dòng)駕駛系統(tǒng)代碼的今天，我們面臨一個(gè)關(guān)鍵安全問題：如何確保 AI 生成的程序絕對(duì)可靠？當(dāng)前主流 AI 系統(tǒng)存在根本性隱患：它們依賴人類編寫的測(cè)試用例進(jìn)行驗(yàn)證，但這種方法存在兩大致命缺陷。

首先，當(dāng)代碼復(fù)雜度增加時(shí)，所需的測(cè)試用例數(shù)量會(huì)呈指數(shù)級(jí)增長——即便是解決一道普通的 LeetCode 編程題，也需要數(shù)十個(gè)測(cè)試用例才能基本覆蓋。更嚴(yán)峻的是，這些測(cè)試無法窮盡所有代碼分支路徑，尤其難以發(fā)現(xiàn)深藏的邏輯漏洞。

上海人工智能實(shí)驗(yàn)室青年科學(xué)家付杰團(tuán)隊(duì)（Veri-Code Team）對(duì)此進(jìn)行了系統(tǒng)性研究，依托形式化語言（如 Dafny）直接生成可驗(yàn)證的代碼，以此判斷代碼行為是否符合人類意圖。團(tuán)隊(duì)在模型訓(xùn)練過程中使用強(qiáng)化學(xué)習(xí)，來減少大模型在可擴(kuò)展形式化軟件驗(yàn)證中對(duì)人類先驗(yàn)知識(shí)的依賴。

談及應(yīng)用落地的可能性，付杰對(duì) DeepTech 表示，該方法適用于確保醫(yī)療、金融、自動(dòng)駕駛和操作系統(tǒng)等安全關(guān)鍵領(lǐng)域的軟件沒有漏洞?！拔覀兛梢曰谠摲椒ㄩ_發(fā)一個(gè)類似 CodeRabbit 的插件，讓大模型生成的代碼自動(dòng)驗(yàn)證其正確性?！?/p>

圖丨付杰（來源：付杰）

近日，相關(guān)論文以《Re：Form——減少可擴(kuò)展形式化軟件驗(yàn)證中的人類先驗(yàn)知識(shí)：在 Dafny 中的初步研究》（Re：Form—Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny）為題發(fā)表在預(yù)印本網(wǎng)站arXiv上 [1]。

目前，該團(tuán)隊(duì)已經(jīng)將數(shù)據(jù)、代碼和模型開源 [2,3]。上海人工智能實(shí)驗(yàn)室實(shí)習(xí)生、清華大學(xué)交叉信息研究院姚班（已直博）顏川皓是第一作者，付杰擔(dān)任通訊作者。

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

驗(yàn)證危機(jī)在 AI 編程能力超越人類時(shí)，可能引發(fā)災(zāi)難性后果。正如最近一項(xiàng)研究所警示的那樣 [4]：當(dāng)前流行的長思維鏈（CoT，chain-ofthought）等非形式化推理方法，本質(zhì)上是在模仿人類不完美的思維模式，這將成為制約 AI 發(fā)展的認(rèn)知枷鎖。

要真正解決安全問題，必須從“給 AI 打安全補(bǔ)丁”（make AI safe）轉(zhuǎn)向“設(shè)計(jì)安全 AI”（make safe AI）——其中一個(gè)有效方法是建立數(shù)學(xué)定理級(jí)別的驗(yàn)證體系，而非依賴個(gè)案測(cè)試。

形式化定理驗(yàn)證器正是打開安全之門的“鑰匙”。以 Lean/Dafny 為代表的驗(yàn)證框架，通過數(shù)學(xué)邏輯引擎生成“無錯(cuò)誤聲明”（error-free statements）。這種聲明的可靠性達(dá)到數(shù)學(xué)定理級(jí)別，其真理性不因 AI 智能水平而變化——正如圖靈獎(jiǎng)得主約書亞·本吉奧（Yoshua Bengio）所言：“即使出現(xiàn)超級(jí)智能，定理依然為真?！?/p>

然而，現(xiàn)有方法陷入了依賴人類的困境：訓(xùn)練過程消耗海量人工標(biāo)注的 CoT，監(jiān)督信號(hào)易受主觀判斷干擾。當(dāng)面對(duì)復(fù)雜編程任務(wù)時(shí)，這種模式已接近崩潰邊緣——人類專家根本無法為每個(gè)任務(wù)提供足夠可靠的監(jiān)督信號(hào)。

例如，為 50 個(gè)初級(jí)程序編寫形式化規(guī)范需要兩名計(jì)算機(jī)科學(xué)家耗費(fèi) 220 小時(shí)，而驗(yàn)證 SeL4 操作系統(tǒng)內(nèi)核更是耗時(shí) 20 人年（注：相當(dāng)于 20 個(gè)人工作一年的時(shí)間）。

在構(gòu)建可驗(yàn)證 AI 系統(tǒng)的道路上，付杰與團(tuán)隊(duì)希望利用形式化定理驗(yàn)證器提供的保真的訓(xùn)練信號(hào)，以完全利用強(qiáng)化學(xué)習(xí)讓模型自主學(xué)習(xí)以生成基于形式化語言的代碼，從而實(shí)現(xiàn)可擴(kuò)展性（scale-up）。

正如強(qiáng)化學(xué)習(xí)領(lǐng)域奠基人之一里奇·薩頓（Rich Sutton）在《苦澀教訓(xùn)》（The Bitter Lesson）[5] 中提出的經(jīng)典觀點(diǎn)：人工智能發(fā)展史反復(fù)證明，試圖將人類思維模式硬編碼到系統(tǒng)中——無論這種設(shè)計(jì)短期內(nèi)多么有效，終將阻礙長期進(jìn)步。而真正的突破性進(jìn)展，永遠(yuǎn)來自基于搜索與學(xué)習(xí)的計(jì)算范式擴(kuò)展。

這一洞見直指當(dāng)前 AI 訓(xùn)練范式中人類先驗(yàn)的不可持續(xù)性這一缺陷：現(xiàn)有方法依賴人工標(biāo)注的 CoT 和由人類提供的結(jié)果監(jiān)督信號(hào)，本質(zhì)上是在強(qiáng)迫 AI 模仿人類的非形式化推理過程。

這不僅消耗海量人力資源（為復(fù)雜編程任務(wù)標(biāo)注可靠監(jiān)督信號(hào)已接近不可能），更嚴(yán)重的是——當(dāng) AI 生成能力達(dá)到超人類水平時(shí)，人類提供的監(jiān)督信號(hào)本身就可能包含錯(cuò)誤或認(rèn)知局限。這種模式完美復(fù)現(xiàn)了薩頓警示的困境：“研究者將自身知識(shí)植入智能體的做法，短期令人滿意，長期卻會(huì)扼殺進(jìn)步”。

付杰在研究過程中一直在探索一個(gè)問題：如何找到一條可以拓展訓(xùn)練、減少人類非必要的先驗(yàn)對(duì)訓(xùn)練的影響的道路（不是移除全部人類先驗(yàn)），同時(shí)整個(gè)過程在數(shù)學(xué)意義上絕對(duì)可以被自動(dòng)驗(yàn)證，以達(dá)到真正穩(wěn)定 aligned 的 human-in-the-loop 人機(jī)共同進(jìn)步（而不是強(qiáng)行把人類隨意放在這個(gè)過程中，成為系統(tǒng)瓶頸）？

這讓他想到美國 MIT 麥克斯·泰格馬克（Max Tegmark）教授提出的“數(shù)學(xué)宇宙假說”：如果能夠用數(shù)學(xué)描述一個(gè)結(jié)構(gòu)，那么這個(gè)結(jié)構(gòu)一定可以在某個(gè)多元宇宙中存在，即現(xiàn)實(shí)世界可以被數(shù)學(xué)很好地表達(dá)?！叭艋谶@個(gè)假設(shè)，那么我們就可以用形式化語言來描述世界，同時(shí)在形式化空間做推理：把真實(shí)世界和數(shù)學(xué)緊密聯(lián)系起來?！?/p>

從這個(gè)角度看，形式化定理驗(yàn)證器是個(gè)絕佳的獎(jiǎng)勵(lì)環(huán)境：通過客觀數(shù)學(xué)邏輯驗(yàn)證確保反饋信號(hào)絕對(duì)準(zhǔn)確，不受人類思維模式的影響。這是在形式化環(huán)境下進(jìn)行訓(xùn)練的本征優(yōu)勢(shì)：是一條可能的可拓展訓(xùn)練的道路。

同時(shí)，付杰意識(shí)到，雖然泰格馬克的假說描繪了用數(shù)學(xué)描述萬物的宏偉圖景，但在當(dāng)前階段，最具現(xiàn)實(shí)可行性和迫切價(jià)值的應(yīng)用領(lǐng)域無疑是軟件。軟件系統(tǒng)天然具備高度的形式化特征，能夠被精確地建模、用數(shù)學(xué)邏輯（如 Dafny 等工具所體現(xiàn)的）進(jìn)行嚴(yán)格規(guī)范和驗(yàn)證。

因此，他和團(tuán)隊(duì)將構(gòu)建可驗(yàn)證的、高可靠性的軟件系統(tǒng)確立為終極目標(biāo)。這不僅是對(duì)數(shù)學(xué)宇宙假說在特定領(lǐng)域可行性的實(shí)踐探索，更是利用形式化環(huán)境的本征優(yōu)勢(shì)——提供絕對(duì)客觀、無歧義的驗(yàn)證信號(hào)，來突破當(dāng)前依賴人類先驗(yàn)的 AI 訓(xùn)練范式，實(shí)現(xiàn)真正可擴(kuò)展（scalable）的“制造安全 AI”路徑的關(guān)鍵一步。

最近，隨著 Manus 等工具的流行，也暴露出一個(gè)問題：生成代碼很容易，但如何驗(yàn)證代碼的正確性卻是一個(gè)難題。隨著代碼規(guī)模和功能的不斷增加，代碼內(nèi)部結(jié)構(gòu)可能會(huì)變得極其復(fù)雜。這種復(fù)雜性可能會(huì)導(dǎo)致功能之間的相互影響，甚至限制代碼功能的進(jìn)一步擴(kuò)展。

這不僅是一個(gè)安全問題，更是功能本身的瓶頸。因此，對(duì)生成代碼進(jìn)行形式化驗(yàn)證是必要的：用形式化驗(yàn)證器來確認(rèn)代碼是否符合用戶意圖，以判斷代碼的正確性。

付杰指出，“我希望能夠?qū)浖M(jìn)行形式化驗(yàn)證。無論哪家公司生成的代碼，都可以根據(jù)用戶的需求判斷代碼是否與需求完全一致。這本質(zhì)上是將驗(yàn)證過程轉(zhuǎn)化為一個(gè)數(shù)學(xué)證明，確保其絕對(duì)正確。”

這一選擇基于形式化語言如 Dafny 在軟件工程場(chǎng)景，相比于其他場(chǎng)景具有獨(dú)特的優(yōu)勢(shì)：

第一，搜索空間壓縮。與數(shù)學(xué)證明工具 Lean 不同，Dafny 直接基于代碼邏輯。在驗(yàn)證過程中，其搜索空間比數(shù)學(xué)定理驗(yàn)證縮減數(shù)個(gè)數(shù)量級(jí)。這意味著模型能更高效地探索解空間邊界，加速能力進(jìn)化

第二，難度線性可度量。在數(shù)學(xué)證明中，一行證明可能蘊(yùn)含極其復(fù)雜的邏輯躍遷（例如，費(fèi)馬大定理的證明僅占半頁紙但需要數(shù)年才能理解）。而 Dafny 代碼行數(shù)與復(fù)雜度呈強(qiáng)線性關(guān)系——50 行代碼的任務(wù)必然比 30 行更具挑戰(zhàn)。這種特性可以像設(shè)計(jì)學(xué)校課程那樣，精準(zhǔn)實(shí)施漸進(jìn)式訓(xùn)練（Curriculum Learning）：從單行斷言驗(yàn)證到多模塊組合，步步為營地突破能力邊界。

第三，組合泛化試金石。Dafny 要求代碼必須符合模塊化結(jié)構(gòu)（函數(shù)/類/接口分離），這天然成為評(píng)估智能體組合能力的理想考場(chǎng)。當(dāng)模型學(xué)會(huì)將已驗(yàn)證的排序模塊、搜索模塊組合成新算法時(shí)，便展現(xiàn)出 Francois Chollet 在 ARC 競賽中強(qiáng)調(diào)的核心智能指標(biāo)——這種能力正是通向通用人工智能（AGI）的關(guān)鍵階梯。

圖丨 Re：Form 流程管道示意圖（來源：arXiv）

為了讓模型生成可被驗(yàn)證的代碼，Veri-Code 團(tuán)隊(duì)采取的方案是直接生成形式化語言（Dafny）編寫的代碼，和精準(zhǔn)描述代碼行為的規(guī)范（specification）并驗(yàn)證生成的規(guī)范是否等價(jià)于用戶意圖。為了大規(guī)模訓(xùn)練，團(tuán)隊(duì)大幅度減少人類先驗(yàn)對(duì)訓(xùn)練的干涉：摒棄人工標(biāo)注的 CoT 與結(jié)果評(píng)判，并拒絕任何依賴人類主觀判斷的獎(jiǎng)勵(lì)機(jī)制。

團(tuán)隊(duì)發(fā)現(xiàn)，讓模型直接輸出結(jié)果而完全不使用 CoT 是可行的，至少在研究中任務(wù)未受到影響。目前，他們也在考慮較短代碼和較局限的任務(wù)上是否可行。但需要了解的是，不使用 CoT 并不意味著對(duì)于更復(fù)雜的問題不需要 CoT。

圖丨不同獎(jiǎng)勵(lì)方案與正則化選擇下的訓(xùn)練曲線（來源：arXiv）

在具體實(shí)現(xiàn)中，Veri-Code 團(tuán)隊(duì)目前關(guān)注第一步：給定代碼實(shí)現(xiàn)（implementation），為該實(shí)現(xiàn)填寫規(guī)范（specification）?；谀壳艾F(xiàn)存關(guān)于 Dafny 代碼的數(shù)據(jù)非常少，并考慮到目前大模型輸出完整無誤的 Dafny 代碼的能力較差，他們通過對(duì)已有數(shù)據(jù)的利用清洗，設(shè)計(jì)了代碼翻譯的 pipeline。

從已有的 Python 源代碼中翻譯成可驗(yàn)證通過的 Dafny 代碼，來獲取訓(xùn)練數(shù)據(jù)，同時(shí)構(gòu)造了測(cè)試模型組合泛化能力的 Benchmark，名為 DafnyComp。考慮到模型需要學(xué)會(huì)基本的 Dafny 語法，研究團(tuán)隊(duì)對(duì) Qwen2.5-coder 進(jìn)行了初步的監(jiān)督微調(diào)（SFT，Supervised Fine-Tuning），當(dāng)模型的語法正確率達(dá)到 80% 后進(jìn)行強(qiáng)化學(xué)習(xí)訓(xùn)練。

圖丨 DafnyComp 基準(zhǔn)測(cè)試中的模型表現(xiàn)（來源：arXiv）

在強(qiáng)化學(xué)習(xí)訓(xùn)練中，除了最基礎(chǔ)的驗(yàn)證通過的 0/1 信號(hào)之外，為了提供更具信息量的獎(jiǎng)勵(lì)信號(hào)，同時(shí)為了防止模型通過輸出簡單語句進(jìn)行獎(jiǎng)勵(lì)破解（reward hacking）, 研究團(tuán)隊(duì)基于 Dafny 等形式化語言的特性（每個(gè)語句都是可驗(yàn)證的數(shù)學(xué)命題），通過分析規(guī)范間的偏序關(guān)系，開發(fā)了新的驗(yàn)證技術(shù)。

并由此提出了規(guī)范優(yōu)越率（SSR，specification superiority rate）的概念, 旨在衡量模型生成的規(guī)范（specification）是否比現(xiàn)有的 Ground Truth 更加優(yōu)越（比如對(duì)函數(shù)輸入的限制更少，對(duì)函數(shù)輸出的描述更嚴(yán)格等）。

付杰指出，這一度量的引入有利于其測(cè)量模型現(xiàn)有的規(guī)范質(zhì)量。同時(shí)將此度量作為獎(jiǎng)勵(lì)信號(hào)，訓(xùn)練后的模型顯著提升了生成的規(guī)范質(zhì)量。

在強(qiáng)化學(xué)習(xí)訓(xùn)練后，Re：Form 的全規(guī)模模型（0.5B-14B）在驗(yàn)證通過率和 SSR 上均超越了現(xiàn)有的 GPT-4o 和 Claude4 等閉源模型。而在 14B 模型在域內(nèi)驗(yàn)證和已有的 DafnyBench，以及該團(tuán)隊(duì)提出的 DafnyComp 上均超越了現(xiàn)有閉源模型。

（來源：arXiv）

“現(xiàn)在已有相關(guān)研究證明，自回歸的 Transformer 只有加上 CoT 才能模擬圖靈機(jī)，在此基礎(chǔ)上才有可能理解代碼的運(yùn)行過程?！备督鼙硎?。

在接下來的研究階段中，研究團(tuán)隊(duì)的重點(diǎn)是：一方面，探索是否能讓模型自己學(xué)會(huì) CoT，而非人類標(biāo)注；另一方面，目前可對(duì)幾百行代碼進(jìn)行驗(yàn)證，研究人員希望未來它能夠支持更長的、達(dá)到上萬行的代碼。

參考資料：

1.https://arxiv.org/abs/2507.16331v2

2.Code: https://github.com/Veri-Code/ReForm

3.Models & Data: https://huggingface.co/Veri-Code

4.https://arxiv.org/abs/2502.09192

5.http://www.incompleteideas.net/IncIdeas/BitterLesson.html

運(yùn)營/排版：何晨龍、劉雅坤