Mistralが自動定理証明向けAI「Leanstral 1.5」リリース、Lean 4の証明作業を支援

Mistral AIが数学の証明やプログラムの正しさを機械的に確かめる作業を支援するAIモデル「Leanstral 1.5」を2026年6月30日に公開しました。Leanstral 1.5は形式証明ツール「Lean 4」向けの自動定理証明と自動形式化に最適化されたモデルで、Mistral AIのLabs枠で無料利用できると案内されています。

Leanstral 1.5 - Mistral AI | Mistral Docs
https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06

Mistral ships Leanstral 1.5 for Lean 4 proof work, free in Labs | AI Weekly
https://aiweekly.co/alerts/mistral-ships-leanstral-15-for-lean-4-proof-work-free-in-labs

AIが生成した文章やコードは一見正しそうに見えても、細かい論理の飛躍や誤りが含まれることがあります。数学の証明やソフトウェア検証では小さなミスが大きな問題につながるため、Lean 4のような形式証明支援システムを使い、コンピューターが確認できる形で正しさを示す手法が使われています。

ただし、形式証明は便利な一方で書き方が独特です。人間が普段使う「明らかに成り立つ」「同じように証明できる」といった表現はコンピューターには通じず、証明の各ステップをLean 4が理解できる形に落とし込む必要があります。自然な数学の文章や仕様書をLean 4向けの記述に変換する作業は手間がかかるため、自動定理証明や自動形式化を助ける専用AIモデルが必要になるというわけです。

Leanstral 1.5は合計1190億パラメーターを持ち、処理時には65億パラメーターが有効になる混合エキスパート(MoE)方式を採用しています。コンテキスト長は256kトークンで、長い証明ファイルや関連コードをまとめて扱うことが可能。なお、Leanstral 1.5は2026年3月に公開されたLeanstralの後継モデルとなっており、元の3月版のモデルはLeanstral 1.5の登場と同時に入れ替わりで提供終了となりました。

信頼できるAIコーディングを実現するためのオープンソース証明検証基盤「Leanstral」をMistral AIがリリース、重大なボトルネック「人間によるレビュー」の克服を目指す - GIGAZINE

Leanstral 1.5の用途として示されている自動定理証明は、与えられた命題をLean 4上で証明する作業をAIが補助するものです。たとえば開発者が証明のゴールを入力すると、Leanstral 1.5が次に必要な証明手順を提案し、Lean 4側で正しさを確認する流れが想定されます。

もうひとつの用途である自動形式化は、人間が読める数学の説明や仕様をLean 4で扱える形式に変換する作業です。論文の一節やソフトウェアの仕様をそのまま検証に使うことはできないため、Lean 4が理解できる定義や定理へ書き直す必要があります。Leanstral 1.5が変換作業の負担を減らすことで、形式証明を専門家だけでなく実務の検証作業にも広げる可能性があります。

Leanstral 1.5はMistral AIのプレイグラウンドにて無料で試すことができます。「Chat Completions」「Function Calling」「Agents & Conversations」などのAPI機能にも対応しています。

なお、モデルカードには3月版からどの程度性能が向上したのかを示す新しいベンチマークは掲載されていません。Leanstral 1.5の登場を報じたAI Weeklyも新しい比較結果やウェイト公開方針はまだ確認できていないと述べています。