MLNLP社群是國內外知名的機器學習與自然語言處理社群，受眾覆蓋國內外NLP碩博生、高校老師以及企業研究人員。

社群的願景是促進國內外自然語言處理，機器學習學術界、產業界和廣大愛好者之間的交流和進步，特別是初學者同學們的進步。

來源 |機器之心

研究團隊構成：香港科技大學、中國科學院軟體研究所、西安電子科技大學和重慶大學。團隊核心成員：香港科技大學的研究助理教授曹嘉倫，主要研究領域包括 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；
後續啟發與影響：基於三種基礎模型的微調模型均已開源；完整的執行上下文和自動驗證流程也將開源，這將有助於降低形式化驗證的門檻，減少人力消耗及部署成本。