米フィジカル・スーパーインテリジェンス（Physical Superintelligence、以下PSI）は2026年11月6日、理論計算機科学の未解決難問「アーロンソン＝アンバイニス予想」を、アンソロピック（Anthropic）の非公開AIモデルを活用した自社システムにより、わずか3日間の稼働で完全証明したと発表しました。量子技術・イノベーション立国戦略のもとでハードウェア開発とアルゴリズム探索を進める理化学研究所や国内量子スタートアップにとって、投資領域を非構造化データから特定の構造化問題へ明確に絞り込む技術的判断材料となります。
3日間の自律稼働がもたらした理論計算機科学の決着と市場の反応
理論計算機科学者のスコット・アーロンソン（Scott Aaronson）とアンドリス・アンバイニス（Andris Ambainis）が提唱した「アーロンソン＝アンバイニス予想（Aaronson-Ambainis Conjecture）」は、2008年の提起から長年未解決のままでした。この予想は、量子コンピュータが古典コンピュータに対して指数関数的な計算速度の優位性（スピードアップ）を獲得するために「入力データの数学的構造」が不可欠であるかを問うものです。
2026年11月6日、マサチューセッツ州ケンブリッジを拠点とするPSIの技術スタッフであるデビッド・トゥルトゥレアン（David Turturean）氏は、単独著者として60ページの証明論文を公開しました。同時に、証明支援系プログラミング言語「Lean 4（バージョン4.33.0）」と数学ライブラリ「Mathlib」を用いた形式検証コードをGitHub上に公開しています。
アーロンソン＝アンバイニス予想を巡るタイムライン
本予想の提示から今回の証明、そして業界の反応に至る時系列は以下の通りです。
| 年月日 | 主体 | 出来事・進展の詳細 |
|---|---|---|
| 2008年〜2014年 | S. Aaronson、A. Ambainis | 予想を提起。2014年に学術誌『Theory of Computing』へ論文掲載 |
| 2019年 | N. Keller、O. Klein | 同予想の証明を発表するも、補題の誤りにより著者自ら撤回 |
| 2026年8月19日 | スタンフォード大学研究チーム | クエリの並列ラウンド数が固定された特殊ケースの証明をプレプリント公開 |
| 2026年9月1日 | 米PSI | ブレークスルー・エナジー・ベンチャーズ主導で5,800万ドル調達し発足 |
| 2026年11月6日 | 米PSI | Anthropicの非公開モデルを用い、一般ケースの完全証明を発表 |
PSIは、ビル・ゲイツ（Bill Gates）氏が創設したブレークスルー・エナジー・ベンチャーズ（Breakthrough Energy Ventures）が主導するシードラウンドで、2026年9月に5,800万ドルの初期資金を調達した公益企業（Public Benefit Corporation）です。同社は「仮想の物理学者（Virtual Physicists）」を組織内に構築し、物理法則の発見や計算理論の解明を目的としています。
証明された定理の技術的帰結
アーロンソン＝アンバイニス予想の成立が意味するのは、量子アルゴリズムが非構造化データやランダムな入力に対して、古典計算を指数関数的に上回るクエリ優位性（データ読み取り回数の優位性）を持たないという事実です。
ピーター・ショア（Peter Shor）氏が1994年に考案した素因数分解アルゴリズム（Shorのアルゴリズム）は、計算対象が内に秘める「周期性」という高度な数学的構造を利用して指数関数的な高速化を実現しています。一方で、データベース検索などに代表される非構造化問題に対しては、グローバー（Grover）のアルゴリズムが示す多項式（2乗）の高速化にとどまります。今回の証明は、ブール立方体上の多項式において、変動性の高い関数には必ず影響度の大きい変数が存在することを厳密に特定しました。これにより、入力データに規則性や隠れた周期が存在しない限り、指数関数的な量子クエリ優位性は原理的に現れないことが数学的に確定しました。
スタンフォード大学のガイ・ブラン（Guy Blanc）氏らの研究チームは、PSIの成果に対して「極めて大きな成果であり、異なる研究の流れを結びつけた」と評価し、専門家向け解説の作成に入っています。一方で、マサチューセッツ工科大学（MIT）の研究者が大学院生やポスドクを対象に実施した調査では、回答者の76%が「AIの発展によって研究意欲が低下した」「修了後に数学のアカデミアに残る可能性が低い」と回答するなど、研究現場の心理面にも劇的な変化が生じています。
参考記事: 量子優位性とは？量子超越性・ユーティリティとの違いと2030年までの導入ロードマップ
階層型AIエージェントと形式検証「Lean 4」による自律証明のアーキテクチャ
今回の成果における技術的特異点は、AIが単に論理の断片を出力したのではなく、形式検証器のフィードバックループを通じて3日間の単一実行内で自ら証明を段階的に最適化した点にあります。
[監督エージェント (Anthropic非公開モデル)]
│ 課題指示・進捗監視
▼
[探索・発想エージェント] ── 命題・証明コード生成 ──► [形式検証器 (Lean 4.33.0)]
▲ │
└──────── 検証エラー／合格シグナル ───────────────┘
多階層エージェントによる探索と反復改善
PSIが構築した社内システムでは、Anthropicの非公開フロンティアモデルの複数インスタンスが役割を分担して協調動作しました。
- 文献に存在する既存の数学的着想を探索・抽出するインスタンス
- 新たな補題や論理ステップを考案し、これらを組み合わせて証明コードを記述するインスタンス
- 全体の進行状況を監督し、エージェント間の整合性を保ちながら改善を指示するインスタンス
システムは稼働3日目の途中で最初の完全な証明を生成しました。その際、多項式の影響度限界指数は初期段階で「22」という粗い値でした。PSIの指示により、システムは中間結果をさらに推し進め、指数を「11」へ縮小し、最終的に予想が求めていた「7（$(\epsilon/d)^7$）」にまで同一実行内で到達しました。
| 最適化フェーズ | 影響度限界指数 | 適用手法 | Lean 4検証結果 |
|---|---|---|---|
| 初回証明達成（3日目） | 22 | 基本的な多項式の展開 | 受理（Accepted） |
| 中間改善 | 11 | レベル別積分（Integration by level） | 受理（Accepted） |
| 最終証明 | 7 | 座標平均化（Coordinate averaging） | 受理（Accepted） |
形式検証系Lean 4が保証した境界線
本成果の信頼性を担保しているのが、定理証明支援系言語Lean 4のカーネルによる機械検証です。PSIが公開したリポジトリでは、証明コード内にプレースホルダ（未証明部分を示すsorry）や独自の追加公理は一切含まれていません。数学ライブラリMathlibが定義する3つの標準公理のみに依存しており、独立した検証器であるleancheckerやRust製の検証器nanodaでも検証の再現が確認されています。
ただし、機械検証が保証する範囲には明確な限界が存在します。
- 機械が保証するのは、Leanコード内で記述された定義式（
PrintedConjecture）から結論が導かれる論理的一貫性のみであること。 - その定義式が、アーロンソン氏らが本来意図した数学的予想と厳密に一致しているかの判断は人間に委ねられていること。
- 同梱された60ページの解説論文の自然言語テキスト自体は、機械検証の対象外であること。
AIが自律的に仮説を立て、コード化し、検証器のエラーメッセージをもとに証明を自己修正するループの成立は、理論研究の作業工程を根本から塗り替えました。
参考記事: AnthropicのAI、耐量子暗号「HAWK」の脆弱性を特定
国内の量子技術開発ロードマップとAI主導型研究への構造的示唆
アーロンソン＝アンバイニス予想の証明と、AIによる研究サイクルの短縮は、日本の産業界と研究機関に対して2つの具体的な針路修正を求めています。
量子アルゴリズム投資の絞り込み
国内では、文部科学省のQ-LEAP（光・量子飛躍フラッグシッププログラム）や量子技術イノベーション拠点（QIH）を中心に、ハードウェアからソフトウェアまでの研究開発投資が進められています。民間企業においても、ビッグデータ処理や機械学習の全般的な高速化を期待して量子アルゴリズムを探索する動きが見られました。
しかし今回の証明により、ランダムかつ非構造化なデータ探索において、量子計算が古典計算を指数関数的に突き放すシナリオは理論的に否定されました。日本企業が限られた計算資源と研究予算を配分すべき対象は、明確な代数的・幾何学的構造を持つ領域に限定されます。
- 材料開発・創薬: 量子化学計算における分子軌道のハミルトニアンシミュレーション
- 暗号・セキュリティ: 隠れ部分群問題に基づく耐量子計算機暗号（PQC）の解析
- 構造化最適化: グラフ構造や明確な対称性を持つ組合せ最適化問題
ビッグデータの検索や汎用アナリティクスに量子優位性を期待した事業計画は前提を見直す必要があります。
「形式検証＋AI」パイプラインの導入障壁と実務的対応
もう一つの示唆は、科学研究およびミッションクリティカルな設計における「AI＋形式検証」の必須化です。日本の学術機関や製造業の研究開発部門では、AIによる自然言語の要約やアイデア出しの導入は進んでいるものの、Lean 4やCoq、Isabelleといった形式検証器を統合した検証パイプラインの運用実績は極めて限られています。
この背景には、数学や論理仕様を形式言語へ厳密に落とし込める専門人材の不足があります。海外では、フロンティアモデルと形式検証基盤を垂直統合した研究システムが未解決問題を数日で処理する水準に達しています。国内の開発組織が直ちに着手すべき実務的アクションは、ソフトウェアの仕様策定、組込みシステムの安全性検証、および数理モデルの評価プロセスにおいて、LLMの出力結果を形式検証器で閉ループ検証する開発環境の構築です。研究者の役割は、長文の検証作業から「解くべき問題の厳密な形式定義」と「検証結果の産業的妥当性の評価」へとシフトしています。
読者が次に取るべきアクション
未解決難問がAIと形式検証器によって数日で解決される環境において、技術責任者や投資家は以下の具体的な評価手順を実行する必要があります。
- 自社量子プロジェクトの対象問題の再分類
現在推進または出資している量子アルゴリズム検証プロジェクトについて、解こうとしている問題が「非構造化データ」に依存していないかを点検してください。周期性や群構造などの数学的規則性を持たない問題への指数関数的スピードアップの期待は排除し、多項式加速にとどまる前提で投資対効果を再試行する必要があります。 - 形式検証ツールの社内PoC着手
クリティカルなアルゴリズムやプロトコルの設計において、LLMによるコード生成単体に依存せず、Lean 4などの証明支援系を用いた「機械的検証ループ」を組み込む実証実験を開始してください。命題の記述と機械検証を自動化するパイプラインの有無が、研究開発の検証速度を左右します。 - 外部専門家による最終査読の推移確認
スタンフォード大学のブラン氏らによる解説論文、および提唱者であるアーロンソン氏の技術的見解を継続して追跡してください。Leanコード内の命題定義が元の予想と完全一致しているかの確定診断をもって、技術選定の確定値とすることが肝要です。
出典: 米PSIによるAaronson-Ambainis予想の証明発表（Pasquale Pillitteri）
出典: PSI公式リサーチ発表
出典: Unite.AI報道
出典: Business Insider報道
