Leanstral 啟示錄：當 AI 學會讓編譯器糾錯，高可靠場景才真正開始
Mistral 的 Leanstral 1.5 不只是一個數學模型，它揭示了 AI 進入高可靠應用的關鍵路徑：不是追求更像人的直覺，而是建立一個由形式化語言、編譯器與驗證器構成的「生成—檢查—修正」閉環。這讓 AI 的產出能被機器嚴格證明，為軟體工程、數學甚至法律等領域帶來根本性的變革。
近期 Mistral 發布的 Leanstral 1.5，表面上是個數學證明模型，但我認為它真正揭示的，是生成式 AI 邁向高可靠應用的關鍵路徑。AI 的價值不在於一次就生成完美無瑕的答案，而在於它能產出可被機器驗證的內容，並在一個「生成—檢查—修正」的閉環中迭代。當 AI 的正確性不再依賴人類直覺，而是由形式化語言與編譯器來定義與保證時，我們才能真正信任它，將其應用於攸關性命的關鍵系統。
Leanstral 1.5：不只是另一個數學天才
2026 年 7 月 2 日，Mistral AI 發表了 Leanstral 1.5，一個基於 1190 億參數（119B）的混合專家模型（MoE），其活躍參數為 60 億（6B），並以 Apache-2.0 授權開源。從數據上看，它在多個數學基準測試中表現驚人，例如在 miniF2F 基準中達到 100% 的證明成功率，在極具挑戰性的 PutnamBench 上解決了 672 題中的 587 題。
然而，如果只把焦點放在這些數字上，就會錯過真正重要的變革。Leanstral 的特殊之處在於，它專為 Lean 4 這個形式化語言而生。
Lean 不僅僅是一種程式語言，它更是一個「互動式定理證明器」（Interactive Theorem Prover）。這意味著，當你用 Lean 寫下一段數學證明時，它的編譯器不僅僅是檢查語法錯誤，而是會嚴格驗證證明的每一步邏輯是否完全正確。只要存在任何瑕疵，編譯器便會直接拒絕通過。
這徹底改變了我們評估 AI 產出品質的方式：Leanstral 不再是單純的「寫作者」，而是能產生一種可被機器百分之百驗證的、結構化的邏輯陳述。這正是它與傳統 LLM 的根本區別。
為什麼「讓編譯器糾錯」比「一次寫對」更重要？
過去幾年，我們對大型語言模型的期待，大多圍繞著它能否像人類專家一樣，一步到位地給出高品質的答案。我們希望它寫出優美的文案、無懈可擊的程式碼、或是充滿洞見的分析。但這個路徑的根本限制是，產出的「正確性」最終還是得由人類來判斷，而人類的判斷既耗時又可能出錯。
證明 AI 的真正價值，不在於「一次就寫出正確的程式」，而在於「讓編譯器來指出錯誤」。
Leanstral 所代表的另一條路徑，則是將判斷正確性的權力交還給機器。這背後的核心思想，是一個可驗證的 AI 工作流程，可以拆解成一個清晰的閉環：
- 生成 (Generate)：由 Leanstral 這樣的模型，針對一個特定問題（例如一個數學猜想），生成一個用形式化語言（如 Lean 4）寫成的證明草稿。
- 檢查 (Check)：將這個草稿交給 Lean 編譯器進行驗證。這個過程是完全確定性（deterministic）且無情的。只要存在一個邏輯漏洞，編譯器就會回傳一個明確的錯誤訊息。
- 修正 (Correct)：模型接收到這個錯誤訊息後，將其作為新的輸入，理解失敗的原因，並生成一個修正後的新版本。這個過程會不斷重複，直到編譯器完全接受證明為止。
在這個閉環中，AI 不再是一個黑盒子般的「答案產生器」，而是一個與形式化系統協作的「探索者」。最終產出的成果之所以可信，不是因為我們相信 AI 的「智慧」，而是因為它通過了一個客觀、嚴格、可重複的驗證程序。它的正確性是由數學和邏輯本身來保證的。
如何將這個模式擴展到數學之外？
這個「生成—檢查—修正」的閉環模式，其潛力遠遠超出了純數學領域。任何可以被形式化語言描述和驗證的場景，都有可能因此迎來質變。這意味著我們終於有機會將 AI 應用於那些對可靠性要求極高的關鍵任務中。
- 軟體與硬體工程：在航空、醫療或金融領域，軟體或晶片的一個微小錯誤可能導致災難性後果。未來，AI 可以在 TLA+ 或 Coq 這類形式化驗證工具的監督下編寫關鍵程式碼，確保系統永遠不會進入死鎖、數據競爭等危險狀態。
- 智慧合約與法律：區塊鏈上的智慧合約一旦部署就難以修改，任何漏洞都可能造成鉅額損失。AI 可以用形式化語言起草合約，並由驗證器檢查是否存在已知的攻擊模式或邏輯矛盾，從源頭上杜絕風險。
- 機器人與自動化系統：我們可以為機器人的行為制定形式化的安全規範（例如「永遠不得進入危險區域」），並讓 AI 在這個框架內生成控制演算法。驗證器可以證明該演算法在任何情況下都不會違反這些安全規範。
Leanstral 的出現，標誌著一個重要的轉向：我們開始將 AI 從一個模仿人類模糊直覺的工具，轉變為一個能與精確、嚴格的形式化系統對話的夥伴。這或許不像讓 AI 寫詩或繪畫那樣引人注目，但我相信，這才是通往可信任、可治理、並能真正改變世界的 AI 的正確道路。
延伸閱讀
我是江中喬，專注於 AI Agent Architecture、Memory Governance 與 Cognitive Diversity，持續研究如何打造能夠長期協作、可信任且可治理的 AI 系統。