定理證明領域也開始自力更生：Mistral 開源 Leanstral 1.5，每條定理定價約 4 美元

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 個真實錯誤，其中 5 個是先前未報告的。 [感知打敗]