11月6日、スタートアップのPSI（Physical Superintelligence）は、未公開のAnthropicモデルを動かす社内研究システムが、18年間未解決だったAaronson-Ambainis予想を証明したと発表した。完全な証明は実行3日目に書き上がり、証明支援系Leanによる逐次検証を通過した。AIが難解な数学に挑むうえでの画期的な主張だが、現時点ではあくまで一社の主張にすぎない。論文はまだ査読を受けていない。
この予想は何を問うているのか
Aaronson-Ambainis予想が問うのは、非構造化データに対して量子コンピュータが古典コンピュータよりどれだけ速くなれるかだ。非構造化入力では、量子アルゴリズムは指数関数的な高速化を実現できない、と主張する。2008年の提起以来、未解決のままだった。今年8月、スタンフォード大学のチームが特殊な場合を先に証明し、PSIによれば自社のシステムがそれを完全な場合へ押し広げた。証明が持ちこたえれば、量子計算の能力の境界に明確な線が引かれる。
機械はどう証明し、何重に検証したのか
PSIによると、研究システムは社内のインフラで連続稼働し、3日目に完全な証明を書き上げ、その後、関連問題で結果を2回改善し、Leanは毎回最終版を受け入れた。PSIは論文とLean 4による形式化証明をGitHubで一緒に公開した。機械検証済みの定理は648件、空欄の証明ステップはなく、追加の公理も導入されていない。命題はLeanカーネルと独立実装のlean4leanでも再実行された。論文の正確性にはPSIの技術スタッフ、David Turtureanが責任を持ち、数学者らが証明を監査した。
教科書に載せるのはまだ早い
機械検証を通過したからといって、数学界に受け入れられたわけではない。Leanが保証できるのは各ステップが規則に従っていることだけで、形式化された命題がAaronsonとAmbainisが当初提示した予想と完全に一致するかどうかは確認できない。その点は専門家の手作業による照合がまだ必要だ。人間が読む論文本文自体も機械検証されていない。証明が数えているのはクエリの回数であって総計算時間ではない。使われたモデルも公開されておらず、Anthropicはコメントを控えた。同じ11月6日、グーグルDeepMindはAIエージェントが1024ビットRSA暗号の新たな弱点を2つ見つけたと発表した。AIは数学と暗号の両面で同時に前進している。PSIの証明が専門家の検証に耐えるかどうか、今後数週間の査読が答えを出すだろう。
