Leanstral 1.5: すべての人のための証明の豊かさ

 (mistral.ai)
1 ポイント 投稿者 GN⁺ 4 시간 전 | 1件のコメント | WhatsAppで共有
  • 形式検証を実際の開発作業により近い形で使おうとする流れの中で、Mistral AIがLean 4向けのApache-2.0モデルLeanstral 1.5を公開
  • モデルは総119Bパラメータのうち6Bのみを有効化し、中間学習・教師ありファインチューニング・CISPO強化学習を経て、証明作成とコードリポジトリ作業をあわせて学習
  • miniF2F 100%、PutnamBench 587/672、FATE-H 87%、FATE-X 34%を記録し、数学証明ベンチマークと実際の証明エンジニアリング評価で高い性能を示す
  • 実際のコード検証では、AVL木の**O(log n)**時間計算量の証明とRust-to-Leanパイプラインを通じて、57個のリポジトリから11件の実バグを発見
  • 重みとleanstral-1-5無料APIが公開されており、定理証明・証明デバッグ・リポジトリへの貢献といった実用的な証明エンジニアリングにすぐ適用可能

Leanstral 1.5の公開とモデル特性

  • Leanstral 1.5は、Lean 4で証明エンジニアリングを行うために作られたモデル
  • ライセンスはApache-2.0で、モデル規模は総119Bパラメータ、アクティブパラメータは6B
  • 形式検証性能を引き上げることで、数学ベンチマークだけでなく実際のコード特性検証にも活用可能
  • miniF2Fを飽和し、PutnamBench 672問中587問を解き、FATE-H 87%、FATE-X 34%を達成

証明フィードバックを学習した3段階訓練

  • 学習は中間学習、教師ありファインチューニング、CISPOベースの強化学習という3段階で構成
  • 強化学習には2つの環境が使われる
    • マルチターン環境: モデルが定理命題を受け取り、証明または反証を行い、Leanコンパイラのフィードバックをもとに証明を繰り返し修正
    • 証明がコンパイルされれば成功となり、そうでなければ問題を解くか予算を使い切るまでループが続く
    • コードエージェント環境: 生のファイルシステム上で開発者のようにファイルを編集し、bashコマンドを実行し、Lean language serverでゴール・エラー・型情報をリアルタイムに確認
  • コードエージェント環境は、リポジトリ内の部分証明の完成、補助定理の作成、複数回のコンテキスト圧縮後も作業を継続する長時間タスクを扱う
  • 最終的な正当性は、対象定理リストを基準にMistralのSafeVerifyフォークで検証される

数学・証明エンジニアリングベンチマーク

  • 評価にはminiF2F、PutnamBench、FATE-H/FATE-X、FLTEvalが使われる
    • miniF2Fは、初等問題からIMOレベルの問題までを含む形式数学ベンチマーク
    • PutnamBenchは、Putnam Mathematical Competitionの672問で構成
    • FATE-HとFATE-Xは、それぞれ大学院・博士課程レベルの抽象代数ベンチマーク
    • FLTEvalは、Fermat’s Last Theoremリポジトリの実際のプルリクエストをもとに証明エンジニアリングの難度を評価
  • miniF2Fでは、検証セットとテストセットの両方で**100%**を達成
  • PutnamBenchとFATE-H/Xでは、自然言語の証明ガイドなしでGoedel-Architect、Seed-Prover 1.5 high、AxProverBaseと比較される
  • FATE-H/X性能: {b:87,34}
  • FATE-Hは87%、FATE-Xは**34%**で、新たな最高性能を達成
  • PutnamBenchではSeed-Prover 1.5 highより7問多く解き、1問あたりのコストは約4ドル水準
    • Seed-Proverのhigh設定は1問あたり10 H20-daysの予算を使い、コストは300ドル超と推定される
    • より高順位の一部の証明器は自然言語の証明ガイドを受けるか、Aleph Proverのように1問あたり54〜68ドルかかる別条件で動作する

長い推論予算でのスケーラビリティとFLTEval

  • Leanstral 1.5はPutnamBenchで、トークン予算を増やすほどPass@8性能が滑らかかつ単調に上昇
  • 試行ごとのトークン予算を25kから4Mまで増やした実験では、解けた問題数は次のように増加
    • 50kトークン: 44問
    • 200kトークン: 244問
    • 1Mトークン: 493問
    • 4Mトークン: 587問
  • 長い証明でも中断せず、数百万トークンにわたって推論・ファイル編集・修正を続ける動作が性能向上につながる
  • FLTEvalも完全にオープンソースとして公開
  • FLTEvalでLeanstral 1.5はpass@1を21.9から28.9へ、pass@8を31.9から43.2へ引き上げ
  • pass@8の43.2はOpus 4.6の39.6を上回り、コストは7分の1水準
  • オープンソースモデルの中でも、3〜10倍大きいモデル群を上回る性能を示す

実際のコード検証事例

  • AVL木の時間計算量証明

    • AVL木は、挿入と削除の際の再平衡化によって**O(log n)**の高さを保つ自己平衡二分探索木
    • Leanstral 1.5は、実際の実装に対して挿入と削除がO(log n)であることを検証
    • この作業には、木の再帰構造を反映する構造的帰納法、モナドベースの時間追跡処理、再平衡化経路に対する網羅的なケース分析が必要だった
    • 証明は270万個以上のトークンと22回のコンテキスト圧縮を経て進行
    • LeanstralはTimeMモナドの各層を体系的に展開し、制御フローと混ざった計算を明らかにする
    • 挿入について高さ単位あたり48ステップという、定数項に近い境界を立て、高さと木のサイズを対数関係で結び付ける

  • Rustコードでバグを見つける

    • バグ検出実験は、AeneasがRustコードをLeanに変換し、Leanstralがコードからユーザー意図を推論して整合性特性を生成するパイプラインで構成
    • Leanstralは各特性について4回証明を試み、すべて失敗した場合はその否定を再び4回試みて証明
    • 57個のリポジトリで47個の違反特性が示され、このうち11件が実バグを指していた
    • 実バグのうち5件は、GitHubに以前報告されていなかったバグ
    • datrs/varintegerライブラリのzigzag decoding sign関数で1件が発見
    • 入力がStd.U64.MAXのとき、(value + 1)式がオーバーフローする
    • デバッグモードではクラッシュが発生し、リリースモードでは静かなデータ破損が発生
    • このエッジケースは、一般的なテストやファジングでは見逃されやすい事例

配布と利用方法

  • 重みはHugging Faceで公開
  • 無料APIエンドポイントはモデルカードでleanstral-1-5という名前で提供
  • 利用環境としてMistral Vibeが推奨される
  • 開始手順は、Mistral Vibeの設定、Leanstral 1.5の導入、エージェント実行、任意のLean LSP MCP導入、証明作業開始の順
  • Lean LSP MCPは~/.vibe/config.tomlに追加して導入する方法が推奨される
  • 既存のMCPサーバーがなければ、mcp_servers = []を削除する必要がある場合がある
  • Leanstralは、定理解決、証明デバッグ、リポジトリへの貢献作業に利用できる

関連記事

1件のコメント

 
GN⁺ 4 시간 전
Hacker Newsのコメント

  • Mistralが大規模モデルと競争するのは難しいという批判は妥当だが、実際には小さなモデルで特定の機能を高品質に提供することに集中しているのだと思う
    OCRやファイル解析のような作業にMistralを使っているが、アカウントに100ドル入れておけば、リクエスト量を気にせず1年は回る
    コストが極めて小さいので、Opus 4.8と競争できなくても十分に価値がある

    • OCRでは実際にどれほど競争力があるのか気になる
      安い価格でそこそこの品質というのは、後でミスを減らすために10倍の料金を払って最高品質を使うよりも、さらにニッチ市場のように見える
    • ヨーロッパの愚か者たちは、できるだけ金を稼ぐための最適化ではなく、良い製品を作るための最適化をしているんだな /s
    • 「年100ドル以下で1年分の文書処理」が、思ったほど素晴らしいのかはよく分からない。少なくとも欧州の競争力という観点では、Mistralは売上の上限を低く設定しすぎていることになる
      OCRはすでにコモディティに近く、オープンソースモデルやAWSのようなところでも標準で提供されている
      さらに年100ドルという価格ではロイヤルティを生みにくく、切り替えコストもないので、より低い価格が出れば顧客はすぐ離れ得る
      容易に複製できる低価格ツールに顧客ロックインがないなら、ビジネスというより機能に近い
      買い手にとっては良いだろうが、欧州企業が長期的に世界の競合と製品力で競争することを望むなら、悪い戦略に見える

  • 取り組み自体は良いが、バグ発見の例が妙に感じられた
    zigzagデコーディングのsign関数でStd.U64.MAX入力時に(value + 1)がオーバーフローし、デバッグモードではクラッシュ、リリースモードでは静かな破損が起きると言っていたが、これをテストが「普通は見落とす」境界条件と呼べるのか分からない
    悪いテストなら見落とすだろうが、慎重な人や機械学習ベースのコーディングシステムは「極端な値をテストしよう」ということをかなりうまくやる。特にユーザー入力をパースするコードならなおさらだ
    もっと興味深いバグも見つけたが、手短に説明しにくかったのでこの例を出したのか気になる

    • 特に「ファジングでも見落とす」という部分が変だ。私が見てきたファジングは、一般に境界値を意図的に探索する
      こうしたエンコーディングライブラリなら、まともなコードに対する基本的な期待値はファジングであり、ほぼ確実に数秒以内に捕まったはずだと思う
      実際にproptestでごく簡単な往復テストを作ったところ、1秒もかからず数十件の失敗と以下の結果が出た:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • 「普通は見落とす」とは言いにくいが、実際に存在していたのだから、時には見落とされるバグではある
      Leanを使うと、どの例をテストすべきかを賢く選ぶ必要が減る、という利点は見えている
    • これは基本的な品質保証だ。テストがこういうものを見落とすなら、私たちが通常期待するよりもずっと有用性が限られていることになる
      著者たちのバックグラウンドが気になってくる
    • これは単なるひどい宣伝だ
      1980年ごろに発明されたすべてのプロパティベーステストシステムは境界値を探索する
      CとC++の意味論、あるいはその欠如のために、実際のテストが難しいことはあり得る。未定義動作につながるすべての入力について、コンパイラが「テスト合格」としても許されるからだ

  • 記事の途中で複数の最前線級LLMとの比較が出てくるが、どれも半年前のモデルだ
    「私たちの新モデルは3世代前の中国モデルより優れている」という感じで、かなり笑えた

    • これは60億パラメータモデルなので、完全に別のクラスだ。むしろ「最前線級の小型言語モデル」として期待が高まる
    • 同意するが、オープンウェイトで比較的小さいというだけでも見出しになる。このモデルはかなりよく動く

  • そのライブラリはhttps://github.com/datrs/varintegerだ
    論文が公開される1週間前に同じ問題がすでにこのリポジトリに上がっていたので、おそらく合っていると思う: https://github.com/datrs/varinteger/issues/8
    この人がLeanstralの社員なのか、それともLeanstralがこのissueを単に持ってきただけなのかは分からない
    このライブラリは小さく、テストが驚くほど貧弱で、8年間ほとんど手が入っていない状態だ: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    ダウンロードは1日約1000件程度で、少ない方に見える: https://crates.io/crates/varinteger
    なので、唯一の例として掲げるほど大きな成功とは見なしにくい。自動検出が有用なのは確かだが、このサブ分野では注目すべき成果なのかよく分からない
    証明作成LLMは使ったことがないが、学習データが少なめなので、一般的なコーディングモデルより荒削りでも驚きはしない
    ちなみにhttps://crates.io/crates/varintegerにはhttps://github.com/mafintosh/varinteger-rsと表示されるが、このアドレスがhttps://github.com/datrs/varintegerにリダイレクトされるので、見かけとは違って同じライブラリに見える

    • 証明の問題は、価値を伝えるのが時々難しいところにある
      重要なのはバグを見つけることではなく、特定の種類のバグが特定の仮定の下で存在しないことを証明することだ
      しかしこの話は売り込みにくいので、マーケティングはしばしば「このバグを見つけた」という方向に流れていく

  • Leanをまったく知らない人にも役立つだろうか？ 作業中のソフトウェアを検証したいが、形式検証の経験はない
    仕様、コード、そして限られた学習時間だけでも使える結果が得られるのか気になる

    • 証明しようとする部分自体は理解する必要があるが、証明プロセス全体をすべて理解する必要はない
      数学というより、Haskellの型を読むことに近く、語彙だけを数学から多く借りている感じ
    • 記事の「Bug Discovery: Finding Hidden Flaws」の節を読むと、Rustコードだけから始めて、オープンソースのRustで問題を見つけるためにモデルを使ったように見える
      アプリケーション検証のためのLeanコードを書くよう、対話しながら支援を受けることもできるかもしれないが、確かではない
    • 少なくとも、コードについてどんな定理を証明したいのか、そしてそれをLeanでどう表現するのかは理解している必要がある
      そうでなければ出力を検証できない
      機械的には正しいと検査された何らかの命題を証明できているかもしれないが、その命題が何を意味するのか、実際に検証したい内容を包含しているのかが分からなければ意味がない
    • Lean4をまったく知らない状態から約6か月で、コーディングの大半をLean4で行うレベルまで来ており、この過程はAI支援のおかげで大きく加速した
      モデルがLean4にどれほど一貫して流暢なのかには驚くほどだ。最前線級のモデルだけでなく小さなローカルモデルも同様で、LLMはLean4を普通によく理解しているように思える
      まだLean4の専門家と呼ぶには道のりが残っているが、いまでは有用なプログラムを作るのに支援が必須というわけではない
      知識がほとんどない状態でも、完全には理解していない部分を信頼できるという点は学習速度を大きく引き上げる。不完全な知識でも依存できるプログラムを得られるのは実用的で、モチベーションにもなる
      中間の証明ステップ全体ではなく、自分の公理と命題の表面を説明する言語部分によって限界が決まる感じだ。時間が経ってより多くのことをするにはより多く理解しなければならないが、ある意味ではN+1レベルで安全に作業できる
      Lean4は定理証明の役割とは別に、楽しいプログラミング言語でもあり、速度も驚くほど速い
      io_uringに接続して使っているが、多くの場合C++/libuvやRust/Tokioよりはるかに速い
      たまにp99.99レイテンシのようなところで大きなテールが見えると、数値を固定幅に変えるといったチューニングが必要になるが、C++やRustでもチューニングは必要だ

  • Lean 4を形式検証用として推している点が興味深い
    この領域はIsabelle/HOLとTLA+の側だと思っていた
    少なくとも3つすべてを使うよう学習したモデルを期待していた気がする。線形代数の前向き導出にはIsabelle/Isarのほうも良さそうに見えるが、誰か説明してくれないだろうか？

    • LeanはIsabelleや、以前のCoqであるRocqに比べて、ソフトウェア検証での採用が少なかったのは確か
      この分野ではAgdaでさえもっと使われてきたほうだ
      ただしLeanは現在、代替手段としてかなりの勢いを得ており、特に汎用関数型プログラミング言語としての能力が大きい
      個人的には、要件と仕様を対応させやすいHoare論理や分離論理ベースのアプローチのほうが実用的だと思う。DafnyとF*が気に入っている

  • Twitterでの発表で、開発者たちがLe Chaton Fatにさりげなく触れていたのが面白かった
    彼らが実際にLe Chaton Fatに関わっていたかどうかに関係なく、本当に「新しい大型汎用」モデルが近いうちに出てきそうだ
    メディア騒動の後にも直接言及していたので期待している。名前は「Large 4」よりもっと創造的だといい

  • 最新のOpenATPでLeanstral 1.5を試せる
    OpenATPはエージェント型の自動定理証明器のためのオープンソースPythonパッケージ兼CLIで、Dockerでローカル実行するか、Modalサンドボックスでリモート実行する方式を標準でサポートしている
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com