重點摘要
形式驗證不再是學術奢侈品——$4 一題 Putnam 競賽數學，掃 57 個 repo 抓出 5 個真實 bug
119B MoE 架構每次僅啟動 6B 活躍參數，三階段訓練加 CISPO 強化學習，PutnamBench 672 題解出 587 題，miniF2F 雙滿分，FATE-H 碩士代數 SOTA。
每道 PutnamBench 題約 $4，競品 Seed-Prover 1.5 需 $300+，差距 75 倍。Apache 2.0 授權，免費 API 端點即可使用，MoE 架構支援本地部署。
掃出 Rust 函式庫 datrs/varinteger 的真實 overflow bug，社群質疑 fuzzing 也能做到；核心價值在功能安全、密碼學等傳統測試無法覆蓋的領域。
前情提要
章節一：Leanstral 1.5 的技術突破與 Lean 4 生態
Leanstral 1.5 是 Mistral AI 於 2026 年 7 月 2 日發布的開源形式驗證模型，採用 Apache 2.0 授權，針對 Lean 4 形式驗證語言量身打造。模型架構為混合專家 (MoE) ，總參數量 119B，但每次推論僅啟動 6B 個活躍參數，大幅降低本地部署門檻。
名詞解釋
Lean 4：一種交互式定理證明助手與函式式程式語言，可對數學陳述或程式邏輯進行機器可驗證的嚴格證明，近年被 AI 研究社群廣泛用於自動化數學競賽題目。
訓練分三層遞進：mid-training 讓基礎模型習得 Lean 4 語法與數學推理，supervised fine-tuning 進行指令對齊，再以 CISPO 演算法驅動強化學習。訓練同時涵蓋定理證明的多輪迭代（透過 Lean 編譯器即時回饋）與真實代碼代理環境（含檔案系統操作、bash 指令與語言伺服器整合），使模型跨越純數學與真實工程的邊界。
基準成績令業界矚目：miniF2F 驗證集與測試集雙滿分 (100%) ，PutnamBench 672 題解出 587 題，FATE-H 碩士級代數 87%(SOTA) ，FATE-X 博士級代數 34%(SOTA) 。FLTEval Pass@1 從前版 21.9% 提升至 28.9%，Pass@8 從 31.9% 升至 43.2%，全面刷新同類模型紀錄。
章節二：從數學證明到真實程式碼 Bug 的跨域能力
Mistral 讓 Leanstral 1.5 掃描 57 個真實開源 repo，發現 5 個先前未被回報的 bug，其中最具代表性的是 Rust 函式庫 datrs/varinteger 中 zigzag 解碼符號函式的整數溢位漏洞。The Decoder 的獨立報導確認了這項發現的真實性——模型不是只會解「紙筆數學題」，而是能在真實工程場景下識別隱藏缺陷。
名詞解釋
zigzag 解碼：一種整數編碼方式，將有號整數映射為無號整數以節省儲存空間，解碼時若邊界檢查不足易發生整數溢位，影響資料完整性。
模型在長推論鏈上的耐力同樣突出。在證明 AVL 樹 O(log n) 時間複雜度時，模型連續跨越 270 萬 tokens 與 22 次中間壓縮，完成結構歸納與單子時間追蹤。token 配額從 50k 擴至 4M 時，PutnamBench 解題數從 44 題躍升至 587 題，展現出強烈的 token budget 擴展性。
HN 社群對 bug 發現能力存在分歧。用戶 Groxx 指出，屬性測試模糊測試「幾乎肯定能在數秒內捕捉到」同樣的 bug，質疑是否真正超越現有工具。但 adev_ 重新定位其意義：形式證明的核心價值在功能安全、協議驗證、密碼學等傳統測試根本無法覆蓋的領域，兩者解決的是本質上不同的問題。
章節三：Mistral 的開源差異化策略與社群回響
Mistral 選擇以 Apache 2.0 完全開源，並提供免費 API 端點 (leanstral-1-5) ，配合低 active 參數設計 (6B) ，主打本地部署可行性。在成本面，Leanstral 1.5 每道 PutnamBench 題估計約需 $4，遠低於競品 Seed-Prover 1.5 的 $300+，呈現出 75 倍的明確經濟差異化優勢。
社群回應整體正面，但夾帶對 Mistral 近期競爭力的疑慮。HN 用戶 bjt12345 替 Mistral 辯護：「哪家沒有落後 frontier 模型？Grok、Meta……很多大公司都在掙扎。」moonset 則承認自己的比較框架有誤，表示對 Mistral 在形式驗證領域的工作真心感到興奮。
The Decoder 的報導強調，此次發布讓 Mistral 在形式數學基準上全面超越競品，是差異化戰略的具體成果——在 frontier 模型軍備競賽之外，Mistral 找到了一個技術護城河更深、競爭者更少的垂直賽道。
章節四：形式驗證自動化的產業前景與挑戰
Leanstral 1.5 的推出代表形式驗證工具從「學術研究專用」走向「工程實用」的重要里程碑。MoE 架構 (6B active params) 降低本地推論門檻，而 Lean 4 生態系正在成熟，從純數學證明延伸至 Rust、C 等系統語言的形式化驗證工具鏈。
挑戰仍然存在。形式化規格本身需人工撰寫，Lean 4 的學習曲線陡峭；目前 benchmark 已飽和 (miniF2F 100%) ，評估框架需隨能力一同演進。功能安全、協議驗證、密碼學等垂直領域是最具商業潛力的應用場景，但企業導入的主要阻力來自 Lean 4 技能缺口，而非模型能力本身。
核心技術深挖
Leanstral 1.5 的核心突破在於將形式驗證的多輪推理迴圈與真實工程環境無縫整合，三階段訓練賦予模型跨越「數學定理→程式碼修復」的雙棲能力。
機制 1：MoE 架構降低推論門檻
119B 總參數的模型在每次推論時僅啟動 6B 個活躍參數，這是混合專家 (MoE) 架構的核心優勢。相較於同等「感知規模」的稠密模型 (Dense) ，MoE 的每 token 計算量更小，使本地 GPU 部署成為可能，同時在記憶體效率上優於全參數激活的競品。
名詞解釋
混合專家 (MoE)：模型由多個「專家」子網路組成，每次前向傳播只路由到部分專家，大幅減少每 token 的浮點運算量，在參數規模與推論成本之間取得平衡。
機制 2：三階段訓練與 CISPO 強化學習
訓練分三層遞進：mid-training 讓基礎模型習得 Lean 4 語法與數學推理；supervised fine-tuning 進行指令對齊；最後以 CISPO 演算法驅動強化學習，讓模型在 Lean 編譯器回饋的多輪迭代中自我修正，強化「不放棄、持續推理」的長推論行為。
名詞解釋
CISPO：Mistral 自研的強化學習演算法，透過編譯器回饋信號 (proof success/failure) 優化模型在長推理鏈上的探索策略，類似 RLHF 但回饋來源是形式驗證器而非人類標注。
機制 3：Token Budget 擴展性
模型設計上支援 token 配額動態擴展：50k tokens 配額時僅解出 PutnamBench 44 題，擴展至 4M tokens 時達到 587 題。在證明 AVL 樹 O(log n) 複雜度的案例中，模型連續跨越 270 萬 tokens 與 22 次中間壓縮，完成結構歸納與單子時間追蹤，展示了形式驗證在長推論鏈下的實際可行性。
白話比喻
傳統 AI 像短跑選手，給 10 秒內的問題才能答好；Leanstral 1.5 更像馬拉松選手——給它 400 萬步的「思考空間」，它能連跑 22 個「驗證→修正」迴圈，把一道極難的數學證明從頭跑到尾。
工程視角
環境需求：Lean 4 + Mistral API
需要 Lean 4 工具鏈（elan 版本管理器 + lake 構建系統），以及 Mistral API 金鑰。免費端點 leanstral-1-5 無需付費即可測試；本地部署需能同時載入 MoE 6B active params 的 GPU 環境（建議 A100 或同等顯卡）。
最小 PoC
import mistralai
client = mistralai.Mistral(api_key="YOUR_API_KEY")
response = client.chat.complete(
model="leanstral-1-5",
messages=[
{
"role": "user",
"content": "Prove in Lean 4 that for all natural numbers n, n + 0 = n."
}
],
max_tokens=50000
)
print(response.choices[0].message.content)
驗測規劃
以 miniF2F 測試集中的 10 道基礎題作為 smoke test，預期 Pass@1 接近 100%。對高難度題目 (PutnamBench) ，建議 Pass@8 配置並設定 1M+ token 配額。真實代碼驗證場景需先將目標函式的型別規格寫成 Lean 4 theorem，再讓模型補全證明。
常見陷阱
- token 配額設太低 (< 100k) 導致模型在長證明鏈中途放棄，誤判為模型能力不足
- 未安裝 Lean 4 語言伺服器 (LSP) 導致編譯器回饋迴圈失效，proof search 退化為盲目生成
- 傳遞 Lean 3 舊語法觸發編譯器錯誤，需先確認
lean-toolchain版本對齊
上線檢核清單
- 觀測：proof success rate、平均 token 消耗量、timeout 比率
- 成本：API 用量監控（免費端點有 rate limit，大批量需評估付費方案）
- 風險：Lean 4 版本鎖定（
lean-toolchain檔案），避免語言伺服器版本漂移導致環境不一致
商業視角
競爭版圖
- 直接競品：Seed-Prover 1.5（DeepSeek 系，$300+／題）、Google DeepMind 的 Gemini 數學推理系統、OpenAI o4 用於數學競賽
- 間接競品：Coq/Isabelle 傳統定理證明助手、Dafny/F* 程式驗證工具、Coverity/KLEE 靜態分析與符號執行工具
護城河類型
- 工程護城河：CISPO 強化學習訓練方法、MoE 架構的推論效率優勢，加上 token budget 擴展性——在同等成本下目前無對手可完整複製此組合
- 生態護城河：Apache 2.0 授權吸引學術研究社群，Lean 4 生態系活躍開發者願意以此為基礎構建工具鏈，形成正向飛輪
定價策略
免費 API 端點策略是典型的開源引流模式：先以零成本降低嘗試門檻，等社群與工具鏈成形後再推出付費企業方案。與 Seed-Prover 1.5 的 $300+／題相比，$4／題的估算成本差距 75 倍，在學術與中小型企業市場具有壓倒性優勢。
企業導入阻力
- Lean 4 技術人才極度稀缺，多數企業沒有能撰寫形式規格的工程師
- 形式驗證的 ROI 不易量化，難以說服管理層批准導入預算
- 現有代碼庫缺乏形式化規格，從零開始補寫 Lean 型別規格工程量巨大
第二序影響
- Lean 4 工程師薪資預期走高，頂尖形式驗證研究者競爭加劇
- 航太、醫療嵌入式、密碼學合規場景將率先出現形式驗證外包需求
- miniF2F 等 benchmark 失去鑑別力後，產業需建立新評估標準，可能催生一批 benchmark 新創
判決：利基市場的強差異化（但主流導入仍需 2-3 年）
Mistral 在形式驗證這個高護城河垂直賽道成功卡位，成本優勢明確、開源策略正確，但短期天花板由 Lean 4 人才供給決定，而非模型能力本身。
數據與對比
數學形式化基準
- miniF2F（驗證集 + 測試集）：100%，雙滿分
- PutnamBench（672 題）：587 題通過（Pass@8，4M token 配額）
- FATE-H（碩士級代數）：87%(SOTA)
- FATE-X（博士級代數）：34%(SOTA)
FLT 費馬大定理評估 (FLTEval)
- Pass@1：28.9%（前版 21.9%，提升 +7.0pp）
- Pass@8：43.2%（前版 31.9%，提升 +11.3pp）
Token Budget 擴展性
token 配額 50k 時解 44 題；4M 時達 587 題，解題數呈現線性擴展潛力。與競品 Seed-Prover 1.5 相比，同等解題率下估算成本約 $4／題，競品約 $300+／題，差距約 75 倍。
最佳 vs 最差場景
推薦用
- 形式化驗證密碼學協議或功能安全規格（航太、醫療嵌入式），傳統測試工具無法給出機器可驗證保證的場景
- 自動化掃描開源 Rust/C 系統庫的型別安全與邊界條件 bug，補強現有靜態分析工具鏈
- Lean 4 教學與學術研究，以免費 API 端點加速定理證明流程，降低研究門檻
千萬別用
- 需要低延遲即時回應的生產環境（長推論鏈不適合 SLA < 1s 的場景）
- 一般 Python/JS 應用的日常 code review（fuzzing 和靜態分析更有效率且成本更低）
- 沒有 Lean 4 技術棧儲備的團隊，短期強行導入會被 Lean 學習曲線拖垮而非受益
唱反調
miniF2F 滿分意謂著這個 benchmark 已失去鑑別力，真正的技術邊界需要新的更難評估框架才能量化，當前成績更像是「清考題」而非能力極限。
掃描 57 個 repo 找到 5 個 bug 聽起來令人印象深刻，但社群已指出同等算力投入在 fuzzing 或靜態分析工具上，可能以更低成本找到更多、更危險的漏洞，形式驗證的 ROI 尚待驗證。
形式驗證自動化的瓶頸不在模型能力，而在 Lean 4 工程師的極度稀缺——即使模型能力再強，沒有人能撰寫形式規格，整條工具鏈仍然無法規模化。
社群風向
批評 Mistral 落後 frontier 模型，說實話有點可笑。首先，誰沒有落後過？Grok、Meta……很多大公司都在掙扎。其次，Mistral 試圖解決的是不同的問題。最後，Mistral 能在這場競賽中堅持這麼久，本身就值得恭賀。
抱歉，我意識到這些是不同等級的模型，本不應該這樣橫向比較。我對 Mistral 在這個領域的工作是真心感到興奮的！
Mistral AI 的 Leanstral 1.5 模型解出 PutnamBench 672 道題中的 587 道，代表在形式驗證推理能力上的重大突破。
這幾乎好得讓人難以置信……最吸引我注意的是：Leanstral-1.5-119B-A6B 承諾——讓 Leanstral 幫你完成任何程式設計任務，例如證明給定定理或修復你專案中的程式碼。它似乎真的有能力做到……
Mistral 發布 Leanstral 1.5 開源模型，專攻證明工程 (proof engineering) 領域。
炒作指數
行動建議
用免費 API 端點 `leanstral-1-5` 對現有 Rust/C 函式庫的核心函式撰寫 Lean 4 型別規格，讓模型自動補全安全性證明，體驗 token budget 擴展性。
將 Leanstral 整合進 CI pipeline——每次 PR 自動觸發高風險函式的形式驗證，發現邊界條件 bug，補強現有 fuzzing 工具鏈。
追蹤 Lean 4 工具鏈與 Leanstral API 的整合進展，以及社群是否建立針對工程場景的新 benchmark（超越 PutnamBench 和 miniF2F 的評估框架）。