LLM 寫 TLA+ 還不夠準

30 個 LLM 的測試顯示，它們能產生像樣的 TLA+，但語意正確率仍很低，還不適合直接拿來寫正式規格。

• 研究機構：Loyola University Chicago
• 核心數據：語意正確率 8.6%
• 突破點：首次系統評估自然語言轉 TLA+

這篇論文直接回答了一個很實務的問題：你用白話描述系統，LLM 能不能把它寫成正確的 TLA+ 規格？答案很明確，至少現在還不行。模型有時候能寫出可解析的內容，但要通過形式驗證，還是常常失手。

這件事很重要，因為 TLA+ 本來就不是一般程式碼。它常被用在分散式與並行系統這類高風險場景。若 LLM 真的能幫忙起草規格，會省下很多入門成本；但如果它只是寫出看起來合理、實際語意錯掉的規格，風險反而更大。

這篇在解什麼痛點

寫 TLA+ 一直都難。它把時序邏輯、一階邏輯、集合論混在一起。也就是說，規格不只要語法正確，還要真的忠實描述系統行為。對工程師來說，最麻煩的不是打字，而是把需求、隱含假設、失敗模式、並行行為、以及一致性規則，翻成精確的數學語句。

LLM 之所以被拿來試，是因為它看起來很適合做這種「從自然語言到形式化表示」的轉換。既然它已經能處理不少程式任務，那能不能也幫忙寫 formal spec？問題在於，formal spec 比一般程式更嚴格。模型就算寫出能 parse 的內容，也可能漏掉公平性條件、弱化不變量，或少一個變數，整個系統語意就變了。

作者也點出資料量的問題。TLA+ 的公開語料遠少於主流程式語言，模型在訓練時接觸得少很多。這讓它比一般 code generation 更難，也解釋了為什麼「自然語言轉 TLA+」一直沒被好好系統化評估。

方法怎麼做

這篇論文建立了一個包含 205 份 TLA+ 規格的 benchmark，來源是 TLA+ Foundation。每份規格都配有自然語言註解和 TLC 設定，並切成 train、validation、test 三部分，用來評估模型能不能從白話生成 TLA+。

研究團隊一共測了 30 個 LLM，橫跨 8 個家族。包含 DeepSeek、LLaMA、Qwen、QwQ、GPT-OSS；也有偏 code 的模型，例如 CodeLLaMA 和 Granite；還有 instruction-tuned 模型，例如 Mistral、Phi、Gemma、Starling-LM；另外也測了 OpenAI GPT 與 Anthropic Claude 這類商用 API。核心掃描涵蓋 25 個開源權重模型，搭配 4 種 prompting 策略，共做了 2,600 次實驗。另有 5 個商用模型只做 few-shot 測試，共 130 次。

每個輸出都會檢查兩次。先用 SANY parser 看語法，再用 TLC model checker 看語意。這個分工很關鍵。語法只是在問「這是不是合法的 TLA+ 檔案」；語意則是在問「它有沒有真的描述對系統行為」。

論文也比較了不同 prompt 方式，並分析失敗模式。其中一個重點是 progressive prompting。根據這篇研究，這是唯一有產生語意成功的策略。作者也觀察模型大小是否有幫助，以及 code-specialized 訓練到底是加分還是扣分。

實際證明了什麼

最直接的結果是：目前的 LLM 不是可靠的 TLA+ 規格作者。整體來看，最佳語法正確率只有 26.6%，語意正確率最高也只有 8.6%。換句話說，模型就算生成出看起來像 TLA+ 的內容，大多還是過不了語意驗證。

另一個重要發現是，模型越大不代表越好。論文明確指出，模型大小無法預測品質，並舉出一個例子：DeepSeek r1:8b 在所有 prompting 策略下都比 70B 版本表現更好。作者因此認為，對 formal language 來說，比起單純堆參數，推理對齊更重要。

研究也發現，code-specialized 模型整體上不如 general-purpose 模型。作者把這歸因於來自主流程式語言訓練的 negative transfer。這對團隊很實用，因為很多人會直覺以為「既然是 code model，寫 formal spec 應該更強」，但在 TLA+ 這裡，情況可能剛好相反。

在失敗分析上，作者整理出五類常見幻覺：Unicode 運算子替換、跨語言語法注入、推理與格式洩漏、生成長度失準、以及結構性錯誤。這些問題被追溯到目前訓練資料的偏差，尤其是 code、formal math 和 reasoning samples 的分布。論文的核心意思不是 LLM 完全不能用，而是不能在沒有專家把關的前提下直接信任輸出。

對開發者的實際影響

如果你在做分散式系統、並行系統，或 verification-heavy 的基礎架構，這篇就是一個提醒。LLM 也許能幫你起草規格、打底、或先把描述整理成更像樣的格式，但它還遠不到「直接相信輸出」的程度。這裡最重要的落差，就是語法和語意之間的距離。

這也暗示了一種比較務實的工作流：把 LLM 當助手，不要當作者。它可以幫忙試寫、改寫、探索不同表述，或在迭代過程中提供草稿，但最後的 spec 還是要靠懂形式方法的人加上 checker 來收尾。從這篇結果看，只靠 prompt engineering 並不能補上核心缺口；就算是研究裡表現最好的 prompting 策略，也沒把語意問題解掉。

對工具開發者來說，作者提到兩個方向很明確：更高品質的 specification 資料集，以及 grammar-constrained generation。這很合理，因為他們觀察到的錯誤不是隨機雜訊，而是反覆出現的結構性失誤。若真的要讓 LLM 寫 formal spec，限制條件大概得比純文字 prompt 強很多。

也要注意限制。這篇摘要沒有公開完整 benchmark 細節到每個模型家族的完整數字，也沒有宣稱這份資料集能涵蓋所有 TLA+ 類型。雖然如此，這份研究仍然有價值，因為它是系統化、可重現的評估，而且測的是對的東西：不是能不能長得像，而是能不能在形式驗證下真的對。

為什麼這篇值得注意

這篇工作有價值的地方，在於它量到的是正確指標。很多 AI for code 的研究只停在表面可用，像是能不能 parse、能不能 compile。但對 TLA+ 來說，真正重要的是生成的規格有沒有真的符合意圖。這篇論文把問題往前推了一步，直接看 formal checking 的結果。

它也補上了一個研究空缺。先前和 GenAI、TLA+ 有關的工作，多半集中在從 code 生成 spec、限制語法，或用 spec 反過來引導 code generation。這篇則是直接挑更難的任務：從自然語言生成 TLA+。這讓它可以當成後續研究的 baseline，也是一個明確警訊：一般 LLM 的進步，並不等於已經解掉 formal specification。

作者表示，他們會釋出 evaluation framework、code、dataset、models 和 results，方便重現與後續研究。對工程師來說，這代表它不只是批評現況，而是提供了一個可以繼續往下做的起點。

結論很直接

目前的 LLM 有時候能寫出看起來像 TLA+ 的內容，但在語意層級仍然太不穩。若你的團隊想把 AI 用在 formal methods，這篇論文的答案很清楚：可以輔助，不能自動化。

• LLM 能產生 TLA+ 外觀，但語意正確率仍很低。
• Progressive prompting 有幫助，但無法解決核心問題。
• Formal spec 需要更強約束、更多資料與人工審查。