摘要： Mistral 於 2026 年 7 月 2 日推出 Leanstral 1.5，採 119B 總參數、約 6B 激活的稀疏架構並以 Apache-2.0 開放權重。官方稱 miniF2F 驗證與測試集全數破解，PutnamBench 完成 587/672，每題成本約 4 美元。這讓大規模重複取樣的形式驗證更具可行性，但成績仍出自官方公告。
2026 年 7 月 2 日，Mistral 推出 Leanstral 1.5，這回的標語是「Proof abundance for all」——讓證明成為人人都享得的富足。距離 3 月問世的初代 Leanstral，這是頭一次大規模翻新：採稀疏 MoE 結構，總參數 119B，每個 token 實際啟用的只有約 6B，權重以 Apache-2.0 授權完整公開。Hugging Face 模型卡 mistralai/Leanstral-1.5-119B-A6B 註明 256k 上下文，API 端點 leanstral-1-5 目前限時免費。
成長幅度看分數就懂。FLTEval 單次取樣，3 月的初代只拿 21.9；1.5 版則把 pass@1 抬到 28.9，pass@8 也從 31.9 一路升抵 43.2，就此越過 Claude Opus 4.6 的 39.6，花費卻只有約七分之一。miniF2F 的變化更要緊：驗證集、測試集全數破解，這條 Lean 4 證明工程的標準基準正式宣告飽和。
1.5 究竟動了哪裡
骨架照用初代的稀疏設計，這次翻新的力氣全下在訓練流程與環境。部署方式也沒變：權重抓回來自己架，或在 Mistral Vibe 裡以 vibe --agent lean 跑起來。模型卡把它寫成初代 Leanstral-2603 的直系升級，支援輸入文字與影像、輸出文字，但戰場僅此一個：Lean 4 證明工程。
三段式訓練，兩套 RL 環境
訓練流程拆成三段：中訓練打頭陣，監督微調居中，最後用 CISPO 演算法跑強化學習。RL 分在兩種環境進行。第一種叫「多輪證明」——模型不斷證出或推翻定理，跟著 Lean 編譯器的回饋一路修正，直到分出勝負或預算見底。第二種是「程式代理」——模型像工程師那樣直接在原始檔案系統上幹活：改檔案、跑 bash、呼叫 Lean 語言伺服器，接下「補齊整個儲存庫的證明」這類長時序工作，對錯則交由 Mistral 自己維護的 SafeVerify 分支把關。
分數盤點：miniF2F 滿分、PutnamBench 攻下 587
攤開數字。miniF2F 的驗證集、測試集統統 100%。PutnamBench 完成 587/672。FATE-H 解掉 87 題（87%）、FATE-X 解掉 34 題（34%），兩邊同步改寫各自基準的史上最佳。測試時擴展那條曲線同樣漂亮：PutnamBench 的 pass@8 在 5 萬 token 時是 44 題，20 萬 token 升至 244 題，100 萬 token 升至 493 題，400 萬 token 收在 587 題——只升不降，中途沒有半點停滯。
一題約 4 美元：成本帳
最扎眼的莫過於成本：Leanstral 1.5 處理一道 PutnamBench 題目，花費約 4 美元。其他人呢？Seed-Prover 1.5 開在高強度設定，估算每題要燒超過 300 美元（約等於每題 10 個 H20 天的算力），Aleph Prover 也落在 54 到 68 美元。這已經是一到兩個數量級的鴻溝。稀疏架構背後的產品邏輯正立足於此：證明搜尋靠大規模平行取樣餵養，單趟夠便宜，pass@k 這套玩法才成立。對形式驗證團隊來說，分水嶺就在這裡——從「偶爾試一把」跨到「天天狂跑」。
不只證明，還能抓蟲
兩個案例值得一書。頭一個：面對一套真實世界的 AVL 樹實作，模型把插入與刪除操作的 O(log n) 時間複雜度完整證了出來——過程吃掉超過 270 萬 token，歷經 22 次上下文壓縮，最終交出「每個高度單位 48 步、外加一個常數項」這個幾乎無法再收緊的邊界。第二個：把 Aeneas（將 Rust 翻成 Lean 的轉譯器）接上 Leanstral 組成一條管線，掃過 57 個儲存庫、點名 47 個遭違反的性質，其中 11 個確屬錯誤、5 個過去從沒人回報過——datrs/varinteger 的 zigzag 解碼符號函式在 Std.U64.MAX 上引爆的整數溢位就是其一。證明模型能逮到人類漏看的蟲，這條路徑比任何分數都更貼近「證明富足」的承諾。