研究團(tuán)隊(duì)構(gòu)成：香港科技大學(xué)、中國(guó)科學(xué)院軟件研究所、西安電子科技大學(xué)和重慶大學(xué)。團(tuán)隊(duì)核心成員：香港科技大學(xué)的研究助理教授曹嘉倫，主要研究領(lǐng)域包括 AI&SE、人工智能測(cè)試、形式化驗(yàn)證等；中國(guó)科學(xué)院軟件研究所副研究員陸垚杰，主要研究領(lǐng)域包括大語(yǔ)言模型及其應(yīng)用。

隨著 DeepSeek-R1 的流行與 AI4Math 研究的深入，大模型在輔助形式化證明寫作方面的需求日益增長(zhǎng)。作為數(shù)學(xué)推理最直接的應(yīng)用場(chǎng)景，形式化推理與驗(yàn)證（formal reasoning and verification），也獲得持續(xù)關(guān)注。

然而，近期的形式化推理大模型大多只針對(duì)單一形式化語(yǔ)言模型，缺乏對(duì)多形式化語(yǔ)言、多形式化任務(wù)場(chǎng)景的深度探索。 

近日，由香港科技大學(xué)牽頭，聯(lián)合中科院軟件所、西安電子科技大學(xué)、重慶大學(xué)等單位，開(kāi)源了一系列形式化推理與驗(yàn)證大模型，僅用 7B，即可在相關(guān)任務(wù)上獲得與 671B 滿血版 DeepSeek-R1 相當(dāng)?shù)乃剑?/strong>

• 論文標(biāo)題：From Informal to Formal–Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
• 論文鏈接：https://arxiv.org/abs/2501.16207
• Hugging Face 模型鏈接：https://huggingface.co/fm-universe

正如 Meta FAIR 和斯坦福大學(xué)等多所機(jī)構(gòu)在去年年底的立場(chǎng)論文（Formal Mathematical Reasoning: A New Frontier in AI）中所指出的，多語(yǔ)言形式化驗(yàn)證模型正日益成為業(yè)界發(fā)展的趨勢(shì)。

事實(shí)上，形式化驗(yàn)證（formal verification）不僅是計(jì)算機(jī)科學(xué)的核心問(wèn)題，也是形式化數(shù)學(xué)最直接的應(yīng)用之一。然而，由于其門檻高、人力消耗大和部署成本高，形式化驗(yàn)證的普及與推廣一直受到限制。

憑借大模型在語(yǔ)義理解、代碼自動(dòng)生成等方面的優(yōu)勢(shì)，引入該技術(shù)有望大幅加速驗(yàn)證流程，從而有效降低人力成本并提升自動(dòng)驗(yàn)證效率。

形式化任務(wù)拆解

研究團(tuán)隊(duì)首先對(duì)形式化驗(yàn)證任務(wù)進(jìn)行了分層拆解，從非形式化的自然語(yǔ)言輸入到可驗(yàn)證的形式化證明（formal proof）或可檢測(cè)的模型（model checking）。在此基礎(chǔ)上，研究團(tuán)隊(duì)將傳統(tǒng)的端到端形式化驗(yàn)證流程細(xì)化為六個(gè)子任務(wù)，包括驗(yàn)證需求分解、形式化規(guī)約片段生成、規(guī)約補(bǔ)全、填空，以及代碼到形式化規(guī)約的自動(dòng)生成。

圖 1 形式化驗(yàn)證任務(wù)拆解

這一過(guò)程可以與代碼生成（code generation）任務(wù)相對(duì)照：代碼生成任務(wù)旨在將自然語(yǔ)言描述的功能轉(zhuǎn)換為相應(yīng)的代碼實(shí)現(xiàn)，而形式化證明生成或模型生成（formal proof/model generation）則將自然語(yǔ)言描述的驗(yàn)證需求轉(zhuǎn)化為由形式化語(yǔ)言編寫的形式化證明（proof）或模型（model）。

圖 2 從代碼生成到形式化證明生成

研究團(tuán)隊(duì)從 Github 收集了五種形式化語(yǔ)言的經(jīng)過(guò)一系列數(shù)據(jù)收集、清洗與整理，最終得到了 14k 數(shù)據(jù)用于訓(xùn)練微調(diào)（fm-alpaca），4k 數(shù)據(jù)用于測(cè)試（fm-bench）。

圖 3 數(shù)據(jù)準(zhǔn)備過(guò)程

大模型在形式化細(xì)分任務(wù)上的能力對(duì)比

通過(guò)對(duì)五種形式化語(yǔ)言（Coq, Lean4, Dafny, ACSL, TLA+）在形式化證明寫作上六種細(xì)分能力對(duì)比，研究團(tuán)隊(duì)獲得了一些有趣的發(fā)現(xiàn)。

從形式化任務(wù)的角度（如圖 4），未經(jīng)微調(diào)的通用指令大模型更擅長(zhǎng)從代碼生成形式化證明（準(zhǔn)確率 43.57%），而不擅長(zhǎng)從自然語(yǔ)言生成形式化證明（8.65%～10.61%），遠(yuǎn)低于代碼生成任務(wù)（從自然語(yǔ)言生成編程語(yǔ)言如 Python）。

滿血版（671B）DeepSeek-R1 平均準(zhǔn)確率為 27.11%，而其他參數(shù)規(guī)模在 8B 至 72B 的模型平均準(zhǔn)確率僅介于 7.32% 與 18.39% 之間。

另外，研究團(tuán)隊(duì)觀察到在形式化規(guī)約填空的任務(wù)中，較大規(guī)模的模型往往不及小規(guī)模模型。例如，70B 的 llama3.1-instruct 模型在填空（列「ProofInfill」）上的準(zhǔn)確率僅為 8B 模型的一半。這一現(xiàn)象可能與這些模型的微調(diào)策略：指令模型被訓(xùn)練得更擅長(zhǎng)生成，而非填空。研究團(tuán)隊(duì)還發(fā)現(xiàn)，盡管 70B 級(jí)規(guī)模模型填寫的形式化規(guī)約片段看似更加正確，但因常常包含額外的內(nèi)容，導(dǎo)致「說(shuō)多錯(cuò)多」，因此最終的準(zhǔn)確率反而不如小模型。

圖 4 驗(yàn)證任務(wù)上的差異（微調(diào)前）

大模型在不同形式化語(yǔ)言上的能力對(duì)比

從形式化語(yǔ)言的角度看（見(jiàn)圖 5），大模型在 ACSL 上的效果最好（34.92%），Dafny 次之（15.92%）。研究團(tuán)隊(duì)認(rèn)為，原因可能在于：一方面，ACSL 語(yǔ)言的關(guān)鍵詞更貼近自然語(yǔ)言，其語(yǔ)法結(jié)構(gòu)又類似于 C 語(yǔ)言，使得生成過(guò)程更為順暢；另一方面，ACSL 規(guī)約片段相對(duì)較短，而 Coq 和 TLA 等語(yǔ)言的規(guī)約片段較長(zhǎng)，生成難度更大。

圖 5 還顯示，僅通過(guò)增加生成次數(shù)（從 1 次提升至 5 次），即可在不用微調(diào)的情況下，得到 10.82%～63.64% 的提升。之后，進(jìn)一步結(jié)合上下文學(xué)習(xí)（in-context learning），可以進(jìn)一步將準(zhǔn)確率翻番（51.33%～532.83%）。

圖 5 形式化語(yǔ)言上的差異（微調(diào)前）

微調(diào)帶來(lái)的能力提升

接下來(lái)，研究團(tuán)隊(duì)在 3 個(gè) 7～8B 的基礎(chǔ)模型（LLaMA-3.1，Qwen-2.5，Deepseek-coder-v1.5）上用 fm-alpaca（14k 數(shù)據(jù)），同時(shí)對(duì)比了普通的對(duì)話型指令微調(diào)數(shù)據(jù)集 tulu-v3 和 ultra-chat。

如圖 6，經(jīng)過(guò)形式化數(shù)據(jù) fm-alpaca 微調(diào)之后，大模型在各類形式化任務(wù)上均有明顯提升（模型名以「fma」為后綴的模型），性能幾乎翻倍。

值得注意的是，這種顯著提升僅用了 14k 條形式化相關(guān)的指令數(shù)據(jù)（instruction-response pairs）。

有趣的是，當(dāng)把形式化數(shù)據(jù)和對(duì)話型指令數(shù)據(jù)混合微調(diào)時(shí)，能進(jìn)一步提升模型性能，從 21.79%（僅用 fm-alpaca 微調(diào)）提升至 23.75%（fm-alpaca + ultrachat）和 25.16%（fm-alpaca + tulu）。

圖 6 微調(diào)前后結(jié)果對(duì)比

對(duì)比圖 5 與圖 6 還可以發(fā)現(xiàn)，盡管增加迭代次數(shù)和上下文學(xué)習(xí)可以提升準(zhǔn)確率，但仍比不上微調(diào)帶來(lái)的提升。

能力遷移探究

最后，研究團(tuán)隊(duì)進(jìn)一步探索了形式化數(shù)據(jù)微調(diào)對(duì)大模型數(shù)學(xué)、推理和編程等任務(wù)上的「遷移能力」。他們通過(guò)對(duì)比微調(diào)前后在上述任務(wù)上的表現(xiàn)差異，以驗(yàn)證大模型能否通過(guò)形式化驗(yàn)證能力訓(xùn)練中習(xí)得推理、數(shù)學(xué)等「元能力」。

實(shí)驗(yàn)結(jié)果令人驚喜：利用形式化數(shù)據(jù)（FM-Alpaca）進(jìn)行微調(diào)后，模型在數(shù)學(xué)、推理、代碼任務(wù)上的平均性能平均性能提升達(dá)到了 1.37% 至 5.15%。

該觀察或?yàn)槲磥?lái)探索模型「元能力」、「能力遷移」提供啟發(fā)。

總結(jié)

• 高質(zhì)量數(shù)據(jù)集構(gòu)建：研究團(tuán)隊(duì)構(gòu)建了包含 18000 對(duì)高質(zhì)量指令 - 響應(yīng)對(duì)的微調(diào)數(shù)據(jù)集（fm-alpaca）與評(píng)估集（fm-bench），覆蓋 5 種主流的形式化語(yǔ)言（Coq, Lean4, Dafny, ACSL, TLA+）和 6 種不同形式化推理與驗(yàn)證任務(wù)；
• 形式化任務(wù)分解與評(píng)估：將從非形式化的自然語(yǔ)言需求到形式化、可驗(yàn)證的證明的轉(zhuǎn)換過(guò)程細(xì)分為六個(gè)子任務(wù)，明確了每一步的目標(biāo)和挑戰(zhàn)，有助于精確定位大模型的能力瓶頸；
• 微調(diào)模型開(kāi)源：通過(guò)微調(diào)，7～8B 的小模型在生成形式化證明的能力得到顯著提升，模型的性能提高了近三倍，在評(píng)估任務(wù)上媲美 671B 滿血版 DeepSeek-R1；
• 后續(xù)啟發(fā)與影響：基于三種基礎(chǔ)模型的微調(diào)模型均已開(kāi)源；完整的執(zhí)行上下文和自動(dòng)驗(yàn)證流程也將開(kāi)源，這將有助于降低形式化驗(yàn)證的門檻，減少人力消耗及部署成本。