Leanstral：信頼できるバイブコーディングのためのオープンソース基盤

AI エージェントはコード生成において非常に能力の高いツールであることが証明されています。しかし、最先端の研究数学からミッションクリティカルなソフトウェアに至るまで、これらのモデルを高リスク領域に適用しようとする際、私たちはスケーリングのボトルネックに直面します：それは人間のレビューです。手動で検証するために必要な時間と専門知識が、エンジニアリングの速度に対する主要な impedance（阻害要因）となっています。 私たちは、タスクを実行すると同時に、厳格な仕様に対して実装を形式的に証明する、より有益な次世代のコーディングエージェントを構想しています。機械生成ロジックのデバッグを行うのではなく、人間が何を望むかを指示します。本日、私たちはそのビジョンに向けた最初の大きな一歩を踏み出します。 ## Leanstral の紹介 Lean 4 用に設計された初のオープンソースコードエージェントである Leanstral をリリースします。Lean4 は、[perfectoid spaces](https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/)（完全体空間）のような複雑な数学的対象や、[Rust フラグメントの特性](https://github.com/AeneasVerif/aeneas) といったソフトウェア仕様を表現できる証明支援系です。既存の証明システムが汎用大規模モデルをラップするものや単一の数学問題に焦点を当てるものであるのに対し、Leanstral は非常に効率的（アクティブパラメータ数 6B）であり、現実的な形式リポジトリで動作するように訓練されています。 - オープンでアクセス可能：Leanstral の重みは Apache 2.0 ライセンスの下、Mistral のバイブ（vibe）モード内のエージェントとして、および無料の API エンドポイントを通じて公開されます。また、トレーニング手法を詳細に記した技術レポートと、競技数学への焦点を超えた評価を可能にする新たな評価スイート「FLTEval」も公開する予定です。 - 効率的かつ強力：Leanstral は証明工学タスク向けに最適化された極めてスパースなアーキテクチャを採用しています。完璧な検証ツールである Lean を活用した並列推論により、既存のクローズドソース競合他社製品に対して高性能かつコスト効率を実現しています。 - MCP によるアップグレード対応：Leanstral はバイブ（vibe）を通じて任意の MCP（Model Context Protocol）をサポートしており、特に頻繁に使用される「lean-lsp-mcp」との組み合わせで最大限のパフォーマンスを発揮するように特別にトレーニングされています。 ## 評価 現実的な証明工学シナリオにおける有用性を反映させるため、Leanstral のベンチマークは、FLT プロジェクトへの各 PR（Pull Request）においてすべての形式化された証明を完了し、新しい数学的概念を正しく定義できるかを対象として行います。これは孤立した数学的問題に対する評価とは異なります。Leanstral は、主要なコーディングエージェント（Claude Opus 4.6, Sonnet 4.6, Haiku 4.5）およびオープンソースモデル（Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B）と比較されます。 ## Leanstral vs. OSS モデル Leanstral-120B-A6B は、はるかに大きなオープンソースの競合モデルと比較して、顕著な効率性の優位性を示しています。GLM5-744B-A40B や Kimi-K2.5-1T-32B といったモデルはスケーリングに苦しみ、FLTEval スコアがそれぞれ約 16.6 と 20.1 で頭打ちになる中、Leanstral は単一のパス（single pass）でこれら両者を上回っています。 最も強力な OSS 競合である Qwen3.5-397B-A17B でさえ、スコア 25.4 に達するには 4 パスが必要です。それに対し Leanstral は、その半分以下の投資（pass@2）でより優れたスコア 26.3 を達成し、線形にスケールを続け、同じコストレベルで 29.3 に到達します。 ![image](https://cms.mistral.ai/assets/78aaa774-c717-4c60-b71b-1161487b28e5.jpg?width=1861&height=1245) ## Leanstral vs. Claude Family Leanstral は、Claude シリーズに対する高価値な代替案として機能し、その数分の一の価格で競争力のあるパフォーマンスを提供します。Leanstral の pass@2 はスコア 26.3 を達成し、Sonnet よりも 2.6 ポイント上回りますが、実行コストは Sonnet の 549 ドルに対してわずか 36 ドルです。pass@16 では Leanstral はスコア 31.9 に達し、Sonnet を 8 ポイント引き離して余裕を持って勝利します。Claude Opus 4.6 は品質において依然としてリーダーですが、そのコストは驚異的な 1,650 ドルで、Leanstral の実行コストの 92 倍に相当します。 ベンチマークでは、評価のために特別に修正を加えず、Mistral Vibe をスケフォールド（基盤）として使用しました。 モデル | コスト ($) | スコア ---|---|--- Haiku | 184 | 23.0 Sonnet | 549 | 23.7 Opus | 1,650 | 39.6 Leanstral | 182 | 21.9 Leanstral pass@2 | 36 | 26.3 Leanstral pass@4 | 72 | 29.3 Leanstral pass@8 | 145 | 31.0 Leanstral pass@16 | 290 | 31.9 ## ケーススタディ ## 新しい Lean バージョンの変更に関する Stack Exchange の投稿への回答 破壊的変更が新しい Lean リリースに適用されると、コードの移行は大きな頭痛の種になり得ます。私たちは Leanstral に、Proof Assistants Stack Exchange からの実際の質問 [a real-world question from the Proof Assistants Stack Exchange](https://proofassistants.stackexchange.com/questions/6471/a-strange-issue-with-a-type-alias-in-lean4) を入力しました。これは、Lean 4.29.0-rc6 で突然コンパイルが停止したスクリプトに関するものであり、このバージョンは学習データに含まれていませんでした（最新のため）。その原因は、単純な型エイリアス `def T2 := List Bool` で定義されたパターンを suddenly 一致させられなくなった書き換え (rw) タクティクスでした。 闇雲に試行錯誤するのではなく、Leanstral は袖をまくり上げました。失敗した環境を再現するためのテストコードを成功裏に構築し、定義的等価性に関する根本的な問題を特定しました。モデルは正しく、`def` が明示的な展開を必要とする剛性の高い定義を作成するため、rw タクティクスがマッチングに必要な基底構造を見ることができなくなっていると指摘しました。 提案された修正は単純でした：`def` を `abbrev` に置き換えることです。`abbrev` は透明なエイリアスを作成し、元の型と即座に定義的等価となるため、rw タクティクスは証明内で再びパターン `(L2 n).length` を完璧に一致させることができるようになりました。Leanstral は作業を完了し、その理由をユーザーに対して完全に説明します。 ## プログラムに関する推論 Rocq の定義を [https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html](https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html) からコピーし、Leanstral に Lean への変換を依頼しました。Leanstral はこれを成功裡に実行し、カスタム記法の実装さえ行いました。例を示します： また、Rocq の記述（証明なし）のみを与えられただけでも、この言語のプログラムに関するいくつかの性質を Lean へ変換して証明することも可能です。 ## 証明を要求する。Leanstral を今日からお試しください。 Leanstral は現在、誰でも利用可能です。 - Mistral Vibe でのゼロセットアップ：Leanstral を Mistral Vibe に直接統合し、即時のゼロセットアップによる「バイブコーディング」と証明を実現しました。/leanstall と入力してアクティブ化してください。その後、Shift+Tab を押してモデルが Leanstral として表示されるまで待ちます。あるいは、vibe --agent lean を使用することもできます。 - Labs API：無料またはほぼ無料の API エンドポイント labs-leanstral-2603 を通じてモデルにアクセスできます。次世代の検証済みコードモデルを強化するための現実的なフィードバックと観測データを収集するため、このエンドポイントは限られた期間、非常に高いアクセシビリティを維持します。 - ウェイトの所有：Apache 2.0 ライセンスの下でモデルをダウンロードし、ご自身のハードウェア上で実行できます。 [ドキュメント](https://docs.mistral.ai/models/leanstral-26-03) - [Mistral Vibe のサインアップ](https://console.mistral.ai/codestral/cli)

Leanstral：信頼できるバイブコーディングのためのオープンソース基盤

背景や根拠まで確認しますか？

関連記事

調べる

選ぶ

サイト

背景や根拠まで確認しますか？

関連記事

ニュースの次に確認する

調べる

選ぶ

サイト