Mistralが選んだ、次の専門分野は「証明」だった。
これまでOCR・コード・音声・安全分類とタスク別に専門モデルを揃えてきたMistralが、数学の形式証明に特化したLeanstral 1.5を新たに投入した。定理を一行ずつ人手で検証してきた研究者やエンジニアの負担を、AIに肩代わりさせるのが狙いだ。
OCR、コード、音声、安全
足りなかったのは「証明」だった
Mistralの専門モデル群は、これまで数学の形式証明だけを欠いていた。
Mistralはここ数年、「何でもこなす1つの巨大モデル」ではなく、タスクごとに特化した小型・専門モデル群を並べる戦略を取ってきた。文書のテキスト化にはMistral OCR、コード生成・エージェント作業にはCodestralとDevstral、音声の認識・合成にはVoxtral、有害コンテンツの検知にはModeration——というように、用途ごとに最適化したモデルを積み上げる構成だ。この並びに、形式証明（formal proof）専用のLeanstral 1.5が新たに加わった。
「形式証明」とは、数学の主張を人間の直感ではなく、Lean 4のような証明支援系(interactive theorem prover)の文法で一行ずつ機械的に検証できる形へ書き下すことを指す。従来、この作業は数学者が数週間から数ヶ月かけて手作業で行うものだった。証明の一歩ごとにコンパイラが正誤を判定してくれる一方、その一歩を思いつくのはあくまで人間の仕事——というのが長年の常識で、OCRやコード生成のように気軽に「AIへ任せる」対象にはなりにくい領域だった。
| 分野 | 担当モデル |
|---|---|
| OCR（文書のテキスト化） | Mistral OCR |
| コード生成・エージェント | Codestral / Devstral |
| 音声認識・合成 | Voxtral |
| 有害コンテンツ検知 | Moderation |
| 数学の形式証明 | Leanstral 1.5（新規） |
定理は、もう一行ずつ
人の手で確かめなくていい。
「生成して、検証する」を
機械の中で回す
形式証明AIに共通するのは、コンパイラという“採点者”を内側に持つ点だ。
一般のチャット用LLMは、答えが「それっぽく正しそうか」を最終的に人間が判断するしかない。これに対し形式証明AIは、生成した証明の一歩一歩をLean 4のコンパイラがその場で機械的に合否判定できる。誤りがあれば差し戻され、モデルは別の証明ステップを試す——この生成と検証の往復を、通るまで何度も回す。曖昧さの入り込む余地がほぼないぶん、正解かどうかを人間が目視で確認する手間そのものを減らせるのが強みだ。
中間学習
Lean 4のコードと既存の証明データを読み込ませ、証明言語としての基礎を積む段階。
教師ありファインチューニング
人間や既存モデルが書いた証明例から、証明の組み立て方そのものを学習する段階。
強化学習（CISPO）
コンパイラの合否判定を手がかりに、実際に通る証明を自力で組み立てられるよう鍛える段階。
Mistralによれば、Leanstral 1.5はこの中間学習→教師ありファインチューニング→CISPOによる強化学習という3段階を経て学習された。検証器（コンパイラ）からの合否フィードバックを直接の手がかりにできるのは、正解が一意に定まらない自然言語のタスクにはない、数学ならではの強みだ。
数字で見る Leanstral 1.5
miniF2Fベンチマークではほぼ全問を解き切り、大学数学オリンピック級の問題集PutnamBenchでは672問中587問を正答した。難関ベンチマークのFATE-H・FATE-Xでもそれぞれ87%・34%とトップクラスの成績を記録している。ライセンスはApache 2.0で、モデルの重みはHugging Faceから誰でも取得できるほか、無料のAPIエンドポイントとしても提供されている。公開後のテストでは、57件のオープンソースリポジトリを検証し、これまで見つかっていなかったバグを5件発見したとも報告されている。
効くのは、証明を書く仕事がある人だけ
一般的なチャット用途で出番が来ることは、ほぼない。
研究者・数学者
定理証明の下書きやLean 4への形式化を、人手より速く進められる。査読前に「本当に成り立つか」を機械的に確認する用途に向く。
金融クオンツ
リスクモデルや価格付けロジックの数学的な整合性を、形式検証で裏付けたい領域と相性がよい。誤りが直接損失につながる場面での採用が想定される。
一般の開発者
通常のアプリ開発やチャットボット用途では、Leanstral 1.5に触れる機会はほぼありません。CodestralやDevstralなど既存の専門モデルの方が、引き続き実務向きだ。
ニッチだからこそ、次に注目すべきこと
形式証明AIの実用化は、これまでDeepMindのAlphaProofのような研究プロジェクトが中心で、一般提供される専門モデルとしては珍しい部類に入る。Apache 2.0のオープンウェイトかつ無料APIという条件は、大学の研究室や金融機関の検証チームが「まず試す」ハードルを大きく下げる。当面の見どころは、Leanstral 1.5を使って外部の研究者がどんな未解決問題やソフトウェアのバグ検証に取り組み始めるか、そしてMistralが次にどの専門領域（物理シミュレーションや回路設計の形式検証など）へモデルを広げていくかだろう。
一方で、形式証明の市場そのものが小さいことは変わらない。Lean 4で証明を書く文化を持つのは、現状では一部の数学・計算機科学コミュニティに限られ、一般の開発チームがすぐに導入する類のツールではない。ベンチマークの高スコアも、あくまで既存の証明問題セット上での成績であり、未解決の新しい定理を自力で証明できる保証にはならない点には注意したい。汎用性の低さゆえに、「専門特化モデルを積み上げる」というMistralの戦略が今後も評価され続けるかは、この先の採用実績次第だろう。