- Lean 4向けに設計された初のオープンソースコードエージェントで、形式証明(formal proof) の自動化により人手による検証負担の軽減を目指す
- Apache 2.0ライセンスでモデル重みを公開し、Mistral Vibe環境と無料APIエンドポイントを通じてすぐに利用可能
- 6Bアクティブパラメータのスパースアーキテクチャを採用し、効率性とコスト削減を実現、lean-lsp-mcpのようなMCP統合をサポート
- FLTEvalベンチマークでQwen3.5、GLM5、Kimi-K2.5などの大規模オープンソースモデルを上回るスコアを記録し、Claude Sonnetと比べて15倍以上低コストで同等に近い性能を示す
- 形式証明の自動化とコード信頼性向上を組み合わせた新しいアプローチで、研究数学とミッションクリティカルなソフトウェア開発の両方での活用可能性を示す
Leanstral 概要
- LeanstralはLean 4のための初のオープンソースコードエージェントで、形式証明支援系(proof assistant) 環境で動作
- Lean 4は複雑な数学的対象（例: perfectoid 空間）やソフトウェア仕様を表現できる
- 既存の証明システムが汎用モデルラッパーや単一問題に集中しているのに対し、Leanstralは実運用に近い形式リポジトリ(formal repositories) で効率的に動作するよう訓練されている
- 6Bアクティブパラメータを持つスパース(sparse)アーキテクチャを採用し、並列推論(parallel inference) とLeanの検証機能を組み合わせる
- MCP統合対応により、lean-lsp-mcpのような一般的なプロトコルと互換性がある
公開とアクセシビリティ
- Apache 2.0ライセンスでモデル重みを公開し、Mistral Vibe内のエージェントモードとして提供
- 無料APIエンドポイント(
labs-leanstral-2603) を通じて誰でもアクセス可能で、ユーザーフィードバックを収集して次期モデルの改善に活用予定
- 技術レポートと評価ツール FLTEvalもあわせて公開し、従来の数学中心評価を超えて実際の証明エンジニアリング性能を測定
性能評価 (Evaluation)
- FLTプロジェクトのPull Request単位で、すべての形式証明と新しい数学概念の定義を完了する能力を基準に評価
- 比較対象: Claude Opus 4.6、Sonnet 4.6、Haiku 4.5、Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B
Leanstral vs. オープンソースモデル
- Leanstral-120B-A6BはGLM5(16.6点)、Kimi-K2.5(20.1点)を上回る26.3点(pass@2) を記録
- Qwen3.5が4回実行(pass@4)で25.4点を獲得した一方、Leanstralは半分の実行回数でより高いスコアを達成
- 同一コスト水準で29.3点(pass@4) まで線形にスケール
Leanstral vs. Claude製品群
- Sonnetに対して2.6点優位(26.3点 vs 23.7点) を示し、実行コストは**$36 vs $549**で15倍以上安価
- pass@16基準で31.9点を記録し、Sonnetより8点高い
- 最高性能のClaude Opus 4.6は39.6点を記録したが、コストは**$1,650でLeanstral比92倍**高い
- すべてのベンチマークはMistral Vibe環境で修正なしに実施
| モデル |
コスト($) |
スコア |
| Haiku |
184 |
23.0 |
| Sonnet |
549 |
23.7 |
| Opus |
1,650 |
39.6 |
| Leanstral |
18 |
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 |
事例研究 (Case Studies)
Leanバージョン変更への対応
- Lean 4.29.0-rc6で発生した型エイリアス関連のエラーを扱うStackExchangeの質問を入力
- Leanstralは問題環境を再現し、定義的等価性(definitional equality) の問題を正確に診断
def の代わりに abbrev を使うよう提案し、rwタクティク(tactic) が再び正常に動作するよう修正- 問題の原因と解決の理由をユーザーに明確に説明
プログラム推論と変換
- Rocqのプログラム定義をLeanへ変換し、ユーザー定義記法まで実装
- 例として
plus2 コマンドが変数Xに2を加える動作を行うことを証明
- 与えられたRocq仕様だけをもとに、Leanで定理(theorem) を完成させて証明を実行
利用方法
- Mistral Vibe統合:
/leanstall コマンドですぐに利用可能
- Labs API: 無料または低コストでアクセス可能
- モデルダウンロード: Apache 2.0ライセンスで直接実行可能
意義
- Leanstralはコード生成と形式証明自動化を組み合わせた初のオープンソースの試み
- 研究数学、検証可能なソフトウェア開発、高信頼システム設計などでの活用可能性を示す
- コスト効率とオープン性を同時に備えた新しいコード検証インフラとして評価される
1件のコメント
Hacker Newsのコメント
人々がついに、エージェントに望む振る舞いを仕様として記述し、その仕様に沿ってコードを書かせるというパターンを認識し始めたのが興味深い
TDDや検証ツールなどどんな手法を使うにせよ、時間が経てばこうした検証スイートは「どう動くべきか」を示す実行可能なドキュメントのリポジトリとして蓄積されていく
こうしたアプローチは、単なるMarkdownの仕様書よりはるかに強力だ。意図ではなく詳細な振る舞いをコードに落とし込むからだ
ソフトウェアが複雑になるほど、「それはJimに聞いてくれ」式の口伝には限界がある
細かさや文脈は、解像度の変化の中で失われてしまう
TDDや検証中心開発には賛成だが、それをコードで書くこと自体が最終目標ではない
すでに数百万行のテストが存在するのだから、それを土台に発展させるのが現実的だ
Leanが実際に何を助けてくれるのか知りたい。
たとえばLeanで状態機械を証明して、それをDartに移すような話なのか？
Leanに詳しくないので、これが現実的なアプローチなのかピンとこない
最近のJack Clark（Anthropic共同創業者）とEzra Kleinのポッドキャストでも触れられていたように、モデルアラインメント（alignment） は相対的なもので、多様性が重要だという議論が多い
Mistralのモデルは他の最先端モデルより見劣りするという意見もあるが、さまざまなアラインメント手法や企業が試されることはエコシステムにとって重要だ
実際の成功事例を見ると、Simon Willisonの Red Green TDD を思い出す
Leanstralが失敗環境を再現するテストコードを作り、定義的等価性（definitional equality） の問題を見つけた過程が印象的だった
このモデルは特定の作業向けに訓練されているが、Opusより性能が低い
Opusは6倍高価だが、その価値はありそうだ
資本の少ない欧州スタートアップがこうしたニッチを狙うのは理解できるが、大きな収益につながるのは難しそうだ
Codexのようなモデルと比較するほうがさらに面白そうだ
「信頼できるコード」というコンセプトは気に入った
ただし比較基準がわかりにくい。Haikuより安いことを強調しているが、Haiku自体がこの作業に弱く、Leanstralはそれよりさらに弱い
正確性が目標なら、「安いがいまひとつ」であることがなぜ重要なのかわからない
それでもOpusも完璧ではないので、規模を拡大すればもっと良い結果を出せるかもしれない
2回ではHaikuやSonnetより良く、16回ではOpusに近づきつつもコスト効率が高い
Leanを知らない立場として、これに直接的な価値があるのか気になる
Goのような言語のコードに自動で証明を付けてくれるのか、それとも単にオープンモデルの多様性を応援すればよいのか？
ただ最終的には、そのLean4仕様自体がソフトウェア成果物になる
だとすると、その仕様が正しいかを検証する問題に戻る――結局は人間のレビューが必要だ
数週間前からこういう流れを予想していたので、実際に当たってうれしい
LLM時代には、コードの人間にとっての読みやすさより証明可能性とトークン効率のほうが重要になる気がする
LeanとRustを組み合わせて、「証明されたコードだけがコンパイルされる」世界が来るかもしれない
関連する議論は以前のコメントにまとめてある
保証するのは単に**論理的に妥当（valid）**であることだけだ
証明が何を証明しているのかを完全に理解することは、プログラムを理解するのと同じくらい難しいが、その過程で思考が深まる利点はある
「オープンソース」と言うだけでなく、実際にApache-2.0ライセンスの重みとして公開した点はうれしい
Mistral公式ニュース によれば
Claude Opusはコスト1,650ドルでスコア39.6、
Leanstral pass@8は145ドルで31.0、pass@16は290ドルで31.9で、
コスト対性能効率はかなり高い