Mistral AI、Lean 4向けオープンソース証明AIエージェント「Leanstral」をリリース

Zach Anderson 2026/3/16 19:13

Mistralは、Lean 4形式検証用の60億パラメータAIエージェント「Leanstral」をリリース。Apache 2.0ライセンスの下、より大規模なモデルを15分の1のコストで上回る性能を実現。

2026年3月16日、Mistral AIはLeanstralをリリースした。これはLean 4形式検証専用に構築された初のオープンソースAIエージェントである。1200億パラメータモデルはわずか60億の有効パラメータで動作し、Apache 2.0ライセンスで提供されるため、企業予算なしでプロダクショングレードの定理証明が利用可能となる。

これが暗号資産にとって重要な理由とは?形式検証—コードが主張通りに正確に動作することの数学的証明—は、スマートコントラクトやブロックチェーンプロトコルのセキュリティ確保におけるゴールドスタンダードとなっている。DeFiコードのバグは数十億ドルの損失を生んできた。Leanstralは、検証済みセキュリティを求めるプロジェクトの障壁を劇的に下げる可能性がある。

パフォーマンス対コストのトレードオフ

Mistralは、フェルマーの最終定理形式化プロジェクトからの実際の証明エンジニアリングタスクをテストする新しい評価スイートFLTEvalを使用して、Leanstralを独自およびオープンソースの競合製品とベンチマークした。

数値は印象的である。Leanstralはpass@2で26.3ポイントを記録し、計算コストは36ドル。Claude Sonnet 4.6は23.7ポイントを達成したが、549ドルの費用がかかり、性能が劣るにもかかわらずコストは15倍以上。pass@16でも、Leanstralは290ドルで31.9ポイントに達し、Claude Opus 4.6の1,650ドルの価格の5分の1未満である(ただし、Opusは39.6ポイントで品質をリード)。

オープンソースの代替品と比較すると、効率の差はさらに広がる。GLM5-744B-A40BとKimi-K2.5-1T-A32Bは、有効パラメータが6-8倍多いにもかかわらず、16-20ポイント付近で頭打ちとなる。Qwen3.5-397B-A17Bは25.4ポイントに到達するために4回のパスが必要だが、Leanstralは2回でそれを上回る。

技術アーキテクチャ

Leanstralは、証明エンジニアリングワークフロー向けに最適化されたスパース混合エキスパートアーキテクチャを使用している。モデルは、MCP(Model Context Protocol)を通じてLeanの言語サーバープロトコルと統合され、lean-lsp-mcpツールで最大のパフォーマンスを発揮するよう特別にトレーニングされている。

Lean 4自体は2023年9月に安定版がリリースされ、数学の形式化のために急速に採用されている。数学的証明の膨大なコレクションであるMathlibライブラリは、同年にLean 4への移植に成功した。フェルマーの最終定理の形式証明のようなプロジェクトは、本格的な数学研究におけるプラットフォームの能力を実証している。

実世界での応用

MistralはLeanstralが、Lean 4.29.0-rc6における破壊的変更に関する実際のStack Exchangeデバッグ質問を処理する様子を紹介した。このエージェントは型エイリアスに関する定義的等価性の問題を診断し、defをabbrevに交換することで戦術マッチングが復元されることを正しく特定した。

このモデルは、Rocq(旧Coq)の定義をLean 4に変換し、証明のセマンティクスを保持しながらカスタム記法を実装するクロスランゲージ翻訳も実演した。

アクセスオプション

3つのデプロイメント方法がある:Mistral Vibeへの直接統合(/leanstallを使用して開始)、期間限定のフィードバック収集用無料APIエンドポイントlabs-leanstral-2603、またはApache 2.0ウェイトを使用したセルフホスト型デプロイメント。

ブロックチェーンプロジェクトにとって、計算は単純明快である。形式検証は従来、高額な監査会社または深い社内専門知識のいずれかを必要としてきた。タスクあたり36-290ドルでコードの正確性を証明できるオープンソースエージェントは、証明が本番環境条件下で成立すると仮定すれば、プロトコルがセキュリティにアプローチする方法を再構築できる可能性がある。

• mistral ai
• leanstral
• lean 4
• 形式検証
• オープンソース