定理證明也開始卷成本：Mistral開源Leanstral 1.5，每題約4美元

據 動察 Beating 監測，Mistral AI 開源 Leanstral 1.5，一款面向 Lean 4 形式化證明的模型。模型總參數量 1190 億，激活參數約 65 億，采用 Apache-2.0 協議，並提供免費 API 訪問。官方評測顯示，Leanstral 1.5 在 PutnamBench 672 道題中解出 587 道；在抽象代數基準 FATE-H 和 FATE-X 上分別達到 87% 和 34%，刷新同類模型最佳表現。Leanstral 1.5 在 PutnamBench 上的平均解題成本約為 4 美元，低於此前部分系統數十至數百美元的成本。隨著單題 token 預算提高，它的解題數量持續增加；在 AVL 樹復雜度證明中，模型經過超過 270 萬 token 推理和 22 次上下文壓縮，最終完成相關證明。除數學證明外，Leanstral 1.5 還被用於代碼驗證。團隊在 57 個開源 Rust 倉庫中發現 11 個真實 bug，其中 5 個此前未被報告。