PSI、Aaronson–Ambainis予想の機械検証済み証明を報告

Physical Superintelligenceは2026年11月6日に、非公開のAnthropicモデルを複数のインスタンスで稼働させた社内研究システムが、2008年以来未解決だった量子コンピューティングの問題、Aaronson-Ambainis予想の証明を見つけたと発表した。

システムは、PSI独自のインフラ上で稼働を開始して3日目に完全な証明を作成し、証明支援系Leanがこれを受理した。その後PSIは、関連する未解決問題をシステムに与え、結果を2度改善させた後、Leanが最終版を受理した。原稿とLean 4による形式化は公開されている。

量子計算の高速化について予想が示すこと

問題は、量子コンピューターが古典コンピューターより指数関数的に高速になり得るのはどのような場合か、という点にある。Shorの1994年の素因数分解アルゴリズムは、アルゴリズムが利用できる繰り返しパターンを入力が持つという構造に依存している。PSIの成果が扱うのは、こうしたパターンが通常存在しない、ランダムまたは非構造的な入力という対照的なケースだ。

クエリモデルでは、古典アルゴリズムは1回のクエリにつき1ビットを読み取る一方、量子クエリは重ね合わせによって多数の入力位置にまたがることができる。PSIの説明は、このモデルを多項式と結び付けている。量子クエリをT回行った後、アルゴリズムが「はい」と答える確率は、入力ビットを変数とする次数が最大2Tの有界多項式となる。したがって、量子アルゴリズムのシミュレーションは、指数関数的な数の入力ビットを読み取らずにその多項式を推定する問題となる。

当初の論文でScott AaronsonとAndris Ambainisは、すべての有界低次数多項式には、非常に大きな影響を持つ変数が存在すると予想した。2人は、この予想を仮定すれば、T回のクエリを行うあらゆる量子アルゴリズムを、入力の大半について、Tの多項式個のクエリを行う古典アルゴリズムでシミュレーションできることを示した。この帰結により、近似誤差と除外する入力の割合をそれぞれ固定した場合、古典クエリ数の増加は指数関数的ではなく多項式的となる。ただし、適切な構造を持つ問題で量子計算が指数関数的な優位性を得る可能性を否定するものではない。

形式的には、このリポジトリでは、次数が最大dである実多項式pを考える。その値は離散立方体上で0から1の範囲にある。一様ランダムな入力に対する分散がε以上なら、少なくとも1つの座標の影響度は (8√15 / (125π⁴)) · ε^(5/2) / d⁶ 以上となり、したがって (ε/d)⁷ 以上となる。影響度とは、その座標のビットを反転させたときのpの変化量の二乗の期待値である。

証明の構築と検証の方法

この議論は、fractional certificateとレベル集合に基づくShachar LovettとJiapeng Zhangの計画に沿っているが、その計画で予想にとどまっていた不等式を、すべてのペアに適用できる新たな不等式に置き換えている。行列式を用いて、入力設定の全単射対応を構成する。PSIによると、この対応はDavid Reimerのより弱いButterfly Lemmaによる対応を発展させたもので、対応する設定が各座標で一致する頻度にも上限を設けている。この上限は新たな不等式に必要となる。

リポジトリでは、初等的な証明を4つの部分に分けている。行列式と全単射から全ペア不等式を導くこと、レベル集合上で積分すること、座標について平均を取ること、そして行ごとの上限を点ごとの感度上限とともに確立することだ。これらの手順を組み合わせることで、影響度の明示的な上限が得られる。

リポジトリに記録された監査によると、形式的な証明にはプレースホルダーも追加公理も含まれていない。各宣言はLeanのカーネルと、Leanの型検査器を独立に実装したlean4leanを通じて再検証された。サンドボックス環境では、nanodaとLeanのカーネルを使用する比較器が最終的な4つの定理を受理した。2台目のマシンでは、正しい小規模解を1つ受理し、意図的に誤りを含めた4つの解を棄却した。

こうした検証には明確な限界がある。形式化された記述が、印刷版の予想と一致していることは、読者が確認しなければならない。人間が読める論文自体は機械検証されていない。また、Leanのカーネルとコンパイラー、Mathlibの定義、検証に用いたマシンは、いずれも信頼基盤の一部として残る。

人間の役割と専門家によるレビュー

PSIの技術スタッフであるDavid Turtureanは、研究システムを開発して実行し、問題の範囲を定め、モデルに初稿をまとめるよう促し、その初稿をレビューした。また、論文の正確性に責任を負っている。リポジトリには、数学的記述、初稿、Leanによる形式化をAIモデルが作成したことが明記されている。Jim Halversonが証明を監査し、Phiala Shanahanが形式化についてコメントした。

この発表は、Guy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tanが2026年8月19日に投稿した論文に続くものだ。これらの著者は、並列量子アルゴリズムにおける古典シミュレーションの帰結をすでに確立し、クエリ数がt、ラウンド数がdのアルゴリズムを、ほとんどの入力についてt^(O(d²))回の古典クエリでシミュレートできることを証明していた。PSIによると、4人全員が証明全体を読み進め、コメントを寄せており、専門家向けのより短い解説を準備している。

PSIが公表した評価の中で、研究者たちは次のように記している。「これは非常に大きな成果だ。量子高速化が可能な問題の性質に重要な示唆を与える、数十年来の予想を解決するものである。この証明は、ブール関数の解析と確率的組合せ論における複数の研究の流れを土台とし、それらを発展させている。すべてが、まさに魔法のような形で一つにまとめられている。」

まず確かめるべき点は、異例なほど具体的だ。独立したカーネルによって符号化された論証を再実行できる一方、符号化された命題がAaronsonとAmbainisの予想に合致していることを専門家が確認し、Leanの対象外となる論文の部分を評価する必要がある。この役割分担によって、機械検証で何が確立され、何に依然として人間による数学的検討が必要なのかが決まる。