PSI、内部システムがAaronson–Ambainis予想を証明したと発表

Physical Superintelligence（PSI）は2026年11月6日、非公開のAnthropicモデルを実行する内部研究システムが2008年以来未解決のAaronson–Ambainis予想を証明したと発表した。PSIによると、Leanは実行3日目に完全な証明を受理し、その後2回の改善版も受理した。[1]

Aaronson–Ambainis予想とは何か

PSIは2026年11月6日、内部研究システムがAaronson–Ambainis予想を証明したと発表した。[1] Scott AaronsonとAndris Ambainisは、量子コンピュータがランダム入力で指数関数的に高速化できるかどうかを問い、有名な高速化（Shorのアルゴリズムなど）が利用する隠れた繰り返し構造をほぼ持たない入力を対象とした。

彼らは多項式に関する予想を述べ、それが真であれば量子コンピュータはランダム入力でせいぜい多項式的に高速化されるだけだと示した。[1] PSIは、研究者らがこの予想を量子複雑性理論の中心的な未解決問題の一つとみなしてきたと記している。

PSIはどのように証明を発見したと主張しているか

PSIは、非公開のAnthropicモデルを実行するシステムが、実行3日目にLean受理証明を得たと述べた。[1] 同社は、実行が自社インフラ上で行われ、Leanがすべてのステップを検証し、システムが後で結果を2回改善して最終版もLeanが受理したと主張する。

PSIの技術スタッフメンバーDavid Turtureanがこの研究を主導した。彼は研究システムを開発し、問題の範囲を定め、実行を行い、モデルに結果を論文初稿にまとめるよう促した。[1] PSIは証明とコードを公開GitHubリポジトリに投稿した。[2]

PSIによると、Stanfordの研究者らはすでに2026年8月に、入力の固定回数の並列ラウンドで観察する量子アルゴリズムについて、予想の予測の特殊ケースを証明していた。[1] 同社は彼らが完全な証明を読み、コメントを送り、専門家向けの短い解説を執筆中だと述べている。

文が一致する場合、結果は何を意味するか

形式定理が元の予想と一致する場合、PSIは、通常のコンピュータが量子コンピュータのyes/no確率を小さな誤差内で予測でき、量子ルック数に対する固定べき乗程度にしか増加しないルック数で、少数の文字列を除くすべてを扱えると述べている。[1]

読者は、形式的なLean文が2008年の元の予想と一致することを確認する必要がある。[1][2] PSIのノートは、Lean開発にプレースホルダーや追加公理がなく、独立したカーネルで再検証されたと提示しているが、本記事はその検証を繰り返さない。

私たちの見解

意見: 2008年の有名予想に対するLean検証済み証明は重大な科学的主張であり、PSIが引用するStanfordのコメントは印象的だが、この主張は「形式証明が存在し専門家が検証中」と読み、公に文が一致するまで量子複雑性の書き換えが確定したとは見なすべきではない。

検証できなかった点

• Lean定理が2008年の元のAaronson–Ambainis予想と形式的に同一であること。
• PSI以外が引用・ホストしていない独立した解説。
• 実行に使用された非公開Anthropicモデルの識別情報とバージョン。