Mistral AI開源數學證明利器：119B參數只激活6B，解題成本僅爲競品百分之一

歐洲人工智能企業Mistral AI近日正式推出面向數學形式化證明的專用模型Leanstral 1.5。該模型專爲Lean4 程序語言打造，總參數規模達119B，但實際推理時僅激活6B參數，以極低的計算開銷實現了驚人的證明能力，並以Apache-2. 0 許可完全開源。

在覈心基準測試上，Leanstral 1. 5 交出了一份近乎完美的答卷。它在miniF2F形式數學基準的驗證集和測試集上均實現了100%完成率，在PutnamBench數學競賽 672 道Lean4 問題中成功解決 587 道。對於抽象代數領域的FATE系列基準，碩士級FATE-H達成率87%，博士級FATE-X達成率34%，兩項成績均爲當前最佳。

解題成本僅爲競品百分之一

更令人矚目的是Leanstral 1. 5 的成本優勢。在PutnamBench數據集上，該模型平均每題解題開支僅需 4 美元，而字節跳動的Seed-Prover 1. 5 需要超過 300 美元，Aleph Prover也需要 54 至 68 美元。這意味着同等工作量下，Leanstral 1. 5 的推理成本僅爲最強競品的約百分之一，爲數學形式化證明的大規模應用掃清了經濟障礙。

在實際工程場景中，Leanstral 1. 5 同樣展現了不俗的實戰價值。模型在測試的 57 個代碼庫中標記了 47 個違規屬性，其中 11 個指向真實的代碼缺陷，更有 5 個是此前從未在GitHub上被報告過的全新問題。從純粹的數學競賽到真實的軟件工程驗證，這款模型正在證明一個事實：參數規模不再是能力的唯一門檻，高效激活纔是將AI推理能力推向實用的關鍵路徑。