最近、Mistral AI は数学形式化証明言語 Lean4専用のオープンソースモデルである Leanstral1.5 を正式にリリースしました。このモデルは Apache-2.0 ライセンスで公開されており、パラメータ総数が119B、アクティベーションパラメータが6Bで、高性能を維持しながら使用コストを大幅に最適化しています。

数学推論に特化した知能ツールとして、Leanstral1.5 の性能は非常に目覚ましいものです。信頼性の高い miniF2F 形式的数学ベンチマークテストにおいて、このモデルは検証セットとテストセットでそれぞれ100% の完了率を達成しました。非常に難しい問題が含まれる PutnamBench 数学コンテスト問題集では、672問中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 のオープンソース化によって、数学界とコンピュータサイエンス界は、より低コストかつ効率的な証明補助ツールを迎えることになりました。計算力と経済的コストを低下させることで、このモデルは数学の形式化証明の普及を加速し、研究者たちが煩雑な計算や確認作業から解放され、核心的な科学的課題の突破に集中できるよう支援するでしょう。