PSIのAI研究システム、量子計算の未解決予想を3日で証明

「AIが何年来の数学の超難問を解いた」という見出しを、今年はもう何度か見た人もいるはずだ。9月にはOpenAIがナビエ・ストークス方程式の証明を発表し、懸賞問題のどの部分を解いたのかが曖昧なまま話題になった。フィールズ賞受賞者25人が連名で懸念を表明する騒ぎにもなった。

正直、またかと思った。11月6日、AI研究企業PSIが今度は量子計算の未解決予想を3日で証明したと発表したからだ。だが実際にGitHubの中身を読むと、わざと嘘の証明を混ぜて検査の仕組み自体が機能するか試すところまでやっていた。何を証明し、AIはどうやってそこにたどり着き、その正しさを何がどこまで保証しているのかを、順に見ていく。

量子計算で何が証明されたか

桁の大きな数の素因数分解を、従来のコンピュータよりはるかに速く解く「ショアのアルゴリズム」をご存じだろうか。1994年にピーター・ショアが示した手法で、入力に周期的な繰り返しという「構造」があることを利用している(PSI公式研究ページ)。

では、構造を持たないランダムな入力に対しても、量子コンピュータは同じように指数的に速くなれるのか。Scott AaronsonとAndris Ambainisはこの問いに対し、「ならない」ことを示す予想を立てた。真であれば、yes/noで答える問いに対して、量子コンピュータがランダムな入力で指数的に多くの回数を節約することはない、と言える(problem_statement.md、PSI公式研究ページ)。

予想の中身は、0と1のスイッチ(入力のビット)で決まる多項式の目盛りを使う。多項式は各入力に対して0から1の間の値を返し、その値のばらつきを「分散」、1つのスイッチを切り替えたときに目盛りがどれだけ動くかの平均を「影響度」と呼ぶ。予想が主張するのは次のことだ。値が十分ばらつく多項式には、切り替えると目盛りを大きく動かす、影響力の強いスイッチが必ず1つはある(problem_statement.md)。

PSIは2026年11月6日、自社の研究システムがこの予想の完全な証明を得たと発表した(PSI公式研究ページ)。アーロンソン=アンバイニス予想は、これで定理になった。量子コンピュータの速さには構造という条件が要る、という見立てが裏付けられたことになる。予想の中身が分かったところで、次に気になるのは、AIがどうやってこの証明にたどり着いたのかだ。

AIは3日で証明にたどり着いた

PSIは研究システムを自社のインフラ上で動かし、非公開のAnthropicモデルのインスタンスを使ったと説明している(PSI公式研究ページ、原文”Instances of a non-public Anthropic model were used in the run.”)。一般に公開されているモデルではなく、PSI社内でしか動いていない。

実行開始から、わずか3日目のことだ。研究システムはすでに予想の完全な証明を作り終え、証明支援システムLeanがそれを受理していた(PSI公式研究ページ)。PSIはその後、関連する未解決問題にもシステムを取り組ませ、結果を2回改良して、Leanが最終版を受理したという。

予想の経緯を日付で並べると、次のようになる。

• 2008年: PSIの発表によれば、この年から未解決だった(PSIはどの時点を指しているか本文に書いておらず、確認できなかった)
• 2009年11月5日: AaronsonとAmbainisの論文がarXivに公開される(arXivの投稿履歴)
• 2014年: 学術誌Theory of Computingに論文が掲載される
• 2026年11月6日: PSIが研究システムによる証明を発表

少なくとも10年以上は未解決だった問いに、研究システムは3日で完全な証明を仕上げていたことになる。

数学的な主張、論文の第一稿、Leanによる形式化は、すべてAIモデルが作った。人間側の役割は、PSIのDavid Turturean氏が論文を査読し、その正しさに責任を負うことだったと、GitHubリポジトリは明記している(GitHub README「License and disclosure」)。3日で証明ができたと言われても、それが本当に正しいかどうかは別の話だ。ここからは、PSIがどうやってそれを確かめたのかを見ていく。

証明の正しさをどう確かめたか

てっきり、検査は「Leanが受理した」のひと言で済ませているのだろうと予想していた。実際には、検査の仕組み自体が機能しているかを試すテストまで用意されていた。わざと誤った命題を1つ混ぜたプロジェクトを作る。Leanのカーネル(論理を検査する核の部分)を切った状態でビルドすると、このプロジェクトは何事もなく受理されてしまう。だが、独立した2つのカーネル検査はどちらもこの誤りを弾いたという(GitHub README「A control」)。

証明の検査は、この2つのカーネルだけでは終わらない。GitHubで公開された内容を整理すると、次の4層になる。

表のとおり、静的監査とカーネル再検査は論理の一貫性を、Comparatorは開発元の異なる別ツールでの再現性を、Stanford大の確認は数学としての妥当性を、それぞれ別の角度から裏付けている(GitHub README「Trust boundary」)。

Stanford大のGuy Blanc・Jordan Docter・Carmen Strassle・Li-Yang Tanの4人は、2026年8月に同じ予想の特殊な場合を自分たちで証明していた。入力を一定回数の並列ラウンドでしか読まない量子アルゴリズムに限った場合だ。PSIの発表後にこの証明を読み、コメントを送ったという(PSI公式研究ページ)。4人はこう評している。

This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups. […] Everything is brought together in a rather magical way.

何十年も未解決だった予想を解決する、大きな成果だという評価だ(PSI公式研究ページの引用。Stanford側の一次発信は確認できていない)。開発元・実装・所属のどれも異なる4つの目が、同じ結論にたどり着いている。それでも、この検査が届かない範囲がある。

機械検査が届かない範囲

GitHubのREADMEは、検査が及ばない範囲も自分から書いている。1つは、Leanで書かれたPrintedConjectureという命題が、本当にアーロンソン=アンバイニス予想と同じ内容を指しているかどうかだ。これは論理の整合性とは別の話で、英語で書かれた予想の文章とLeanの記述を読み比べて確かめるしかない、とREADMEは明記している(GitHub README「What these checks do not cover」)。この確認が効くのは論理の一貫性までで、Leanの命題が元の予想を正しく言い換えているかどうかは、この記事が扱った機械検査の外側にある。

論文の本文も同じだ。証明の流れを説明する文章そのものは機械検査の対象外で、どの段落がLeanのどの宣言に対応するかは、別の対応表に人が記録している。Leanのカーネル・コンパイラ・Mathlibの定義、そして検査を実行したマシンそのものは、検査の前提として信頼している、ともREADMEは書いている(同README「What these checks do not cover」)。

Stanford大の4人が証明を読んだのも、この「英語の予想とLeanの記述が対応しているか」を専門家の目で確かめる作業にあたる。発表からまだ数日で、PSI・Anthropicのどちらにも属さない査読者による正式な検証はこれからになる。

まとめ

PSIは2026年11月6日、研究システムが量子計算の未解決予想「アーロンソン=アンバイニス予想」の完全な証明を得たと発表した。使ったのは非公開のAnthropicモデルで、証明にかかったのは3日だった。証明が真なら、構造を持たないランダムな入力で量子コンピュータが指数的に高速化することはない、と言える。証明の正しさは、Leanの受理だけでなく、ソースコードの静的監査、実装の異なる2つのカーネルによる再検査、外部ツールComparatorでの照合、そしてStanford大の研究チームによる内容確認という4層で裏付けられている。

一方で、Leanの命題が元の予想を正しく言い換えているかどうかは機械検査の対象外で、ここは専門家が文章を読み比べて確かめる領域になる。「Leanで検証された」という発表を見たとき、どこまでが機械的な確認で、どこから先が専門家の確認なのかを分けて読めば、その発表の裏付けがどれだけ厚いのかを自分で見積もれるようになる。