IT之家 7 月 6 日消息，歐洲人工智能企業(yè) Mistral AI 當(dāng)?shù)貢r(shí)間本月 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)測(cè)試的驗(yàn)證集和測(cè)試集上均實(shí)現(xiàn)了 100% 的完成率；在 PutnamBench 數(shù)學(xué)競(jìng)賽問題集的 672 道 Lean 4 問題中可解決 587 道；對(duì)于 FATE 系列抽象代數(shù)基準(zhǔn)測(cè)試，其在碩士級(jí) FATE-H 上實(shí)現(xiàn)了 87% 的達(dá)成率，博士級(jí) FATE-X 達(dá)成率則為 34%，均為最佳表現(xiàn)。

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

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

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