Mistral AI 推出 Leanstral 開源證明代理，專為 Lean 4 設計
Zach Anderson 2026年3月16日 19:13
Mistral 發布 Leanstral，一個用於 Lean 4 形式化驗證的 6B 參數 AI 代理，在 Apache 2.0 許可下以 1/15 的成本擊敗更大型模型。
Mistral AI 於2026年3月16日發布 Leanstral——首個專為 Lean 4 形式化驗證而建構的開源 AI 代理。這個 120B 參數模型僅運行 6B 活躍參數，並在 Apache 2.0 許可下發布，使生產級定理證明無需企業級預算即可使用。
為什麼這對加密貨幣重要？形式化驗證——證明程式碼確實按其聲稱的方式運作的數學證明——已成為保護智能合約和區塊鏈協議的黃金標準。DeFi 程式碼中的漏洞已造成數十億美元的損失。Leanstral 可能大幅降低尋求驗證安全性專案的門檻。
效能與成本權衡
Mistral 使用 FLTEval 對 Leanstral 進行基準測試，與專有和開源競爭對手進行比較，這是一個測試費馬最後定理形式化專案中實際證明工程任務的新評估套件。
數據令人驚豔。Leanstral 在 pass@2 下獲得 26.3 分，計算成本為 36 美元。Claude Sonnet 4.6 取得 23.7 分，但費用高達 549 美元——成本超過 15 倍，效能卻更差。即使在 pass@16 下，Leanstral 以 290 美元達到 31.9 分，成本仍不到 Claude Opus 4.6 的 1,650 美元價格的五分之一(儘管 Opus 在品質上以 39.6 分領先)。
與開源替代方案相比，效率差距進一步擴大。GLM5-744B-A40B 和 Kimi-K2.5-1T-A32B 儘管擁有 6-8 倍的活躍參數，仍停留在 16-20 分左右。Qwen3.5-397B-A17B 需要四次通過才能達到 25.4 分——Leanstral 僅用兩次就超越了。
技術架構
Leanstral 使用針對證明工程工作流程優化的稀疏專家混合架構。該模型透過 MCP(模型上下文協議)與 Lean 的語言伺服器協議整合，專門訓練以在 lean-lsp-mcp 工具中實現最大效能。
Lean 4 本身於 2023 年 9 月推出穩定版，並在數學形式化方面迅速普及。Mathlib 函式庫——一個龐大的數學證明集合——在同年成功移植到 Lean 4。像費馬最後定理的形式化證明等專案展示了該平台進行嚴肅數學工作的能力。
實際應用
Mistral 展示了 Leanstral 處理關於 Lean 4.29.0-rc6 重大變更的真實 Stack Exchange 除錯問題。該代理診斷出類型別名的定義相等性問題，並正確識別出將 def 替換為 abbrev 將恢復策略匹配。
該模型還展示了跨語言翻譯，將 Rocq(原 Coq)定義轉換為 Lean 4，同時保留證明語義並實現自訂符號。
存取選項
存在三種部署路徑：在 Mistral Vibe 中直接整合(使用 /leanstall 開始)、在 labs-leanstral-2603 的免費 API 端點進行限時回饋收集，或使用 Apache 2.0 權重進行自主託管部署。
對於區塊鏈專案而言，計算很直接。形式化驗證傳統上需要昂貴的審計公司或深厚的內部專業知識。一個能以每項任務 36-290 美元證明程式碼正確性的開源代理可能重塑協議處理安全性的方式——假設證明在生產條件下成立。
圖片來源：Shutterstock- mistral ai
- leanstral
- lean 4
- 形式化驗證
- 開源
