Mistral AI 釋出 Leanstral 1.5：Apache-2.0 許可的 Lean 4 程式碼代理模型，解決 PutnamBench 672 道問題中的 587 道

Mistral AI 今日釋出了 Leanstral 1.5，這是一款專為 Lean 4 打造的程式碼代理模型，主要面向自動定理證明和證明工程。模型權重以 Apache 2.0 許可開源，同時提供了免費的 API 端點 leanstral-1-5。

Leanstral 1.5 是之前 Leanstral-2603 模型的升級版，屬於 Mistral Small 4 系列。Lean 4 是一種證明助手，能夠機械地檢查每一步邏輯，可表達完美空間等物件以及 Rust 片段的性質。

架構方面，Leanstral 1.5 採用混合專家（MoE）設計，將每個令牌路由至少數專業子網路，從而在保持大容量的同時降低計算量。模型共有 128 個專家，每令牌啟用 4 個，總引數量 119B，每令牌啟用 6.5B，上下文長度 256k。輸入支援文本和影像，輸出僅為文本。

訓練分為三個階段：中期訓練、監督微調，以及使用 CISPO 的強化學習。兩個強化學習環境塑造了模型的代理行為：在多輪環境中，模型需給定定理並嘗試證明或反駁，根據 Lean 編譯器反饋逐步迭代；在程式碼代理環境中，模型在原始檔案系統中工作，可編輯檔案、執行 bash 命令，並使用 Lean 語言伺服器即時獲取目標、錯誤和型別資訊，從而完成部分證明、構建輔助引理，並透過上下文壓縮維持長任務。正確性由 Mistral 的 SafeVerify 分支驗證。

效能方面，Leanstral 1.5 在 miniF2F 驗證集和測試集上均達到 100%，解決了 PutnamBench 中 672 道問題中的 587 道。在 FATE-H 和 FATE-X 代數基準上達到新 SOTA（87% 和 34%）。在 FLTEval 上，pass@1 從 21.9 提升至 28.9，pass@8 從 31.9 提升至 43.2，且以七分之一成本超越 Opus 4.6。PutnamBench 上，Leanstral 以每問題約 4 美元的成本比 Seed-Prover 1.5 high 設定多解決 7 道問題，而後者每問題成本約 300 美元以上。測試時縮放是模型的核心特性，提高每個嘗試的令牌預算可提升效能。

實際應用中，Leanstral 證明了真實 AVL 樹的 O(log n) 時間複雜度，並發現了開原始碼中的錯誤：透過 Aeneas 將 Rust 翻譯為 Lean，自動推斷使用者意圖並生成正確性屬性，在 57 個倉庫中標記了 47 個違反屬性和 11 個真實錯誤，其中 5 個先前未報告。開發團隊可使用它完成部分證明、自動生成函式正確性屬性，或透過證明/反駁推斷不變數來壓力測試 Rust 程式碼。

使用方面，最簡單的途徑是 Mistral Vibe CLI，在免費計劃中啟用實驗模型即可。也支援自託管，需要 vLLM 0.24.0 及以上版本，並提供了詳細的部署命令。透過 OpenAI 相容客戶端呼叫，可設定 reasoning_effort 引數。此外，還支援 OpenAI 風格的函式呼叫和 lean-lsp-mcp 伺服器整合。