2026-07-04 02:53:25
Mistral 推出 Leanstral 1.5 用於形式化證明,將成本降至每個問題約 4 美元
根據 OneMillionAI 報導,Mistral AI 最近發布了 Leanstral 1.5,這是一個針對 Lean 4 的形式化驗證模型,總參數達 1190 億,活躍參數 650 億。該模型以 Apache-2.0 授權發布,並提供免費 API 存取。在 PutnamBench 上,Leanstral 1.5 解決每個問題的平均成本約為 4 美元,遠低於先前每個問題需花費數十到數百美元的系統。 該模型在 672 道 PutnamBench 問題中正確解答了 587 道,在抽象代數基準 FATE-H 上達到 87%,在 FATE-X 上達到 34%,創下同類模型的新效能紀錄。除了數學證明之外,Leanstral 1.5 也被應用於程式碼驗證,在 57 個開源 Rust 儲存庫中發現了 11 個真實漏洞,其中 5 個是先前未回報的。