Mistral AI Releases Leanstral 1.5: An Apache-2.0 Lean 4 Code Agent Model Solving 587 of 672 PutnamBench Problems

Mistral AI 今日正式釋出 Leanstral 1.5，這是一款專為 Lean 4 證明助手打造的程式碼代理模型。該模型不僅以 Apache 2.0 授權開放權重，還同步上線了免費的 API 端點 leanstral-1-5。Leanstral 1.5 是先前 Leanstral-2603 的升級版本，屬於 Mistral Small 4 系列，目標鎖定自動定理證明與證明工程領域。 Leanstral 1.5 採用混合專家（MoE）架構，總共擁有 128 個專家子網路，但每次處理每個 token 僅啟動其中 4 個，因此總參數量雖達 119B，實際激活參數僅 6.5B，大幅降低運算成本。模型支援 256k token 的上下文長度，可接受文字與圖像輸入，輸出則為純文字。訓練過程分為三個階段：中期訓練、監督式微調，以及基於 CISPO 的強化學習。在強化學習階段，Mistral 設計了兩種環境：多輪環境中，模型需針對定理提出證明並根據 Lean 編譯器反饋反覆修正；程式碼代理環境則讓模型直接在原始檔案系統中編輯檔案、執行 bash 指令，並透過 Lean 語言伺服器即時獲取目標、錯誤與型別資訊，甚至能進行上下文壓縮以處理長時間任務。 在基準測試方面，Leanstral 1.5 表現亮眼。它在 miniF2F 驗證集與測試集上均達到 100% 的飽和成績；在 PutnamBench 上成功解決 672 題中的 587 題；在 FATE-H 與 FATE-X 代數基準上分別創下 87% 與 34% 的新最佳紀錄。針對 FLTEval（取自費馬最後定理儲存庫的真實 pull request），模型的 pass@1 從 21.9 提升至 28.9，pass@8 則從 31.9 躍升至 43.2，超越 Opus 4.6 的 39.6，且成本僅為其七分之一。 成本效益是 Leanstral 1.5 的另一大亮點。在 PutnamBench 上，每個問題的運算成本約為 4 美元，遠低於 Seed-Prover 1.5 high 設定下每個問題約 300 美元以上的花費（後者每個問題需耗費 10 個 H20 天）。與其他模型如 Goedel-Architect、AxProverBase 及 Aleph Prover（每個問題約 54 至 68 美元）相比，Leanstral 1.5 在性價比上具明顯優勢。模型還展現了測試時擴展的特性：提高每次嘗試的 token 預算，能顯著提升 PutnamBench 的 pass@8 成績——從 50k token 時的 44 題，一路攀升至 4M token 時的 587 題。 除了數學證明，Leanstral 1.5 在程式碼驗證上也展現實用價值。Mistral 團隊公開了兩個案例：其一，模型成功證明了一個真實 AVL 樹實作的 O(log n) 時間複雜度，該證明使用結構歸納與 TimeM monad，總共耗費超過 270 萬個 token，歷經 22 次上下文壓縮；其二，透過自動化流程將 Rust 程式碼轉譯為 Lean，Leanstral 推斷使用者意圖並生成正確性屬性，在 57 個開源儲存庫中標記出 47 個違反屬性的案例與 11 個真實 bug，其中 5 個是先前未在 GitHub 上回報的漏洞，例如 datrs/varinteger 中 zigzag 解碼的 sign 函式在輸入 Std.U64.MAX 時會因溢位導致崩潰或資料損毀。這些案例顯示，開發團隊可直接利用 Leanstral 1.5 在儲存庫內完成部分證明、自動生成函式的正確性屬性，或透過證明與反證推斷的不變量來壓力測試 Rust 程式碼。