Mistral AI、数式証明に最適化した119B MoEモデル「Leanstral 1.5」を公開

フランスのAIスタートアップであるMistral AIは、数学的証明や厳密なプログラム検証のための言語「Lean 4」に最適化されたAIモデル「Leanstral 1.5」を公開し、同社のLabs枠にて無料提供を開始した。本モデルは、これまで人間の専門家に依存していた数学記述の検証やコードの安全確認プロセスを自動化することを目指している。

1. 119BパラメータのMoEアーキテクチャと初代の廃止

Leanstral 1.5は、総パラメータ数1190億、アクティブパラメータ数65億（6.5B）の混合専門家（MoE）アーキテクチャを採用している。さらに256kトークンの広大なコンテキストウィンドウを備え、長い証明コードをまとめて処理できる。なお、本モデルの公開に伴い、2026年3月に公開された初代の「Leanstral」は提供を終了（廃止）した。

2. 「自動定理証明」と「自動フォーマライズ」の支援

本モデルは主に2つの役割を担う。1つは、人間が証明の目標を入力するとLean 4の文法に適合する証明手順をAIが提案する「自動定理証明」。もう1つは、人間の自然言語や数式で書かれた仕様書を、Lean 4が処理できるコード形式へと変換する「自動フォーマライズ」である。これにより、学術論文の検証などが大幅に容易になる。

3. APIアクセスと無料プレイグラウンドの提供

Leanstral 1.5はMistral AIのプレイグラウンドで試すことができるほか、API経由で「Chat Completions」「Function Calling」「Agents & Conversations」などの機能もサポートする。一方で、3月版からの具体的な性能向上の詳細を示すベンチマーク数値や、重みの公開方針については詳細がまだ明示されていない。

「Leanstral 1.5」の登場は、ソフトウェア開発の安全性を高めるための形式検証や、数学的な証明作業のハードルを下げる重要な一歩である。バグのないミッションクリティカルなシステムの構築において、AIが定理証明器（Lean 4）と連携して機能する機会が増えることで、ITインフラやセキュリティの信頼性向上に寄与することが期待される。

引用元：GIGAZINE