研究團隊構成：香港科技大學、中國科學院軟件研究所、西安電子科技大學和重慶大學。團隊核心成員：香港科技大學的研究助理教授曹嘉倫，主要研究領域包括 AI&SE、人工智能測試、形式化驗證等；中國科學院軟件研究所副研究員陸垚杰，主要研究領域包括大語言模型及其應用。

隨著 DeepSeek-R1 的流行與 AI4Math 研究的深入，大模型在輔助形式化證明寫作方面的需求日益增長。作為數學推理最直接的應用場景，形式化推理與驗證（formal reasoning and verification），也獲得持續關注。

然而，近期的形式化推理大模型大多只針對單一形式化語言模型，缺乏對多形式化語言、多形式化任務場景的深度探索。 

近日，由香港科技大學牽頭，聯合中科院軟件所、西安電子科技大學、重慶大學等單位，開源了一系列形式化推理與驗證大模型，僅用 7B，即可在相關任務上獲得與 671B 滿血版 DeepSeek-R1 相當的水平！

• 論文標題：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 和斯坦福大學等多所機構在去年年底的立場論文（Formal Mathematical Reasoning: A New Frontier in AI）中所指出的，多語言形式化驗證模型正日益成為業界發展的趨勢。

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

憑借大模型在語義理解、代碼自動生成等方面的優勢，引入該技術有望大幅加速驗證流程，從而有效降低人力成本并提升自動驗證效率。

形式化任務拆解

研究團隊首先對形式化驗證任務進行了分層拆解，從非形式化的自然語言輸入到可驗證的形式化證明（formal proof）或可檢測的模型（model checking）。在此基礎上，研究團隊將傳統的端到端形式化驗證流程細化為六個子任務，包括驗證需求分解、形式化規約片段生成、規約補全、填空，以及代碼到形式化規約的自動生成。

圖 1 形式化驗證任務拆解

這一過程可以與代碼生成（code generation）任務相對照：代碼生成任務旨在將自然語言描述的功能轉換為相應的代碼實現，而形式化證明生成或模型生成（formal proof/model generation）則將自然語言描述的驗證需求轉化為由形式化語言編寫的形式化證明（proof）或模型（model）。

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

研究團隊從 Github 收集了五種形式化語言的經過一系列數據收集、清洗與整理，最終得到了 14k 數據用于訓練微調（fm-alpaca），4k 數據用于測試（fm-bench）。

圖 3 數據準備過程

大模型在形式化細分任務上的能力對比

通過對五種形式化語言（Coq, Lean4, Dafny, ACSL, TLA+）在形式化證明寫作上六種細分能力對比，研究團隊獲得了一些有趣的發現。

從形式化任務的角度（如圖 4），未經微調的通用指令大模型更擅長從代碼生成形式化證明（準確率 43.57%），而不擅長從自然語言生成形式化證明（8.65%～10.61%），遠低于代碼生成任務（從自然語言生成編程語言如 Python）。

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

另外，研究團隊觀察到在形式化規約填空的任務中，較大規模的模型往往不及小規模模型。例如，70B 的 llama3.1-instruct 模型在填空（列「ProofInfill」）上的準確率僅為 8B 模型的一半。這一現象可能與這些模型的微調策略：指令模型被訓練得更擅長生成，而非填空。研究團隊還發現，盡管 70B 級規模模型填寫的形式化規約片段看似更加正確，但因常常包含額外的內容，導致「說多錯多」，因此最終的準確率反而不如小模型。

圖 4 驗證任務上的差異（微調前）

大模型在不同形式化語言上的能力對比

從形式化語言的角度看（見圖 5），大模型在 ACSL 上的效果最好（34.92%），Dafny 次之（15.92%）。研究團隊認為，原因可能在于：一方面，ACSL 語言的關鍵詞更貼近自然語言，其語法結構又類似于 C 語言，使得生成過程更為順暢；另一方面，ACSL 規約片段相對較短，而 Coq 和 TLA 等語言的規約片段較長，生成難度更大。

圖 5 還顯示，僅通過增加生成次數（從 1 次提升至 5 次），即可在不用微調的情況下，得到 10.82%～63.64% 的提升。之后，進一步結合上下文學習（in-context learning），可以進一步將準確率翻番（51.33%～532.83%）。

圖 5 形式化語言上的差異（微調前）

微調帶來的能力提升

接下來，研究團隊在 3 個 7～8B 的基礎模型（LLaMA-3.1，Qwen-2.5，Deepseek-coder-v1.5）上用 fm-alpaca（14k 數據），同時對比了普通的對話型指令微調數據集 tulu-v3 和 ultra-chat。

如圖 6，經過形式化數據 fm-alpaca 微調之后，大模型在各類形式化任務上均有明顯提升（模型名以「fma」為后綴的模型），性能幾乎翻倍。

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

有趣的是，當把形式化數據和對話型指令數據混合微調時，能進一步提升模型性能，從 21.79%（僅用 fm-alpaca 微調）提升至 23.75%（fm-alpaca + ultrachat）和 25.16%（fm-alpaca + tulu）。

圖 6 微調前后結果對比

對比圖 5 與圖 6 還可以發現，盡管增加迭代次數和上下文學習可以提升準確率，但仍比不上微調帶來的提升。

能力遷移探究

最后，研究團隊進一步探索了形式化數據微調對大模型數學、推理和編程等任務上的「遷移能力」。他們通過對比微調前后在上述任務上的表現差異，以驗證大模型能否通過形式化驗證能力訓練中習得推理、數學等「元能力」。

實驗結果令人驚喜：利用形式化數據（FM-Alpaca）進行微調后，模型在數學、推理、代碼任務上的平均性能平均性能提升達到了 1.37% 至 5.15%。

該觀察或為未來探索模型「元能力」、「能力遷移」提供啟發。

總結

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