IT之家 7 月 6 日消息，歐洲人工智能企業(yè) Mistral AI 當(dāng)?shù)貢r間本月 2 日宣布推出面向數(shù)學(xué)形式化證明程序語言 Lean 4 的 Leanstral 1.5 模型。該模型總共擁有 119B 參數(shù)，激活 6B 參數(shù)，以 Apache-2.0 許可開源。

Mistral AI 表示，Leanstral 1.5 模型在 miniF2F 形式數(shù)學(xué)基準(zhǔn)測試的驗證集和測試集上均實現(xiàn)了 100% 的完成率；在 PutnamBench 數(shù)學(xué)競賽問題集的 672 道 Lean 4 問題中可解決 587 道；對于 FATE 系列抽象代數(shù)基準(zhǔn)測試，其在碩士級 FATE-H 上實現(xiàn)了 87% 的達(dá)成率，博士級 FATE-X 達(dá)成率則為 34%，均為最佳表現(xiàn)。

Mistral AI 強調(diào)了新模型的成本優(yōu)勢：對于 PutnamBench 數(shù)據(jù)集中的問題，Leanstral 1.5 的平均解決開支僅有 4 美元，而 Seed-Prover 1.5 需要 300 美元以上，Aleph Prover 也需要 54~68 美元。

而在實際場景應(yīng)用中，Leanstral 1.5 在測試的 57 個代碼庫中標(biāo)記了 47 個違規(guī)屬性，其中 11 個指向了真實的缺陷，包括 5 個此前未在 GitHub 上被報告過的問題。

廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。