近日， Mistral AI 正式發佈了專爲數學形式化證明語言 Lean4設計的開源模型 —— Leanstral1.5。該模型採用 Apache-2.0許可協議，以119B 的參數總量及6B 的激活參數，在兼顧高性能的同時大幅優化了使用成本。

作爲一款專注於數學推理的智能工具，Leanstral1.5的表現相當亮眼。在權威的 miniF2F 形式數學基準測試中，該模型在驗證集和測試集上均達成了100% 的完成率。面對極具挑戰性的 PutnamBench 數學競賽題庫，它能夠從672道 Lean4問題中成功解答587道。此外，在抽象代數領域的 FATE 系列基準測試中，它同樣展現了統治力:在碩士級別的 FATE-H 測試中達成率高達87%，即便是面對博士級別的 FATE-X 測試，其達成率也達到了34%，創下了該類模型的新紀錄。

image.png

成本優勢是此次模型發佈的另一大核心亮點。Mistral AI 強調，相比於市面上的其他方案，Leanstral1.5極大地降低了科研試錯成本。以 PutnamBench 中的題目爲例，使用 Leanstral1.5進行求解的平均成本僅爲4美元，而對比模型 Seed-Prover1.5的開銷超過300美元，Aleph Prover 的成本也處於54至68美元之間。這一顯著的成本壓縮，有望讓高精度的數學證明輔助技術走出實驗室，服務於更廣泛的科研羣體。

在實際的代碼開發場景中，Leanstral1.5也展現了極強的“找茬”能力。在對57個代碼庫的實測中，該模型成功識別出47個違規屬性，其中11個經覈實爲真實缺陷。尤爲值得一提的是，其中有5個漏洞此前從未在 GitHub 上被報告過，證明了 AI 在輔助程序驗證與安全審查方面的巨大潛力。

隨着 Leanstral1.5的開源，數學界與計算機科學界正迎來一個更低門檻、更高效的證明輔助工具。通過降低算力與經濟成本，該模型有望加速數學形式化證明的普及，助力科研人員從繁瑣的計算與覈對工作中解脫出來，專注於核心科學問題的突破。