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

フランスのAIスタートアップのMistral AIが、数学的証明やソフトウェア仕様の検証などを支援するAIモデル「Leanstral」を公開しました。Leanstralは形式証明ツール「Lean 4」に対応したオープンソースのAIエージェントで、数学やプログラムの正しさを厳密に検証する「証明エンジニアリング」を支援することを目的としています。

Leanstral: Open-Source foundation for trustworthy vibe-coding | Mistral AI
https://mistral.ai/news/leanstral

The Lean 4 Theorem Prover and Programming Language | Automated Deduction – CADE 28
https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37

AIは高度な推論や数学的証明、コーディングなどが可能ですが、AIが完了したタスクに問題がないかは人間が最終的な確認・検証を行う必要があります。しかし、最先端の研究数学や複雑なソフトウェアの場合は検証の難易度も高く、人間が手動でレビューするために必要な時間と専門知識がエンジニアリングのスピードを阻害する最大の要因となります。

そこでMistral AIは、タスクを実行するだけではなく、実装の正当性を形式的に証明できるより有用なコーディングエージェントの世代を構想しているそうです。その一環として、数学研究やソフトウェア検証などの分野で使われる証明支援システム「Lean 4」向けに設計された初のオープンソースコードエージェントが「Leanstral」です。

Leanstralは証明の構築や検証をAIが補助できるようにすることを目標としており、Mixture-of-Experts(MoE)と呼ばれるアーキテクチャを採用しています。MoEアーキテクチャは証明工学タスクに最適化されており、必要な専門モジュールのみを能動的に選択して計算を行うため、モデル全体のパラメータ数が大きくても実際の計算ではその一部のみを使用することで高い性能と低い計算コストを両立できるとされています。Leanを検証器として用いた上で複数の推論結果を同時に生成して検証することで、Leanstralは既存のクローズドソース競合製品と比較して高いパフォーマンスとコスト効率を実現しています。

以下は、形式的証明の完了と新しい数学的概念の正しい定義についてベンチマークする「FLTEval」のスコアを、主要なオープンソースモデル(Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B)と比較したもの。横軸の「pass」は同じ問題に対する試行回数、縦軸はベンチマークスコアを示しています。競合のオープンモデルで最も強力なQwen3.5 397B-A17Bでも4回の試行で「25.4」というスコアに到達していますが、Leanstralは2回の試行で「26.3」とより優れたスコアを達成し、4回の試行では「29.3」までスコアを伸ばしていることが分かります。

また以下は、主要なコーディングエージェント(Claude Opus 4.6、Sonnet 4.6、Haiku 4.5)とLeanstralのコストパフォーマンスを比較した表。LeanstralはSonnet 4.6やHaiku 4.5と同等のスコアを獲得するために必要な実行コストが大幅に低くなっていることが分かります。また、Claude Opus 4.6のスコアは「39.6」とかなり高くなっていますが、実行コストはLeanstralを2回実行する場合の約92倍となっており、Leanstralはコストパフォーマンスの高さをアピールしています。

LeanstralはApache 2.0ライセンスの下、Mistral Vibe内のエージェントモードおよび無料のAPIエンドポイントを通じて公開され、研究者や開発者が自由に利用・改変できる形になっています。また、トレーニング手法の詳細を解説した技術レポートと、競技数学に偏重した評価から脱却するための新しい評価スイート「FLTEval」も公開予定です。