1万エージェントの正体は、検証器だった
1万エージェントの正体は、検証器だった
見出しになった数字
2026年9月8日、OpenAI が、ミレニアム懸賞問題のひとつ「ナビエ・ストークス方程式の存在と滑らかさ」について、AIが解決に至る証明を生成したと発表した。
見出しになったのは、この数字だ。
約1万のAIエージェントを並行稼働、約88時間で到達。
先に断っておくと、この証明はまだ査読前で、正式に解決と認められたわけではない。発表の経緯——著者クレジットの扱いや、研究者の私的な利用データがモデル側に流れた可能性——をめぐって、数学者から強い反発も出ている。真偽の判定はここではしない。
ここで見たいのは、そこではない。
**「1万体を並列に走らせる」という運用の型そのものは、OpenAI 自身が構成を公開している。**そして、そこには自分たちのスケールでも真似できる構造がある。
1万ではなく、まず100だった
構成をよく読むと、いきなり1万体を投入したわけではない。
Step 1: 約100体 × 約50時間
→ 隣接する、より簡単な問題(オイラー方程式)を先に落とす
Step 2: その結果を「出発点」としてリソースを振り替え
→ ここで概ね1万体規模の同時並行に
Step 3: 到達(開始から約88時間)
Step 4: 形式検証系 Lean での形式化・機械検証に、別途17時間
踏み台になる小さい問題を先に落として、その成果を次の問題の初期条件として持ち込んでいる。
つまり「大きい問題に大量投入」ではなく、階段だ。そして階段の1段目は、100体だった。
これは重要だと思う。1万という数字は個人にも中小規模のチームにも縁遠いが、100体という段は、すでに現実的な射程に入っている。
で、なぜ1万体が意味を持ったのか
ここが本題だ。
普通、生成の並列度を上げると、詰まる場所が移動する。
並列度を上げる前: 「作る」が遅い
並列度を上げた後: 「作る」は速い。「正しいか判定する」が遅い
100体のエージェントが100個の候補を出したら、100件のレビュー待ちが誰かの机に積まれる。その誰かは、たいてい自分だ。**ボトルネックは消えたのではなく、生成から検証へ移動しただけ。**台数は成果に変換されない。
OpenAI の構成でそれが起きなかったのは、後段に Lean があったからだ。
Leanは対話的定理証明支援系で、小さな信頼された核(カーネル)を持ち、証明が正しいかどうかを人間のレビューを介さずに機械が判定できる。
だから1万体が吐いた候補を捌ける。
言い方を変えると、こうなる。
並列エージェントのスケール上限を決めているのは、エージェントの台数ではなく、後段の検証器の処理能力である。
1万エージェントの正体は、Lean だった。
自分のドメインの「Lean」は何か
この見方をすると、やることの順番が変わる。
台数を増やす前に、「機械が◯×を返せる形」に問題を落とす作業が本体になる。
| ドメイン | そこでの「Lean」にあたるもの |
|---|---|
| ソフトウェア開発 | テストが通る / 型が通る / ビルドが通る / リンタが黙る |
| データ処理 | スキーマ検証、件数と合計値の突き合わせ |
| 調査・リサーチ | 一次情報URLへの到達確認、複数ソース間の数値一致 |
| 業務システム | 受け入れ条件を機械判定可能な形に書き下したもの |
ここが自動化できていない領域に並列エージェントを当てても、レビュー地獄になるだけだ。
逆に、**判定器さえあれば、台数は後からいくらでも増やせる。**投資すべきは判定器のほうだと思う。
多数決ではなく、仮説を割る
もうひとつ、構成で目を引いた点。
同じ指示をN体に投げて多数決を取る、という設計ではない。
問題を A/B/C/D の変種に割り、一部のグループには「証明せよ」を、別のグループには「反証せよ」を、同時に投げている。
賭けを両建てしている。
これは、並列化の設計単位が「試行回数」ではなく「分岐させる仮説」だということを意味する。
そしてこの区別は、実務でそのまま効く。
分岐させるものが無い課題に、並列エージェントを当ててはいけない。
設計空間が狭い機能——たとえば「ここにカウンタを1つ足す」——を10体に投げても、10通りのほぼ同じ実装が出てきて、選ぶ手間だけが増える。トークンが溶ける。
並列が効くのは、方針そのものが割れているときだ。「どの層でフックするか」で3案あるなら、3体に1案ずつ実装させて、判定器に勝ち残らせればいい。
コストは、後から足すガードではない
規模の話も書いておく。
ナビエ・ストークスの分だけで、270万メッセージ、出力約1300億トークン。
この桁は個人や小規模チームには無関係に見えるが、上限を持たない並列実行は、10体でも100体でも簡単に金額が跳ねるという事実は同じだ。1体が暴走して延々とループするのは、日常的に起きる。
だから、累積コストの上限ガードは「動いてから足す機能」ではなく、並列度を上げるための前提工事だと考えている。順番を逆にすると、たぶん一度痛い目を見る。
10か、100か
1万は多い。でも、10とか100はやらないといけない、と思っている。
そう思う理由が、この発表を読んでむしろはっきりした。1万という数字が特別なのではなく、階段の1段目が100体だったからだ。そして、その1段目を登るために必要なのは、大量の計算資源ではなく、
- 判定器(機械が◯×を返す装置)
- 分岐設計(回数ではなく仮説を割る)
- コスト上限(並列化の前提工事)
の3つだった。
どれも、今日から手をつけられる。台数はその後だ。