ヨーロッパの人工知能企業Mistral AIは、最近数学の形式的証明を専門にしたモデル「Leanstral 1.5」を正式にリリースしました。このモデルはLean4プログラミング言語に特化しており、総パラメータ数は119Bですが、実際の推論時には6Bのパラメータのみがアクティブとなり、非常に低い計算コストで驚くべき証明能力を実現し、Apache-2.0ライセンスに基づいて完全オープンソースとなっています。

image.png

コア基準テストにおいて、Leanstral 1.5はほぼ完璧な結果を示しました。miniF2F形式数学基準の検証セットおよびテストセットで100%の完成率を達成し、PutnamBench数学コンテストの672問のLean4問題に対して587問を解決しました。抽象代数分野のFATEシリーズ基準において、修士レベルのFATE-Hでは87%、博士レベルのFATE-Xでは34%の達成率を記録し、両方の成績は現在の最高記録です。

問題解決のコストは競合の1％以下

より注目すべきは、Leanstral 1.5のコスト上の優位性です。PutnamBenchデータセットにおいて、このモデルは平均して1問あたり4ドルの解決費用で済む一方、ByteDanceのSeed-Prover 1.5は300ドル以上、Aleph Proverでも54～68ドルかかります。これは同程度の作業量において、Leanstral 1.5の推論コストが最も強力な競合の約1％であることを意味し、数学の形式的証明の大量利用における経済的な障壁を解消しています。

実際のエンジニアリングシーンにおいても、Leanstral 1.5は優れた実戦価値を示しました。テストされた57のコードライブラリで47個の不正属性を特定し、そのうち11個は実際のコード欠陥を指しており、さらに5個はGitHub上でこれまで報告されたことのない新たな問題でした。純粋な数学コンテストから現実的なソフトウェア工学検証に至るまで、このモデルはパラメータ規模が能力の唯一の基準ではないことを証明しています。効率的なアクティブ化こそがAI推論能力を実用に導く鍵であるということです。