Leanstral は、その開始以来、Lean 4 での証明工学にオープンで実用的なアプローチを提供してきました。本日、Leanstral 1.5 をリリースします。これは、無料の Apache-2.0 ライセンスモデルで、119B の総パラメータとわずか 6B のアクティブパラメータを持ち、形式検証をこれまで以上に強力でアクセスしやすくする性能向上を実現しています。
Leanstral 1.5 は、miniF2F を飽和させ（検証セットとテストセットで 100%）、PutnamBench の 587/672 の問題を解決し、FATE-H（87%）と FATE-X（34%）で新記録を達成しました。ベンチマークを超えて、複雑なコードプロパティを検証し、オープンソースリポジトリで未知のバグを発見し、厳密な形式手法が実世界でも効果的で実用的であることを証明しました。
トレーニングプロセス Leanstral 1.5 は、中間トレーニング、教師ありファインチューニング、CISPO による強化学習の 3 段階を経ます。2 つの強化学習環境で広範なトレーニングを実施しました。
- マルチターン環境：モデルは定理のステートメントを与えられ、証明または反証する必要があります。モデルは証明を提出し、Lean コンパイラからのフィードバックを受け、試行ごとにアプローチを改善します。証明がコンパイルされれば成功、そうでなければモデルが問題を解決するか予算を使い切るまでループが続きます。
- コードエージェント環境：Leanstral は、生のファイルシステムで開発者のように動作します。ファイルを編集し、bash コマンドを実行し、Lean 言語サーバーを使用して目標、エラー、型情報をリアルタイムで検査します。これにより、リポジトリ内の部分的な証明の完成、補助補題の構築、複数ラウンドのコンテキスト圧縮を伴う長期的なタスクに対処できます。モデルは完全な証明工学ワークフローをナビゲートすることを学び、最終的には SafeVerify のフォークによって正しさが検証されます。
評価結果 miniF2F では、Leanstral 1.5 は完全に飽和しました。PutnamBench と FATE-H/X では、Goedel-Architect（自然言語ガイダンスなし）、Seed-Prover 1.5（高設定）、AxProverBase と比較して、Leanstral 1.5 は FATE-H/X で新記録（それぞれ 87 問と 34 問を解決）を達成しました。PutnamBench では、Seed-Prover よりもはるかに低いコスト（問題あたり約 4 ドル vs Seed-Prover の 300 ドル以上）で 7 問多く解決しました。より高いランクの証明器は、自然言語による証明ガイダンスを受けているか、Aleph Prover（問題あたり 54-68 ドル）のように実行コストがはるかに高いかのいずれかです。
Leanstral 1.5 は、形式推論モデルとしてこれまでにない最強のテスト時スケーリングを示しました。試行あたりのトークン予算を 25k から 4M に増やすにつれて、PutnamBench の Pass@8 は滑らかに単調増加しました。50k で 44 問、200k で 244 問、1M で 493 問、4M で 587 問です。証明が長く続いても、Leanstral は推論、ファイル編集、修正を続け、予算を直接解決問題に変換します。
また、FLTEval ベンチマークも完全にオープンソース化しました。Leanstral 1.5 は、ベンチマークの pass@1 を 21.9 から 28.9 に、pass@8 を 31.9 から 43.2 に引き上げ、Opus 4.6 の 39.6 を 7 分の 1 のコストで上回り、3～10 倍のサイズのオープンソースモデルとの差を広げました。
コード検証ケーススタディ
- AVL 木の時間計算量証明：Leanstral 1.5 は、構造的帰納法と慎重なモナディック時間追跡を使用して、実際の実装における AVL 木の O(log n) 時間計算量を証明しました。270 万トークンと 22 回の圧縮を経て、TimeM モナドの各層を体系的に展開し、制御フローとインターリーブされた基礎となる計算を明らかにし、ほぼ厳密なバウンドを確立し、高さと木のサイズを対数関係で結び付け、挿入と削除が確かに O(log n) であることを完全に検証しました。
- バグ発見：自動化パイプライン（Aeneas が Rust コードを Lean に翻訳し、Leanstral がユーザーの意図を推論してコードから正しさのプロパティを生成）を用いて、57 のテストリポジトリで 47 の違反プロパティをフラグし、そのうち 11 が実際のバグを示し、5 つは GitHub で未報告でした。例えば、datrs/varinteger ライブラリのジグザグ復号用 sign 関数で、入力 Std.U64.MAX に対して式 (value + 1) がオーバーフローし、デバッグモードでクラッシュ、リリースモードでサイレント破損を引き起こしました。これはテストやファジングでは通常見逃されるエッジケースです。
始め方 Leanstral 1.5 は Apache-2.0 ライセンスです。重みは Hugging Face で入手でき、無料 API エンドポイント leanstral-1-5 としても利用可能です。Mistral Vibe での使用を推奨します。API キーを取得し、手順に従ってセットアップしてください：Mistral Vibe のインストール、Leanstral 1.5 のインストール、エージェントの起動、オプションで Lean LSP MPC のインストール。これで、定理の証明、証明のデバッグ、リポジトリへの貢献を Leanstral に依頼できます。