AI研究企業PSI、量子計算の18年未解決問題を証明

概要

詳細

Aaronson-Ambainis予想とは

量子コンピューターは、特定の構造を持つ問題であれば古典的なコンピューターより指数的に高速に解けることが知られています。一方、Aaronson-Ambainis予想は、入力に特別な構造がないランダムな問題の場合、量子コンピューターの優位性はごくわずか(多項式的な範囲)にとどまるはずだという内容です。PSIによる証明では、ある種の数式(多項式)が一定でない限り、入力のどこかのビットが結果に与える影響の大きさに、具体的な下限があることを示したとされています。これは、従来示されていたよりも強い結果だといいます。

どのように証明されたか

PSIの発表によると、証明作業を主導したのは研究員のTurturean氏です。同氏がシステムを設計し、問題を整理してAIに取り組ませたところ、実行3日目には証明の全体像が得られたといいます。その後、関連する未解決問題にも取り組ませながら、証明の内容を2度改善したとしています。最終的な証明はTurturean氏が精査し、内容の正しさについては同氏が責任を負うとしています。証明の手法は、研究者Lovett氏とZhang氏による既存の方針を土台にしつつ、その中で未解決だった不等式の一つを、新たな方法で証明し直したものだと説明されています。

検証の仕組み

証明は数式証明支援ツール「Lean」でも確認され、PSIは「不足している手順や、新たに追加した仮定はない」としています。さらに、2種類の独立した検証プログラムでも確認が取れたとしています。社内では、アドバイザーのJim Halverson氏が証明全体を確認し、同じくアドバイザーのPhiala Shanahan氏がLeanでの形式化について助言したとされています。社外からは、2026年8月に本予想の特殊な場合を証明していたスタンフォード大学の研究者らが証明を読み、専門家向けの短い解説版を準備していると紹介されています。

注意点

PSIが利用したAIモデルは、Anthropicからまだ公開されていないモデルであるため、どの系列のモデルなのかは明らかにされていません。また、証明そのものはLeanによる形式検証や複数の目によるチェックを経ているとされていますが、学術誌への掲載など、より広い専門家コミュニティによる査読はまだ行われていない段階です。スタンフォード大学の研究者らによる解説版の公開など、今後の検証の進展を踏まえて評価していく必要がありそうです。