7月4日、Runtime Wireが「Mistral opens Leanstral 1.5 in a bet on machine-checked AI」と題した記事を公開した。MistralがLean 4向けの証明モデル「Leanstral 1.5」をApache-2.0ライセンスでオープンソース公開し、形式検証をAI製品戦略の中核に据えようとしている動きについて詳しく紹介されている。
Leanstral 1.5とは何か
Mistral AIは7月2日、Leanstral 1.5をリリースした。Lean 4向けの証明モデルで、Apache-2.0ライセンスのもとHugging Faceで公開されている。無料APIも提供される。
モデルのアーキテクチャは総パラメータ数1190億、アクティブパラメータ数60億のMixture-of-Experts構成だ。訓練は3段階（中間訓練→教師あり微調整→強化学習）で行われており、強化学習フェーズではCISPOと呼ばれる手法を使っている。CISPOはMistralが提案するClipped Importance Sampling Policy Optimizationの略で、方策勾配法の一種であるPPOの派生手法に相当する。
Lean 4は定理証明支援システムであり、数学的主張やプログラムの仕様を機械的に検証できる言語だ。通常の大規模言語モデルが「それっぽい答え」を返すのに対し、Lean 4のコンパイラは証明が正しいかどうかを厳密に判定する。Leanstral 1.5の特徴は、この検証フィードバックをループに組み込んでいる点にある。
最も面白いのはベンチマークではなく「バグ発見パイプライン」
リリースの中で最も実用的な内容は、コンテストベンチマークの結果ではなく、実際のRustコードからバグを見つけた事例だ。
MistralはOSSリポジトリ57件に対して以下のパイプラインを適用した：
- AeneasでRustコードをLean 4に変換
- Leanstral 1.5が「このコードが正しければ成立するはずの性質」を推論
- その性質を証明しようと4回試みる
- 証明に失敗したら、今度はその否定（＝バグがある）を証明しようと4回試みる
この結果、47件の性質違反を検出し、そのうち11件が実際のバグ、5件はGitHubに未報告だった。具体例として挙げられているのがdatrs/varintegerライブラリで発見されたバグだ。
なお、このパイプラインはモデルの推論と証明試行を自動化しているが、対象リポジトリの選定や検出結果の精査には人間の判断が介在しうる構造になっている点は留意しておきたい。
「コードが主張通りに動くことを証明する」というアプローチは形式手法の研究者が長年訴えてきたものだが、実際のOSSリポジトリで未報告バグを出したという報告は、議論をより具体的な地点に引き寄せる。
ベンチマーク数値：強いが自社報告
ベンチマーク面では以下の数字が報告されている：
- miniF2F：検証・テストセットともに100%
- PutnamBench（672問中）：4Mトークンバジェットで587問解答
- FLTEval（フェルマーの最終定理関連PRを元にした評価セット。Mistralがオープンソースで公開した評価ハーネス）：pass@1で21.9→28.9、pass@8で31.9→43.2（Claude Opus 4.6の39.6を上回り、コストは約7分の1）
記事内では「FATEベンチマーク」という表記も登場するが、これはFLTEvalとは別の評価セットであり、フェルマーの最終定理のLean形式化プロジェクト（FLT）に関連する難易度の異なるサブセットを指すと考えられる。元記事での説明は簡略なため、詳細は公式ブログを参照されたい。
テスト時スケーリングの数値は、推論コストを増やすほど性能が上がるという傾向を示している。PutnamBenchでのPass@8は、トークンバジェット50,000で44問、200,000で244問、100万で493問、400万で587問と伸びている。
コスト比較として、MistralはPutnamBench1問あたり約4ドルと主張している。Seed-Prover 1.5 highは推定300ドル以上、Aleph Proverは54〜68ドルだという。ただしMistral自身が「高ランクシステムは異なる条件（自然言語証明ガイダンスを含む）で動作している場合がある」と注記している。
なお、これらはすべてMistralの自社報告であり、独立した再現検証はリリース記事には含まれていない。
形式検証AI競争の背景
形式検証とLLMの組み合わせは、ここ1〜2年で急速に注目を集めている分野だ。
- Google DeepMindのAlphaProofは、AlphaZeroスタイルの強化学習とLeanを組み合わせ、2024年の国際数学オリンピック（IMO）で銀メダル相当のスコアを記録した
- DeepSeekのDeepSeek-Prover-V2は、サブゴール分解を強化学習で訓練したオープンソースのLean 4証明器として論文を公開している
- Harmonic（Aristotleを開発するPalo Altoの数学AI企業）は1億2000万ドルのシリーズCを調達、評価額は14億5000万ドルに達している
Mistralの差別化は配布戦略だ。Apache-2.0ライセンスで重みを公開し、無料APIも用意する。Lean 4ベースの評価ハーネスFLTEvalもオープンソース化した。
残る課題：評価の信頼性
2025年6月に公開された論文「Faults in Our Formal Benchmarking」は、Lean定理証明ベンチマークに関する問題を指摘している。Lean 4のカーネルは形式文を機械的に検証するが、それは「形式的な命題が証明できた」ということであり、元の非形式的な意図と一致しているかどうかは別問題だ。
この論文は広く使われているLean定理証明ベンチマーク5件とそのフォークに対して4833件の問題を特定し、そのうち398件はカウンターサンプルや空虚な定理、健全でない公理など機械的に認証された問題だという。
Leanstral 1.5の次の試練は、外部の研究者や開発者がベンチマーク結果を再現できるか、失敗ケースを精査できるか、そして報告されたバグをリポジトリのメンテナーが実際に受理するかどうかだ。
詳細はMistral opens Leanstral 1.5 in a bet on machine-checked AIを参照していただきたい。
