量子コンピュータは、あらゆる計算問題を従来のコンピュータより高速に解けるわけではない。その代表例が、Peter Shorが1994年に発表した素因数分解アルゴリズムだ。ショアのアルゴリズムが既知の主要な古典アルゴリズムより大幅に高速なのは、対象となる数学的問題に潜む周期性を利用しているためである。つまり、量子コンピュータの強みを引き出すには、問題が持つ数学的構造が重要な役割を果たす。

では、そうした構造を利用できないランダムな入力に対しても、量子コンピュータは古典コンピュータを指数関数的に上回る高速化を達成できるのだろうか。計算複雑性理論におけるこの未解決問題に対し、Scott AaronsonとAndris Ambainisは2008年、純粋数学の命題を通じて答えを導く方法を提案した。彼らの研究はarXivにプレプリント(arXiv:0911.0996)として登録され、2014年には学術誌『Theory of Computing』第10巻(133〜166ページ)に掲載された。その中で提示された予想が正しければ、一様ランダムに選ばれた大半の入力について、量子アルゴリズムを多項式個のクエリで古典的に模倣できることが示されていた。

2026年11月6日、研究機関Physical Superintelligence(PSI)のDavid Turtureanは、この「アーロンソン・アンバイニス予想」を証明したとするプレプリントを公開した。同時に、定理証明支援系「Lean 4」を使った形式検証コードも公開している。今回の成果は、物理的な量子コンピュータを使った実験ではなく、数学的な証明とその機械検証に関するものだ。また、証明の発見から論文化までの過程にAIが関与したことも注目されている。

AD

量子計算の高速化を支える数学的構造とは何か

この研究の舞台となるのは、アルゴリズムが入力データにアクセスする回数を評価する「決定木クエリ計算量モデル」である。通常の計算時間とは異なり、計算機が内部で行う演算の回数は考慮せず、入力への問い合わせ回数だけを計算コストとして数える。古典アルゴリズムは1回のクエリで入力の1ビットを読み取るのに対し、量子アルゴリズムは複数のビット位置の重ね合わせを利用したクエリを実行できる。この違いが、量子アルゴリズムによる高速化を考える出発点となる。

1998年、Robert Beals、Harry Buhrman、Richard Cleve、Michele Mosca、Ronald de Wolfらは、量子クエリ計算量と多項式の次数を結び付ける重要な結果を示した(arXiv:quant-ph/9802049)。任意の量子アルゴリズムが回のクエリを実行する場合、そのアルゴリズムが特定の入力を受け入れる確率は、入力ビットを変数とする実数多項式で表現できる。この多項式の次数は最大でも$2T$であり、受理確率を表すため、ブール入力に対する値は常に0から1の範囲に収まる。これにより、量子アルゴリズムの性質を、多項式に関する数学的問題として調べられるようになった。

AaronsonとAmbainisが着目したのは、この有界な低次多項式を古典アルゴリズムで近似する方法だった。少数の入力ビットを調べるだけで多項式の値を十分な精度で予測できれば、量子アルゴリズムの受理確率も効率よく推定できる。そこで彼らは、入力全体に対して一定以上の変動を持つ有界低次多項式には、十分に大きな「影響力」を持つ変数が少なくとも1つ存在すると予想した。今回の研究は、この数学的予想を証明することで、長年未解決だった量子クエリ計算量の問題を解決したとするものである。

有界低次多項式には影響力の大きい変数が必ず存在する

今回証明された主定理を、数学的に整理してみよう。長さのブール文字列を入力とし、それぞれのビットが0または1を取る空間を考える。を変数の実多項式とし、その次数を以下とする。また、すべてのブール入力に対してが成り立ち、一様分布に従う入力について、多項式の値の分散がを満たすと仮定する。

ここで重要になるのが、個々の入力ビットが多項式の値に及ぼす「影響力(influence)」である。あるビットを反転させたとき、多項式の値が大きく変わるなら、そのビットは強い影響力を持つ。今回使用する影響力は、値の変化を単純に平均したものではなく、変化幅の二乗の期待値として次のように定義される。

ここでは、入力文字列の番目のビットだけを反転させたものを表す。Turtureanの主定理は、前述の条件を満たす多項式について、少なくとも1つの座標が次の不等式を満たすことを示している。

定数は、次のように明示されている。

この結果の重要な点は、影響力の下界が入力変数の総数に依存しないことである。入力ビット数がどれほど増えても、多項式の次数と分散だけから、一定以上の影響力を持つ変数の存在が保証される。しかも、影響力の下界は次数に対して指数関数的に小さくなるのではなく、多項式の逆数として与えられている。この性質が、量子クエリ計算量に関する予想を解決する鍵となった。

従来、一般的な有界実多項式について知られていた影響力の下界は、次数が増えるにつれて指数関数的に減少するものだった。初期の結果は、Irit Dinur、Ehud Friedgut、Guy Kindler、Ryan O'Donnellらが2007年に示したフーリエ解析の定理から導かれていた。しかし、次数が大きくなると保証できる影響力が急速に小さくなるため、AaronsonとAmbainisが必要とした古典シミュレーションの効率を保証するには不十分だった。

一方、出力値が0または1に限られるブール値関数については、Ryan O'Donnell、Michael Saks、Oded Schramm、Rocco A. Servedioによる決定木の研究(2005年)や、Noam NisanとMario Szegedyの研究(1994年)などから、対応する性質がすでに知られていた。さらに、Ashley Montanaro(2012年)、Paata Ivanisvili(2026年)、Nikhil Bansal、Makrand Sinha、Ronald de Wolf(2022年)、Francisco Escudero Gutiérrez(2023年)らによって、さまざまな特殊ケースで進展があった。しかし、0から1までの任意の実数値を取り得る一般の有界低次多項式について、次数の多項式に反比例する影響力の下界を証明することはできていなかった。今回の研究は、この一般的なケースに初めて解を与えた点で重要である。

ただし、今回導かれた分散の乗、次数の6乗という指数や、係数が理論上の最適値であると証明されたわけではない。これらは予想を解決するのに十分な、明示的な下界として導かれたものであり、さらに改善できる余地がある。また、今回の定式化では入力変数をで表しているが、ブール関数解析ではを用いる場合もある。表現方法によって影響力の定義に含まれる係数などが変わるため、異なる定式化の数値を直接比較する際には注意が必要だ。

AD

量子アルゴリズムの古典シミュレーションはどこまで可能になるのか

有界低次多項式には十分な影響力を持つ変数が存在するという予想が証明されたことで、AaronsonとAmbainisが提示していた古典シミュレーション定理の前提条件が満たされた。彼らの原論文における定理3.3は、影響力に関する予想が正しければ、量子アルゴリズムの受理確率を古典アルゴリズムで効率よく推定できるとするものだ。具体的には、回のクエリを実行する量子アルゴリズムに対して、ある決定論的な古典アルゴリズムが存在する。この古典アルゴリズムは、任意に指定した相加誤差と例外割合について、一様分布から選ばれた入力の少なくともの割合で、の受理確率を誤差以内に推定できる。

このとき、必要な古典クエリ数の上界は次のように表される。

つまり、今回の証明が正しければ、従来は予想を前提としていたこの結果が、無条件に成立することになる。誤差と例外割合を固定した場合、古典アルゴリズムに必要なクエリ数は、量子アルゴリズムのクエリ数に対して多項式の範囲に収まる。したがって、一様ランダムな入力について、大半のケースで量子アルゴリズムの受理確率を近似するという目的に限れば、クエリ数における指数関数的な差は生じない。

ただし、この結果を「量子コンピュータの優位性が否定された」と解釈するのは誤りである。定理が保証するのは、あくまで特定の条件下での古典シミュレーションであり、適用範囲には重要な制約がある。

第一に、この保証は最悪ケース(worst-case)ではなく、平均ケース(average-case)に関するものだ。入力全体のうち最大の割合を占める例外的な入力では、古典アルゴリズムの推定誤差がを超えても構わない。例えば、問題の解が入力空間のごく一部に集中している場合、今回の定理だけでは、その特殊な入力を効率よく処理できるとはいえない。また、許容誤差や例外割合を小さくするほど、必要なクエリ数は増える。

第二に、クエリ数が多項式で抑えられることと、実際の計算時間が多項式で抑えられることは別問題である。クエリ計算量モデルでは、入力データへのアクセス回数だけを評価し、クエリの間に必要となる内部演算やメモリ操作のコストを考慮しない。このため、古典アルゴリズムが多項式個のクエリで受理確率を推定できたとしても、その処理全体が多項式時間で完了するとは限らない。今回の定理が、そのまま実用的な量子回路シミュレータの高速化につながるわけではない。

第三に、古典アルゴリズムが近似するのは、量子アルゴリズムが最終的に出力する受理確率という単一の数値である。量子回路内部の量子状態ベクトル全体を再現したり、あらゆる測定方法に対する確率分布を効率よく計算したりすることまで保証するものではない。この違いは、多数の量子ビットからなる量子状態を古典的に模倣する問題を考える際に特に重要となる。

第四に、今回の結果は多項式オーダーの量子高速化を否定しない。例えば、Groverの探索アルゴリズムによる平方根オーダーの高速化は、今回の定理と矛盾しない。また、ショアのアルゴリズムのように周期性などの数学的構造を利用する問題についても、今回の定理だけで量子アルゴリズムの優位性が否定されるわけではない。特定の条件を満たす入力だけを対象とする「約束問題(promise problem)」にも、同じ結論をそのまま適用することはできない。

関連する研究として、2026年8月24日にはスタンフォード大学のGuy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tanが、重要な部分的成果を発表している(arXiv:2608.19158)。この研究では、入力への問い合わせを固定回数の並列ラウンドで実行する、適応性が制限された量子アルゴリズムについて、ランダム入力に対する指数関数的な高速化が存在しないことを証明した。今回のTurtureanによる成果は、こうしたラウンド数の制限を設けず、一般の適応型量子クエリアルゴリズムを対象とする予想を解決した点で異なる。

レベル集合と全ペア不等式を用いた証明の仕組み

Turtureanの証明は、まったく新しい発想だけから生まれたものではない。重要な土台となったのは、Shachar LovettとJiapeng Zhangが2023年に提案した「分数証明書(fractional certificate)」を利用する証明戦略である(LIPIcs.ITCS.2023.84)。両者は、影響力の大きい変数の存在を示すための有望な方法を提示していたものの、その方法を完成させるうえで必要な組み合わせ論的な不等式は未証明のままだった。Turtureanは、この障害を別の不等式によって乗り越えた。

LovettとZhangの基本的な発想は、多項式の値域である区間を複数の閾値で区切り、各閾値以上の値を取る入力の集合を調べるというものだ。こうした集合は「レベル集合」と呼ばれる。各レベル集合について入力ビットに非負の重みを割り当て、複数のビットを反転させた場合の関数値の変化を、対応する重みの総和で評価する。この方法を使えば、多項式全体の振る舞いを個々の座標の寄与に結び付けられる可能性がある。しかし、証明を完成させるには特定の組み合わせ論的不等式が必要であり、そこが未解決の問題として残されていた。

Turtureanは、LovettとZhangが予想した不等式を直接証明する代わりに、新たな「全ペア不等式(all-pairs inequality)」を導入した。この不等式の証明で中心となるのは、単項式で構成された行列の行列式を解析し、その最低次数の項を利用して構築した全単射(一対一対応)である。入力空間内の点を適切に対応付けることで、必要な評価を導く仕組みとなっている。

この構成には、David Reimerが1999年にvan den Berg-Kesten予想を解決した際に用いた「バタフライ補題(Butterfly Lemma)」と共通する考え方がある。ただし、Reimerの手法による対応付けだけでは、今回必要となる評価を導くには条件が弱すぎる。Turtureanは、対応付けられた2つの入力が特定の座標でどの程度一致するかを制御する、より厳密な条件を組み込んだ。この座標の一致に関する制約によって、全ペア不等式の証明が可能になった。

証明は、この不等式を出発点として段階的に進む。まず、全ペア不等式をすべてのレベル集合にわたって積分し、関数の3次モーメントに関する不等式を導く。次に、この3次モーメントの評価から、少なくとも1つの座標について、関数値の平均絶対増分(mean absolute increment)が十分に大きいことを示す。最後に、座標に関する平均化を行い、絶対増分の評価を二乗平均で定義される影響力の下界へと結び付ける。

この過程では、分数証明書の重みに関する上界と、各入力点における感度(pointwise sensitivity)の上界が組み合わされる。これらの評価を積み重ねることで、最終的な影響力の下界に次数の6乗が現れる。こうして、従来は指数関数的な次数依存性しか得られていなかった一般の有界実多項式について、多項式オーダーの下界が導かれた。

今回の成果と、その解釈において注意すべき点を整理すると、次のようになる。

論点 今回示された内容 根拠・検証状況 注意すべき点
数学の主定理 有界低次実多項式には、変数総数に依存せず、以上の影響力を持つ変数が存在する。 TurtureanのプレプリントとLean 4の形式検証コード 下界の指数や係数が最適値と証明されたわけではない。
量子クエリ計算量 固定された誤差と例外割合のもとで、大半の一様ランダム入力に対する量子アルゴリズムの受理確率を、多項式個の古典クエリで近似できる。 AaronsonとAmbainisの2014年の論文における定理3.3と今回の主定理 量子優位性全般の否定ではなく、多項式時間の古典シミュレーションも保証しない。
形式検証 主要な4つの定理宣言がLean 4と複数のチェッカーによる検証を通過したと報告されている。 公開GitHubリポジトリ。Lean 4.33.0、Mathlib v4.33.0を使用 形式化された命題と元の予想の意味的な対応や、論文の自然言語部分まで自動検証されるわけではない。
AIの関与 PSI独自の研究環境で、非公開のAnthropicモデルが証明の発見、形式化、論文初稿の作成を支援した。 PSIの発表と著者による貢献の説明 完全自律での問題解決や、他の難問でも再現できることを示したものではない。

AD

Lean 4による形式検証と、その信頼性の限界

今回の研究が注目されるもう一つの理由は、数学的な証明を記した論文だけでなく、Lean 4による形式検証コードが同時に公開されたことである。Leanは、数学的な命題と証明を形式言語で記述し、その論理的な正しさをコンピュータで検査する定理証明支援系だ。通常の論文では、読者が証明の各段階を読み解いて論理の正しさを確認する必要がある。これに対して形式検証では、記述された証明が定められた論理規則に従っているかを機械的に確認できる。

公開リポジトリには、証明の中心となる4つの定理宣言が含まれている。PSIの報告によると、これらの証明には、未完成の部分を仮に正しいものとして扱うsorryのようなプレースホルダーや、不適切に追加された独自公理は含まれていない。公理への依存関係を調べる#print axiomsを実行した結果、使用されているのは命題外延性(propext)、選択公理(Classical.choice)、商の健全性(Quot.sound)の3つのみだったという。いずれもLeanと数学ライブラリMathlibで標準的に使用される論理的な前提であり、特殊な追加公理に依存して証明を成立させたものではないと説明されている。

検証環境には、Lean 4.33.0とMathlib v4.33.0が指定されている。さらに、PSIによると、Leanの公式ツールleancheckerで証明を再検証したほか、独立した型チェッカー実装であるlean4leanとnanodaによる検証も実施した。複数の実装を使って証明を確認するのは、単一の検証系に不具合があった場合でも、誤った証明が見逃される危険を減らすためである。

その重要性を示すため、公開リポジトリには意図的に誤った命題を使った対照実験も含まれている。Leanのカーネルによる検証を無効化した状態では、偽の命題を含むコードでもlake buildが成功し、追加の公理も表示されなかったという。しかし、このコードを独立したチェッカーで再検証すると、偽の命題は拒否された。この実験は、単にプロジェクトのビルドが成功しただけでは形式検証の正しさを保証できず、カーネルによる証明の検査が不可欠であることを示している。

もっとも、形式検証を行ったからといって、証明に関するあらゆる問題が自動的に解消されるわけではない。特に重要なのは、Leanで形式化された命題(PrintedConjecture)が、AaronsonとAmbainisの元の予想と数学的に同じ内容を表しているかどうかである。Leanは、形式化された命題に対する証明の正しさを検証できるが、その命題が人間の意図した数学的主張と一致しているかどうかを自動的に判断することはできない。定義に抜けや過剰な条件がないか、元の予想を正しく表現しているかについては、数学者による確認が必要となる。

また、論文に書かれた自然言語による説明、先行研究の整理、直感的な解釈、未解決問題についての考察などは、Leanによる検証の対象外である。形式検証そのものも、カーネルやチェッカーの実装、基礎となる定義、実行環境などが正しく機能することを前提としている。独立したチェッカーの使用は、こうした信頼基盤への依存を減らす有効な方法だが、すべての前提をなくすものではない。形式検証の意義は、人間が確認すべき範囲を明確にし、形式化された証明の論理的な誤りを厳密に検出できる点にある。

なお、公開リポジトリには、定数の改善を目指す発展的な定理aaronson_ambainis_of_fbsDegreeBoundも含まれている。ただし、この定理はAgarwalとBen-Davidが導入した予想上の境界条件FbsDegreeBoundを仮定した条件付きの結果である。この仮定自体はリポジトリ内で形式化されていないため、無条件で証明された主定理とは区別する必要がある。

AIは18年間未解決だった数学の難問をどう解いたのか

今回の研究では、数学的な結論だけでなく、証明の発見にAIがどのように関与したかも重要な論点となっている。PSIが公開した説明によると、研究を主導したのは同機関のTechnical StaffであるDavid Turtureanだ。Turtureanは独自の研究用ハーネスを設計し、解くべき問題の範囲を定めたうえでAIシステムを実行した。そのバックエンドには、詳細が公開されていないAnthropicのAIモデルが使用された。

PSIの報告では、システムの稼働開始から3日目に、アーロンソン・アンバイニス予想を解決する証明の全体像が得られ、Leanによる検証も通過したという。その後、関連する未解決問題への適用を試みる過程で、影響力の下界が2度改善され、最終的な形式化が完成した。論文の初稿もモデルへのプロンプトを通じて作成されたが、Turtureanが内容を精査し、数学的な正当性について責任を負っている。さらに、物理学者でAI研究者のJim Halversonが証明を監査し、マサチューセッツ工科大学の理論物理学者Phiala ShanahanがLeanによる形式化について助言した。

ここで重要なのは、この成果が人間の関与なしにAIだけで生まれたものではないという点だ。人間の研究者が問題を設定し、研究環境を構築したうえで、AIによる証明の探索と形式検証を組み合わせている。証明の改善や論文作成にもAIが使われた一方、最終的な内容の確認と数学的な責任は研究者が担った。また、今回公開された論文はGitHubリポジトリを伴うプレプリントであり、現時点で学術誌の査読を完了した成果ではない。

PSIの発表には、前述のスタンフォード大学の研究者であるGuy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tanによる好意的な評価も掲載されている。4人は証明を精読し、長年の予想を解決する重要な成果であることに加え、ブール関数解析と確率的組み合わせ論の研究成果を巧みに組み合わせている点を評価したという。また、専門家向けの簡潔な解説記事を執筆中であることも紹介されている。ただし、こうした専門家による評価は有力な参考材料となるものの、正式な査読プロセスそのものではない。

AIの能力を評価する際にも、慎重な解釈が必要である。稼働開始から3日目に証明が得られ、その後2度の改善が行われたという記録は、今回の研究過程を理解するうえで重要だ。しかし、それだけでAIが同じ問題を繰り返し解ける確率や、数学研究の生産性をどれほど高めるかを定量的に判断することはできない。使用したモデルの詳細なバージョンやパラメータ、プロンプトの構成、他のモデルとの比較、無関係な未解決問題への適用結果などについても、体系的なデータは公開されていない。

したがって、今回の成果を「AIが完全に自律して数学の難問を解決した」と表現するのは正確ではない。一方で、人間が設計した研究環境の中で、AIによる推論とLeanによる形式検証を組み合わせ、長年解かれていなかった重要な数学的問題の証明に到達したことには大きな意義がある。特に、AIが生成した証明を形式的に検査できる仕組みは、数学研究にAIを取り入れるうえで重要な方法の一つとなり得る。

量子計算の限界が明確になった先に残る課題

アーロンソン・アンバイニス予想の証明が示したのは、量子コンピュータの高速化には、問題の性質に応じた明確な限界があるということだ。一様ランダムなブール入力について、一定の相加誤差と例外割合を許容するなら、量子アルゴリズムの受理確率は多項式個の古典クエリで近似できる。これは、量子アルゴリズムがどのような問題で優位性を発揮するのかを考えるうえで、重要な理論的制約となる。ただし、内部計算に要する時間や、周期性などの数学的構造を利用する問題における量子高速化まで制限するものではない。

今後は、公開された証明と形式検証コードについて、数学者や理論計算機科学者によるさらなる精査が進むとみられる。とりわけ、Leanで形式化された命題と元の予想の対応関係を確認し、査読を通じて数学的な成果として定着するかが重要となる。また、今回得られた影響力の下界における次数依存性をどこまで改善できるかも未解決だ。LovettとZhangの証明戦略に関連する他の組み合わせ論的な予想に、今回の全ペア不等式を応用できるかどうかも研究課題として残されている。

AIを利用した数学研究という観点でも、今回の事例は重要な検証対象となる。人間による問題設定、AIによる証明の探索、Leanによる形式検証という組み合わせが、他の長年の未解決問題にも有効なのか、それとも特定の問題と研究環境がうまく適合した結果なのかは、今後の事例を通じて判断する必要がある。今回の成果は、量子計算の理論的限界を明らかにするとともに、AIが数学研究の発見と検証にどこまで貢献できるのかを考えるうえでも、重要な一歩となった。