ハクソク

世界を動かす技術を、日本語で。

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

70日前原文(mistral.ai)

概要

Leanstralは、Lean 4向けに開発された初のオープンソースコードエージェント。 高度な証明支援とコーディング自動化を効率的に実現。 OSSモデルやClaudeファミリーと比較して高効率・低コストを実現。 FLTEvalによる実践的なベンチマークで優位性を証明。 Mistral VibeやAPI経由で即利用可能、モデル重みも自由にダウンロード可能。

Leanstral：Lean 4向けオープンソースコードエージェントの登場

  • Leanstral は、Lean 4用に設計された初の オープンソースコードエージェント
  • Lean 4は、 複雑な数学的対象 や ソフトウェア仕様 を形式的に表現できる証明支援システム
  • Leanstralは、 効率性重視の6Bパラメータ設計 ・現実的な形式化リポジトリでの運用に特化
  • 既存の証明システムと異なり、 大規模汎用モデルのラッパーや単一問題特化型ではない
  • Apache 2.0ライセンス 下でモデル重みを公開、Mistral VibeのエージェントモードやAPI経由で利用可能
  • 技術レポートやFLTEval評価スイート も公開予定、競技数学以外の評価指標を拡充

Leanstralの技術的特徴

  • 高疎性アーキテクチャ 採用、証明エンジニアリングに最適化
  • Leanを完璧な検証器 として並列推論を活用し、パフォーマンスとコスト効率を両立
  • MCP（Modular Code Protocol） に対応、特にlean-lsp-mcpとの高い親和性
  • FLTプロジェクトのPR単位 で全証明・新規概念定義を完了できるかをベンチマーク指標に採用

Leanstral vs OSSモデル・Claudeファミリー

  • Leanstral-120B-A6B は、GLM5-744B-A40BやKimi-K2.5-1T-32Bと比較し、 遥かに高効率

    • GLM5やKimi-K2.5はFLTEvalスコア上限が16.6・20.1程度
    • Leanstralは 一回のパスで両者を超えるスコア
    • Qwen3.5-397B-A17Bが4パス必要な25.4を、Leanstralは 2パスで26.3 を達成
    • Leanstralは コスト同等で29.3までスケール可能

  • Claudeファミリーとの比較

    • Leanstral pass@2はスコア26.3、Sonnetを2.6ポイント上回り、 コストは$36（Sonnetは$549）
    • pass@16ではスコア31.9、Sonnetより8ポイント高い
    • Claude Opus 4.6は品質で優位だが、 コストはLeanstralの92倍（$1,650）
    • すべてのベンチマークはMistral Vibe上で追加改変なしで実施

| モデル | コスト($) | スコア | |:-------------|:---------|:------| | Haiku | 184 | 23.0 | | Sonnet | 549 | 23.7 | | Opus | 1,650 | 39.6 | | Leanstral | 182 | 21.9 | | Leanstral@2 | 36 | 26.3 | | Leanstral@4 | 72 | 29.3 | | Leanstral@8 | 145 | 31.0 | | Leanstral@16 | 290 | 31.9 |

ケーススタディ

  • Leanバージョン変更時のStackExchange質問対応

    • Lean 4.29.0-rc6で発生したスクリプトのコンパイルエラーをLeanstralが解析
    • defによる型エイリアス定義 がrwタクティックでパターンマッチできない問題を特定
    • abbrevへの書き換え を提案し、問題を解決
    • 理由も明確に説明し、ユーザーに納得感を提供

  • プログラムの形式的検証

    • Princeton大学のRocq定義（https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html）をLean形式へ自動変換
    • 独自記法の実装や、与えられた命題の証明まで自動生成
    • 証明要求にも対応可能

Leanstralの利用方法

  • Mistral Vibeで即利用
    • Vibe内で/leanstallコマンドを入力するだけでコーディング・証明開始
  • Labs API提供
    • labs-leanstral-2603エンドポイントで 無料・低価格API を提供（期間限定）
    • 現実的なフィードバック収集と次世代モデルへの反映を目的
  • モデル重みのダウンロード可能
    • Apache 2.0ライセンス 下で自由に取得・ローカル運用可能
  • 詳細ドキュメントやサインアップ
    • Mistral Vibe公式サイトから利用登録・詳細情報取得可能

Leanstralは、証明支援とコード生成の両立を目指す現場において、 高効率・低コスト・即応性 を兼ね備えた新世代エージェント。 形式的検証や数理研究、ミッションクリティカルなソフトウェア開発現場での生産性向上に貢献。

Hackerたちの意見

信頼できる雰囲気のコーディングだね。他のやつより全然いい！でも、比較がよく分からないな。Haikuに対するコスト削減を強調してるけど、Haikuってこのタスクにはあんまり向いてないし、Leanstralはもっとダメなの？正確さを重視するなら、「うん、ダメだけど10倍安い」ってのがどう関係あるの？それとも何か勘違いしてる？期待できる点としては、Opusもこのベンチマークではあんまり良くないみたいだし、これをスケールアップすればOpusより良い結果が出せるかもね。これがポイントかな。

└

そんなに難しくないよ。プロンプトで「信頼できる出力だけを求める」ってはっきり言えばいいだけだから、簡単だよ。

└

グラフはあんまり分かりやすくないけど、設定可能なパスがあるみたいで、2パスだとHaikuやSonnetより良くて、16パスになるとOpusに近づいてくるけど、まだそこまで行ってないみたい。ただ、Sonnetよりは常に安いね。

他の人も同じ反応してるか気になる。このモデルはこのタスク専用にトレーニングされてるのに、Opusに比べてかなり劣ってる。Opusは約6倍高いから、今やってるタスクに対しては…全然その価値があるように思える。[1]: テストしたモデルの総合的な広がりに基づいて

└

こういうベンチマークにどれだけ信頼を置けるかは分からないけど、いずれにせよ、pass@2とpass@3を持つと印象が変わるみたい。もっと興味深い比較はCodexとの比較になるだろうね。

└

同意。アイデアは素晴らしくて立派だよね。でも、AIが証明していることの一つは、質がコントロールや信頼よりも重要なことが多いってこと（敏感な分野やアプリケーションを除いてね）。もちろん、資本集約的ではないから、比較的小さなEUのスタートアップがそのニッチに注力するのは理解できる。でも、理由から考えると、売上にはあまり影響しないだろうね。

ここで言ってる「パス」って何？LLMの評価では見たことないな。改善を探るときに、別のモデルがコードベースを走らせるのは面白いかもね。

└

質問に答える試行回数のことだよ。

彼らが報告している現実の成功は、Simon WillisonのRed Green TDDを思い出させるね。 > 「暗闇の中で手探りする代わりに、Leanstralは腕まくりをした。失敗した環境を再現するテストコードを成功裏に構築し、定義的平等性による根本的な問題を診断した。このモデルは、defが明示的な展開を要求する厳格な定義を作成するため、rw戦術が必要な基盤構造を見えなくしていることを正しく特定した。」

└

TDDはエージェント的なコーディングタスクにおけるプロンプトエンジニアリングだね。

参考までに、Lean 4の論文はこちら: https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37

いい驚きだな。「オープンソース」って言って、本当にオープンソースを意味してる人がいるなんて。どうやら、重みはApache-2.0ライセンスみたいだね。

これを数週間前に予想してたから、当たって嬉しい！ > LLMや似たような未来のツールの時代に、これがどうなるのか興味あるな。人間がコードを扱うのがどれだけ簡単かを無視して、証明可能性やテスト、もしかしたらトークン効率に焦点を当てる未来のフェーズチェンジがあるんじゃないかな。 > LeanとRustを組み合わせて、コンパイラに優しいものに縮小したものを想像してみて。高水準言語で必要なことを指定して、「バイブコード」を返されるのではなく、正しく証明されたコードが返ってくる。だって、それだけが成功裏にコンパイルできるコードだから。 https://news.ycombinator.com/item?id=47192116

モデルから抽出されたから、俳句の比較なの？

最近、モデルの整合性が相対的で、整合性の多様性が重要だって話がたくさんされてるよね。ジャック・クラーク（Anthropicの共同創設者）とエズラ・クラインの最近のポッドキャストエピソードを見てみて。ここでの多くのコメントは、ミストラルのモデルが他の最前線のモデルに追いついていないって指摘してるけど、これは私の個人的な経験でもある。でも、モデルの整合性技術やそれを訓練する企業の多様性がもっと必要だよね。だから、これを真剣に受け止めている企業は貴重だと思う。