Anthropic、1,000体のFable 5.2エージェントがフェルマーの最終定理の形式証明を再現した方法を詳述

Anthropicによると、初期版のClaude Fable 5.2を実行する1,000体のエージェントチームが、フェルマーの最終定理のLean形式化を28.7時間で再現した。同社はこれをおもちゃの実験と呼んでいる。9月に行われた形式化は、Fable 5.1とおおむね同等の社内モデルを使い、研究者の指示のもと数十体のエージェントが取り組んだもので、11日と約60億の出力トークンを要した。Anthropicによると、今回の実行では出力トークン数が3分の1となり、証明の長さも7分の1になった。Prove2Meプラットフォームも、研究者による進行の誘導も使わなかった。

実験環境。 各エージェントには、ネットワーク接続のない軽量仮想マシン上で、シェルとファイルエディター、LeanとMathlib、mainへのマージリクエストを送る独自のGitブランチ、共有Postgresデータベースが与えられた。Anthropicは、証明すべき60の命題、古典的な解法の1文の概略、必要な定義、以前の作業で証明済みの補題47個をチームに与え、リード1体と補助役999体を配置した。組織化の方法について、それ以上の指示は与えなかったという。

エージェントの取り組み。 Anthropicによると、リードは最初の10分で、順序、割り当て、メモ、サブタスク、完了済み作業の5つのデータベーステーブルを作成した。序盤、補助役たちは60の命題のうち47個を予算内で証明するのは不可能と判断した。リードはいったんそれらを保留にしたが、最初の10個が約70分で証明されると再び取り組み始めた。約18時間後、リードは約750体の補助役をLanglands–Tunnellに移した。担当リーダーは期限内に完了する確率を1%未満と見積もっていた。補助役たちはこれを最大10階層、2,418個のタスクからなるツリーに分割し、28.4時間時点で証明を完了、最終定理は28.7時間時点で証明された。

安全対策。 Anthropicによると、サンドボックスに加えて、プロンプトで指示された分類器がすべてのシェルコマンドとファイル編集を実行前に確認し、ブロックが発生するとチーム全体が停止して人間によるレビューに回る仕組みだった。また、オフラインモニターがチームの行動を確認した。同社によると、100万回を超えるツール呼び出しのうち、ブロック基準に該当したものはなかった。今回の実行で使われたのは行動ベースのモニターのみで、その後まもなく、思考の連鎖とエージェント間の通信も読み取るモニターを追加したという。Anthropicは、リリース前のアラインメント評価を終えていない可能性のあるモデルでも、こうした実験を行っていると述べている。

留意点。 Anthropicは、今回の成果によってProve2Meのような領域特化型プラットフォームが不要になるわけではないと述べている。また、エージェントは難問に早々に諦めたり、難易度を見誤ったりする傾向があり、人間の励ましが引き続き役立つ場合があるという。