11月9日、claude.dev（※Anthropicの公式サービスではなく、Claude APIを活用した第三者サービス）が「Safely scaling multi-agent teams with Claude Fable 5.2 / claude.dev Blog」と題した記事を公開した。この記事では、1,000エージェントチームがClaude Fable 5.2（※Anthropicの内部・早期バージョンと思われるが、2025年5月時点で公式に広く公表されたモデル名ではない）を用いて、フェルマーの最終定理の証明をコンピュータが検証可能な形式に再現した実験と、その安全設計について詳しく紹介されている。
1,000エージェントがフェルマーの最終定理の証明を形式化
フェルマーの最終定理（「n > 2 のとき、aⁿ + bⁿ = cⁿ を満たす正の整数 a, b, c は存在しない」）は、350年以上未解決であり続け、1995年にアンドリュー・ワイルズが129ページの証明を発表して初めて解決した。
今回の実験が取り組んだのは、その証明を「再証明」することではない。コンピュータが全ステップを機械的に検証できる形式（Lean言語による形式化）に変換・再現することだ。Leanは定理証明支援系と呼ばれるプログラミング言語・システムの一種で、数学的な証明を厳密なコードとして記述できる。Leanで書かれた証明はコンパイラが各ステップの論理的正当性を逐一チェックするため、「証明した」という主張は客観的・機械的に確認可能になる。この「形式化」は、人間が書いた証明の信頼性を機械的に担保する手段として、数学コミュニティの長年の目標とされてきた。
Anthropicは2024年9月、研究者数名と数十のエージェントが11日間・約60億トークンを費やし、Lean言語で1,300万行のコードを書いてこの形式化を達成したと発表した。このとき、エージェント間の調整にはProve2Meという専用プラットフォームと研究者によるディレクションが必要だった。
今回の実験では、Claude Fable 5.2の早期バージョンを搭載した1,000エージェントのチームが、Prove2Meも研究者の介在もなしにこの証明の形式化を再現した。結果は以下のとおりだ。
- 所要時間：28.7時間
- 使用トークン数：前回の3分の1
- 証明の長さ：前回の7分の1
専用ツールなしで自律的に調整システムを構築
今回の実験で最も興味深いのは、エージェントが自らコーディネーション機構を組み立てた点だ。
各エージェントにはシェル、ファイルエディタ、自分専用のGitブランチ、共有PostgreSQLデータベースへのアクセスが与えられた。ネットワークアクセスは遮断されており、使えるのはこれら汎用ツールのみ。Prove2Meのような専用の調整プラットフォームは存在しない。
チームの構成は「リード1体 + ヘルパー999体」のシンプルな階層だった。リードへの指示は「問題を分割してヘルパーに割り当てること」、ヘルパーへの指示は「リードからの作業を待ち、不明な点はリードに確認すること」のみ。
リードは開始から10分以内に、共有データベース上に5つのテーブルを自律的に設計・作成した。
| テーブル | 用途 |
|---|---|
| Announce | リードからチーム全体への指示 |
| Assign | 各ヘルパーへの作業割り当て |
| Notes | 進捗報告や作業宣言のオープンボード |
| Subtasks | 誰でもタスクを追加・取得できるToDoリスト |
| Landed | 完了した作業のログ |
その後リードは60の証明すべきステートメントを16〜17体のヘルパーからなるクルーに割り当て、各クルーにキャプテンを任命した。開始から約27分後には3つのステートメントがすでに証明済みになっており、リードはヘルパーの評価を読んで「予算内では不可能」と判断した47ステートメントを保留し、残り10ステートメントにほぼ全ヘルパーを再集結させた。クルーの規模は最大139体まで拡大した。
前回の形式化で失敗した原因は「エージェントがプロジェクトの状態を見失い、協調が崩壊した」ことだったが、今回はSQLデータベースという汎用ツールでその問題を解決している。分散書き込みの競合はSQLトランザクションで処理する設計になっており、エージェント数が増えるほど有効に機能する構造だ。
3層の安全設計
100エージェントで共有マシンを使ったテストでは、半数以上のランでメモリ・ディスク・CPUが枯渇して停止・再起動を余儀なくされた。 今回は各エージェントを独立した軽量VMで動作させることでこの問題を回避している。100から1,000エージェントへのスケールアップにあたって、共有マシンから個別VMへの移行が必須になった点は、マルチエージェント基盤を設計する上での実践的な教訓と言えるだろう。
安全設計は3層構造だ。
サンドボックス化
- 各エージェントはネットワーク非接続のVM内で動作
- Gitへのプッシュは自分のブランチのみ（mainへはマージリクエスト経由）
- データベースアクセスは非特権ロール、各SQLに5秒の制限と256MiBの書き込み上限
- カーネルはロードモジュール・kexec・生メモリアクセス等を無効にしたlockdownモードで動作
リアルタイム監視
LLMベースの分類器がすべてのツール呼び出し（シェルコマンド、ファイル編集）を実行前にチェックする。分類器がブロックを判定した場合、チーム全体が停止し人間のレビューが必要になる設計（フェイルクローズド）だ。
今回の実験では100万回以上のツール呼び出しで1件もブロックされなかった。 実験後にCoTモニターで同じ呼び出しを再評価したところ、rootアクセス確認の1件だけがブロックに近かった。
オフライン監視
リアルタイム監視と並行して、他エージェントの行動を参照できるオフラインモニターもチームの行動を分析する。なお今回の実験では並列CoTモニターはまだ使用していなかった（実験直後に追加）という点も正直に記されている。
実験が示す意義
今回の実験は、マルチエージェントシステムのスケーラビリティと安全設計の両面で注目に値する。Leanによる形式化という客観的に検証可能なベンチマークを設定したことで、「エージェントが何を達成したか」が曖昧にならない評価軸を持っている点も特徴的だ。専用のオーケストレーションツールを与えず、汎用ツールのみでエージェント自身が調整機構を構築したという事実は、今後のマルチエージェント設計における「どこまでを基盤が担い、どこまでをエージェントに委ねるか」という議論に実践的な示唆を与えるものだろう。
詳細はSafely scaling multi-agent teams with Claude Fable 5.2 / claude.dev Blogを参照していただきたい。
