PSI、AIで量子計算の未解決予想を証明　科学的発見の事業化を進める

科学研究向けAIを開発するPhysical Superintelligence（PSI）の研究システムが、2008年から未解決だった量子計算の「アーロンソン＝アンバイニス予想」の証明を見つけました。同社は現在、物理シミュレーションを使ったデータセンターの最適化で収益を得ており、長期的には理論物理学の成果を技術へ転換する事業を目指しています。

量子計算の高速化に必要な条件を解明

アーロンソン＝アンバイニス予想は、量子コンピューターが通常のコンピューターより大幅に少ない入力の読み取りで問題を解ける条件に関わる数学の予想です。証明によって、ランダムな入力に対して「はい・いいえ」で答える問題では、量子計算の入力読み取り回数に指数関数的な優位が生じないことが示されました。

この分野では、入力の特別な構造を利用して高速化します。例えば、大きな数の素因数分解を高速に行うショアのアルゴリズムは、問題に隠れた繰り返しのパターンを利用します。今回の結果は、量子計算が指数関数的に読み取り回数を減らせる問題には、入力にまれなパターンが必要だという関係を裏付けるものです。

PSIのシステムは、非公開のAnthropic製AIモデルを使い、自社の計算基盤で実行されました。実行の3日目に完全な証明を得て、証明の各段階をコンピューターで検査する支援ソフト「Lean」が受理しました。その後、関連する未解決問題の探索を続ける中で結果を2度改善し、最終版もLeanに受理されています。

研究を率いたデイビッド・タートゥリアン氏は、研究システムの開発、問題の選定、実行を担当しました。さらにモデルに論文の初稿作成を指示し、初稿を確認したうえで、論文の正しさに責任を負う役割を担っています。

機械による検査と専門家による理解を組み合わせる

証明は外部の研究者にも共有され、Guy Blanc氏ら4人が解説を作成しました。解説は証明を4つの主要段階に整理し、既存研究とのつながりを説明しています。中心的な考え方を伝えるため、数式に含まれる指数の最適化より、証明の見通しを優先した構成です。

PSIの成果で使われたLeanは、形式的に記述された定理が、定義や前提、公理から導かれることを検査します。この検証では、数学の言葉で意図した内容と、コンピューターに入力した定理の記述が一致しているかも確かめます。定理の記述や参照する定義を点検し、証明が依存する公理を調べる手順が設けられています。

PSIでは、顧問のジム・ハルバーソン氏が証明を監査し、同じく顧問のフィアラ・シャナハン氏がLeanによる形式化について意見を寄せました。タートゥリアン氏も、AIが導いた解を印刷して読み、人間にとって自然な形で提示する方法を検討したと語っています。

モデルを研究に使うための「ハーネス」

PSIは、科学上の問題に合わせたハーネスや周辺の仕組みを使います。ハーネスとは、AIモデルの周囲で、外部ツール、文脈、記憶、実行手順などを管理するソフトウェアです。科学研究向けの構成では、計画を立て、ツールを動かし、結果を観察して計画を修正する流れに、検索や継続的な記憶を組み合わせます。

PSIのマット・パインズ最高経営責任者（CEO）は、研究システムにはハーネス、ツール、記憶システム、シミュレーション基盤が必要だと述べています。幅広い選択肢を検討し、問題を広く深く探索できる構成を重視しています。

こうした研究ハーネスの構成例に、北京大学の研究者らによる「AutoSci」があります。再利用できる科学知識と、個別の研究に属する着想・実験・原稿などの記憶を分け、ハーネスが研究の状態、文脈、検証、フィードバックを管理します。

現在の収益源はデータセンターの最適化

PSIは現在、熱、電力、水、音といった変数をシミュレーションし、データセンターを最適化するツールから収益を得ています。パインズ氏は、施設の性能と地域社会への影響が、施設の物理的な条件に直接左右されると述べています。

この最適化が扱う課題の一つが、冷却設備内外の熱や空気の流れです。計算機で流体の動きを解析する「数値流体力学（CFD）」を使ったデータセンター研究では、サーバー設備への吸気温度や空気の流れる方向に加え、屋上の冷却装置が隣接設備や発電機の排熱を吸い込む条件を調べています。

電力、水、排出量、費用の関係も、冷却方式を選ぶ際の検討対象です。Wedan Emmanuel Gnibga氏らの「FlexCoolDC」研究は、米カリフォルニア州、テキサス州、ドイツ、フランスを対象に、蒸発冷却を使う場合と使わない場合を比較しました。水を節約する冷却方式への変更が費用に与える影響は地域で異なり、炭素排出量もカリフォルニア州とテキサス州では増える一方、フランスでは影響が小さいという結果でした。

冷却研究では、室内の機器配置だけでなく、屋外設備、気象条件、通常運転時と故障時の状態もシミュレーションの対象になっています。

理論上の発見を実験と技術へつなぐ

PSIの長期的な目標は、理論物理学の発見を装置などの技術へ結び付けることです。パインズ氏は、計算で得た結果を、できるだけ効率よく実験で検証する方法に注力していると語っています。AIが着想を示し、実験で自然界の性質として確かめ、それを新しい装置に利用する循環を構築する考えです。

AIを科学研究に使う際の検証や共有の手順も、研究者間で議論が続いています。ハルバーソン氏は、透明性を保ち、専門家に連絡することを重視したと述べました。MITでは科学研究の新たな進展速度への対応を物理学者らが議論する会合が予定され、同氏も参加する予定です。