[論文閱讀] 人工智能 + 軟件工程 | 用大語言模型架起軟件需求形式化的橋梁

用大語言模型架起軟件需求形式化的橋梁

論文信息

@misc{beg2025short,title={A Short Survey on Formalising Software Requirements with Large Language Models}, author={Arshad Beg and Diarmuid O'Donoghue and Rosemary Monahan},year={2025},eprint={2506.11874},archivePrefix={arXiv},primaryClass={cs.SE}
}

一段話總結

本文是關于利用大語言模型（LLMs）輔助軟件需求形式化的聚焦文獻綜述，介紹了從自然語言需求生成Dafny、C和Java等形式化規范的案例，如Laurel框架可生成超50%的Dafny輔助斷言。研究通過多個學術數據庫結合AI工具Elicit篩選文獻，將現有方法分為“僅提示”“提示+迭代”“微調”等類別，指出斷言生成可靠性高于完整契約合成，未來將聚焦提示工程、鏈思維推理及神經符號混合方法。

思維導圖

在這里插入圖片描述

研究背景：當自然語言遇上形式化驗證的鴻溝

想象一下，你讓朋友幫忙買杯咖啡，說"來杯冰美式，少糖"，結果收到一杯加了奶的熱咖啡——這就是自然語言歧義在日常生活中的小麻煩。而在軟件領域，這種歧義可能引發大問題：某自動駕駛系統的需求文檔中"緊急情況下優先制動"的描述，因缺乏形式化定義，可能導致系統在雨天濕滑路面誤判制動時機。

傳統上，解決這個問題需要將自然語言需求轉化為形式化規范（如Dafny、LTL邏輯公式），但這需要工程師同時掌握需求工程、形式化方法和定理證明，直接導致軟件開發周期延長30%。就像讓詩人同時成為數學家，既要懂"床前明月光"的意境，又要能推導微分方程。大語言模型（LLMs）的出現，就像給這位"詩人"配備了智能數學助手——既能理解自然語言的語義，又能生成嚴謹的形式化表達式，這正是本文研究的核心課題：如何用LLMs打通自然語言需求到形式化驗證的"任督二脈"。

創新點：LLM如何改寫需求形式化的游戲規則

這篇綜述的獨特價值在于，它首次系統梳理了LLM在軟件需求形式化中的"十八般武藝"，并揭示了三個顛覆性創新：

1. 自動化斷言生成的突破
傳統上，工程師需要手動為代碼添加斷言（如Dafny中的assert語句），而Laurel框架通過LLM能自動生成超50%的輔助斷言，就像IDE的智能補全功能突然學會了形式化邏輯。例如，在解析十進制字符串的Dafny函數中，LLM能自動生成"assert s1 + ‘.’ + s2 == [s1[0]] + (s1[1…] + ‘.’ + s2)"這樣的關鍵斷言，幫助驗證器理解字符串分解邏輯。

2. 神經符號方法的融合魔法
SAT-LLM等框架將LLM與邏輯求解器（SMT solver）結合，就像讓翻譯家與數學家合作：LLM理解需求語義，SMT solver驗證邏輯一致性。這種組合能以100%的精度檢測需求沖突，而單純使用ChatGPT的精度僅為60%左右。

3. 領域定制化的prompt工程
不同于通用LLM應用，文中提出的"雙階段提示法"（定位代碼缺失位置+提供斷言示例）如同給LLM戴上"領域眼鏡"，使硬件驗證斷言生成正確率達到89%。這就像讓GPT-4專門訓練成"需求形式化專家"，而不是萬能但不精的"百科全書"。

研究方法和思路：如何系統性探索LLM的形式化能力

文獻綜述的"三步淘金法"

數據庫地毯式搜索：在IEEE Xplore、ACM Digital Library等平臺用"LLM+軟件需求"等關鍵詞搜索，結果差異巨大（Google Scholar返回1.48萬篇，而IEEE Xplore僅17篇），突顯精準篩選的重要性。
AI助手初篩：用Elicit工具自動提取論文摘要和DOI，將人工篩選量減少70%，就像用搜索引擎過濾海量信息。
人工精挑細選：通過"是否涉及NLP與形式化方法結合"的標準，最終從數千篇文獻中鎖定35篇核心研究。

方法論的"五行分類法"

作者將現有研究分為五類，每類就像不同的"武器裝備"：

僅提示（Prompt-only）：直接用LLM生成規范，如GPT-3.5驗證代碼是否符合需求。
提示+迭代：通過"思考步驟"引導LLM，類似教孩子做題時逐步引導。
模型微調：針對需求形式化任務優化LLM參數，如SpecSyn框架使規范生成準確率提升21%。
驗證器集成：LLM與VeriFast等驗證工具聯動，實時檢查規范可驗證性。
神經符號混合：LLM與定理證明器結合，如Explanation-Refiner用LLM生成解釋，再用定理證明器驗證正確性。

案例研究的"顯微鏡觀察"

以Dafny斷言生成為例，研究團隊解剖了LLM的工作機制：

錯誤信息定位：通過Dafny驗證器的錯誤信息，確定需要添加斷言的代碼位置。
示例模式學習：給LLM提供代碼庫中的斷言示例，如"確保整數部分正確提取"的形式化表達。
增量驗證：生成的斷言會被插入代碼中，由Dafny自動驗證是否能解決原始錯誤。

典型案例與工具

工具/框架	應用領域	核心方法	效果數據
Laurel	Dafny斷言生成	定位代碼缺失位置+示例提示	生成超50%輔助斷言
AssertLLM	硬件驗證斷言	3個定制LLMs分階段處理	89%正確斷言率
SpecSyn	軟件規范合成	序列到序列學習	準確率比前代工具高21%
nl2spec	自然語言轉形式化	迭代細化翻譯	開源實現+Web界面

方法論分類

類別	特點	代表研究
僅提示（Prompt-only）	直接使用LLM，無額外調優	GPT-3.5驗證代碼
提示+迭代/人機交互	結合人工反饋或鏈式推理	nl2spec、Chain-of-Thought
微調（Fine-tuned）	針對任務優化LLM參數	SpecSyn、Req2Spec
神經符號（Neuro-symbolic）	LLM+邏輯推理工具	SAT-LLM（SMT solver）
驗證器集成（Verifier-in-loop）	LLM與驗證工具聯動	Lemur、Explanation-Refiner

關鍵研究發現

任務可靠性差異：斷言生成（如Laurel的50%、AssertLLM的89%）比完整契約合成（如GPT-4o生成的VeriFast規范常失敗）更可靠。
任務范圍影響：小范圍、明確任務（如單個斷言）LLM表現更優，復雜系統級規范需迭代優化。

主要貢獻：給領域帶來的三大實在價值

1. 建立需求形式化的"武器庫"

整理出35篇核心文獻的工具矩陣，從Laurel（Dafny斷言生成）到AssertLLM（硬件驗證斷言），再到nl2spec（自然語言轉時序邏輯），就像為工程師提供了"需求形式化工具超市"，可根據項目類型（如航天軟件、芯片設計）選擇合適的LLM工具。

2. 揭示任務成功的"黃金法則"

通過對比研究發現：斷言生成（如硬件驗證中的89%正確率）比完整契約合成（如Java建模語言JML的50%正確率）更易成功。這提示工程師應優先將復雜需求拆解為小顆粒度的斷言生成任務，如同將大工程拆分成可管理的子模塊。

3. 繪制未來研究的"藏寶圖"

明確指出三個高價值研究方向：

提示工程升級：用"鏈思維（CoT）"讓LLM分步推導，如先分析需求語義再生成邏輯公式。
人機協同進化：開發"需求形式化IDE"，讓工程師能實時糾正LLM生成的規范，類似程序員與AI結對編程。
安全關鍵領域深耕：針對自動駕駛等場景，將ISO 26262等安全標準嵌入LLM訓練數據，確保生成的規范直接滿足安全要求。

關鍵問題

問題1：LLMs在軟件需求形式化中的主要方法論有哪些？

答案：主要包括“僅提示”（直接使用LLM，如GPT-3.5驗證代碼）、“提示+迭代/人機交互”（結合人工反饋或鏈式推理，如nl2spec）、“微調”（針對任務優化LLM參數，如SpecSyn）、“神經符號”（LLM與邏輯推理工具結合，如SAT-LLM集成SMT solver）及“驗證器集成”（LLM與驗證工具聯動，如Lemur）。