Mistral 開源 Leanstral 1.5：6B 參數形式驗證模型，miniF2F 達 100%、自抓 5 個未公開 Rust bug

編按：本文綜合整理自 Mistral 官方部落格、Mistral Docs 模型卡、Hugging Face 模型頁、The New Stack，並加入 Siami 編輯部觀點與分析。

Mistral AI 於 2026 年 7 月 2 日發布 Leanstral 1.5，一個基於 Lean 4 證明助手的開源形式驗證代理模型，整份權重採 Apache-2.0 授權 在 Hugging Face 公開釋出。這是 Mistral 在「可驗證 AI」路線上的一次重要推進——在數學證明基準上表現大幅躍升，且能在真實 Rust 程式碼中主動找出過去未被回報的 bug。

模型架構與訓練機制

Leanstral 1.5 採用 Mixture-of-Experts（MoE）架構，總參數量 119B，但每次推論只啟動 6B 活躍參數，相當於在成本可控的前提下放大了模型容量。

訓練流程分為三個階段：

Mid-training（中期訓練）：在大量 Lean 4 證明資料上繼續預訓練
Supervised Fine-Tuning（監督微調）：以人類標註的證明步驟作為監督訊號
Reinforcement Learning with CISPO：用 CISPO（一種新型 RL algorithm for reasoning）強化證明與程式碼生成

訓練環境同時涵蓋兩個 RL 場景：

多輪證明環境：模型拿到定理陳述，要嘛證明、要嘛反證。提交證明後接收 Lean 編譯器的錯誤訊息，反覆修正直到成功或預算用盡。

程式碼代理環境：模型像開發者一樣直接在檔案系統中編輯檔案、跑 bash、呼叫 Lean 語言伺服器查詢目標與型態資訊，能處理長時間跨度的任務（如補完倉庫中未完成的證明）。

這種「讀編譯器錯誤並自我修正」的能力，是 Leanstral 1.5 在實戰中能可靠運作的關鍵。

benchmark 成績：miniF2F 飽和、PutnamBench 領先

在 4 個形式數學基準上，Leanstral 1.5 取得以下成績：

miniF2F（驗證+測試集）：100%（飽和）
PutnamBench：587 / 672（比 Seed-Prover 1.5 high 多解 7 題）
FATE-H（研究所代數）：87% state-of-the-art
FATE-X（博士代數）：34% state-of-the-art

成本面是更值得注意的數字：

每解一道 PutnamBench 問題，Leanstral 1.5 大約 $4
Seed-Prover 1.5 high 設定約 $300+（每題配 10 H20-day 預算）
Aleph Prover 介於 $54–$68 之間

Pass@8 on PutnamBench 隨 token 預算的擴展曲線（官方釋出數據）：

50k token：44 題
200k token：244 題
1M token：493 題
4M token：587 題

這條曲線證明 Leanstral 在長 context 下不是「撞牆放棄」，而是把預算直接轉成解出問題。其中 AVL-tree 證明跨 22 次 context compaction、跑了超過 270 萬 token。

真實世界程式碼驗證：自抓 5 個未公開 Rust bug

Leanstral 1.5 並不只會做數學題。它的實際殺手鐧是程式碼驗證 pipeline：

Aeneas 將 Rust 程式碼翻譯為 Lean
Leanstral 從程式碼推斷使用者意圖並產生正確性 property
嘗試證明（4 次）；若失敗，反過來證否定（4 次）
若雙向都失敗 → 標記為「可能違規」

在 57 個 Rust 倉庫的實測中，這條 pipeline 抓出 47 個違規 property，其中 11 個對應到真實 bug——5 個從未在 GitHub 被回報。

其中一個被命名為「zigzag decoding sign function」的 bug：當輸入為 Std.U64.MAX 時，(value + 1) 會溢位，造成 debug 模式 crash、release 模式靜默腐敗。這種邊界情境對 fuzzing 和測試來說通常都會漏掉。

// 經典溢出 bug pattern
fn zigzag_decode(value: u64) -> i64 {
    ((value + 1) / 2) as i64 * if value % 2 == 0 { 1 } else { -1 }
}

這個案例清楚展示，當形式驗證走完整個「編譯器錯誤 → 自我修正」循環，它能在測試與 fuzzing 都抓不到的角落找到缺陷。

🚨 為什麼這件事重要

形式驗證長期被視為「成本太高、產出太慢」的奢侈品——多半只用在性命攸關的航太、醫療、密碼學領域。Leanstral 1.5 把這個差距縮到幾個量級：

每題 $4 已逼近一般「呼叫 LLM 解題」的單位成本。這意味著中型軟體團隊可以例行性把核心 module 跑一輪形式驗證，不再是學術 demo 等級。
Apache-2.0 + Hugging Face 公開權重，等於企業與學界都可以本機部署，沒有資料外送顧慮。這跟 DeepSeek 的開源策略類似，但切入的是更專業的「證明工程」 niche。
跨學科可移植——同一個模型既能解 Putnam 競賽數學、也能驗證 Rust 程式正確性，證明 RL 在形式推理上的擴展性。

更重要的是時機點：2025 年 IMO（國際數學奧林賽）DeepMind DeepThink 拿下金牌、ByteDance Seed-Prover 拿下銀牌，業界正式承認「形式推理模型」是一個獨立賽道。Leanstral 1.5 是這個賽道第一個開源 + 成本合理的選項。

🚨 數據解讀與質疑

雖然 benchmark 數字漂亮，仍有幾個面向值得保留態度：

FLTEval 提升有限：從 21.9 → 28.9（pass@1），相當於每 5 道題多解 0.7 道。對開源社群是進步，但還沒到「取代人類審查」的程度。
5 個未公開 bug 樣本太小：57 個 repo、11 個 bug、5 個新，統計意義偏弱。要驗證 pipeline 是否真的有泛化能力，還需要更大規模、可重現的 benchmark。
「100% 飽和 miniF2F」 已是該基準天花板——這更像是研究結論，不是商業價值指標。要回答「能不能解 IMO 全新題」，得等獨立的第三方重現實驗。
HuggingFace 上的 Apache-2.0 並不代表訓練資料沒有 IP 爭議。HF 討論串已有研究員對類似的「全開源授權」提出質疑，使用前仍應實地查核。
Mistral 沒公開具體的訓練算力、資料來源、CISPO 細節，學術界想重現的門檻仍高。

Siami 觀點：把 Leanstral 1.5 視為「形式驗證進入日常開發工作流」的起點，比當成「AI 證明取代人類」更貼近現實。

怎麼開始用

權重下載：Hugging Face mistralai/Leanstral-1.5-119B-A6B
免費 API：leanstral-1-5 endpoint（Mistral La Plateforme / Labs）
官方推薦路徑：Mistral Vibe CLI + Lean LSP MCP server

# 1. 安裝 Mistral Vibe
uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup

# 2. 裝模型
/leanstall exit

# 3. 啟動 agent
vibe --agent lean

# 4. 加 Lean LSP MCP（選用）
# ~/.vibe/config.toml
[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

# 5. 開始證明

編按：實際部署環境請依 Mistral 官方 README 為準；以上是轉述文章步驟。