Mistral 正式推出 Leanstral 1.5，這是一次針對其開源代碼驗證工具的重大升級。Leanstral 1.5 採用 Apache-2.0 許可證發行，配備了 119 億參數的模型，其中 60 億參數處於活躍狀態。這次升級為形式代碼驗證帶來了顯著的性能提升，旨在讓嚴格的證明工程變得更加可達。作為一個專為 Lean 4 用戶設計的工具，Leanstral 1.5 將 AI 的力量帶入了數學證明與程式碼驗證的領域，使研究人員與工程師能夠更高效地進行複雜的形式驗證工作。
突破性基準測試成績
Leanstral 1.5 在多個知名的證明基準上取得了最先進的成績。該模型解決了 PutnamBench 中的 587 個問題（總共 672 個），飽和了 miniF2F 基準，並在 FATE-H 上達到 87%，在 FATE-X 上達到 34%。這些數字不僅代表了理論上的進步，更重要的是在實際應用中的驗證。在測試過程中，Leanstral 1.5 在 57 個開源儲存庫中發現了五個之前未知的 bug，證明了其在實際代碼驗證中的有效性。這種從理論基準到實際應用的轉變，標誌著 AI 輔助的形式驗證已經達到了可以在生產環境中發現真實問題的水平。
先進訓練管道的成果
Leanstral 1.5 的強大能力源於其先進的訓練管道，包括中期訓練、監督微調與使用 CISPO 方法的強化學習。這種多層次的訓練方法使得模型不僅在數學證明上表現出色，同時也展現出強大的代碼驗證技能。雖然訓練主要集中在數學領域，但該模型已經證明了其在跨領域應用中的適應性。這種方法的成功表明，針對特定領域進行深度優化的 AI 模型，能夠在該領域達到專家級別的性能。
開源與可達性的承諾
為了促進更廣泛的採用，Leanstral 1.5 完全開源，並可在 Hugging Face 上下載。此外，使用者還可以透過免費 API 進行實際的 Lean 4 證明工程工作。這種開放的方式降低了進入門檻，使得全球的研究人員與開發者都能夠利用這項先進的工具。開源發行不僅加速了社群的創新，也建立了一個協作的生態系統，讓更多人能夠貢獻改進與應用。
新聞資料來源
https://alternativeto.net/news/2026/7/mistral-launches-leanstral-1-5-with-major-performance-upgrade-in-formal-verification/
https://mistral.ai/news/leanstral-1-5/