PSI という組織が、量子計算量の理論で15年以上解けていなかった『Aaronson-Ambainis 予想』を、AI で証明したと自社の研究ページで主張した。使ったのは、Anthropic がまだ公開していないモデルだという。PSI は、数学の証明を機械で確かめるソフト Lean の検査を通ったと書いている。一方、人間の研究者による独立した確認はまだない。10月に OpenAI と Anthropic が、計算量の大きな仮説である ETH を反証したと発表したときと同じ構図である。証明が書けるかではなく、正しいと誰が決めるのかが問われている。
日本の会社にとって：大半の会社には、すぐには関係ありません。量子コンピュータの実証や投資を検討している研究開発や新規事業の部門は、ベンダーが言う「速くなる」が問題の特別な構造に頼った話かどうかを、次の提案を受けるときに確かめておくとよいでしょう。証明が確定するまでは、判断の根拠にはしないことです。
何を証明したと言っているのか
Aaronson-Ambainis 予想は、計算量理論の研究者 Scott Aaronson（テキサス大学オースティン校の教授）と、量子アルゴリズムの研究者 Andris Ambainis（ラトビア大学）が2009年ごろに出した予想である。ざっくり言うと、こういう問いだ。問題に特別な構造がなく、入力がでたらめに与えられる場合でも、量子コンピュータは古典のコンピュータより桁違いに速く答えを出せるのか。
予想の答えは「できない」である。量子のアルゴリズムが問い合わせを T 回するなら、古典のアルゴリズムでも T の多項式の回数で、ほとんどの入力についてまねできるとする。数学としては、値が一定の範囲に収まる低い次数の多項式には、必ず影響の大きい変数が1つある、という形で書かれる。これまでは部分的な結果しかなかった。
正しければ、量子コンピュータで劇的に速くなる問題は、素因数分解のように特別な構造を持つものに限られる、という見方に理論の裏づけが付く。「量子なら何でも速くなる」という売り込みに歯止めをかける結果である。
機械の検査が保証すること、しないこと
PSI は、証明が Lean の検査を通ったと書いている。Lean は、証明の一歩一歩が論理の規則に合っているかを機械で確かめるソフトで、AI が書いた長い証明を確かめる手段として、今年いっきに広がった。
ただし、Lean が保証するのは「Lean で書いた言明が、その証明で導ける」ことだけである。その言明が、人間が予想として理解しているものと同じ意味かどうかは、Lean は教えてくれない。10月の ETH の件では、まさにここが問題になった。計算量の研究者 Lance Fortnow はブログで、OpenAI の Lean の言明が論文の主張より少し弱いと指摘した。検査は通っていても、証明したものが看板の主張より弱かったのである。
Lean そのものにも限界がある。7〜8月には Lean の中核部分で、正しくない証明を通しうる不具合が相次いで見つかった。数学者の Thomas Hales は10月、Terence Tao のブログへの寄稿で、いくつもの独立した検査器で同じ証明を突き合わせるよう提案している。Anthropic が ETH の証明で、Lean と別の検査器の両方にかけたのも、そのためである。
ETH の反証と同じ道をたどる
10月26〜27日、OpenAI と Anthropic はそれぞれ、自社のモデルが ETH（3-SAT のような問題は、どう工夫しても総当たりに近い時間がかかるという仮説）を反証したと発表した。どちらも Lean の検査を済ませていた。それでも Anthropic の論文は、執筆の時点で人間は誰も確かめていないと自分で書いた。
検証を頼まれた計算量の研究者 Ryan Williams（MIT）は、一部は型どおりだが「異星のもののように見える部分が2つか3つある」と述べ、研究者の共同体みんなで取り組む必要があるとした。発表から2週間近くたっても、独立した検証が終わったという知らせはない。
確かめる人の選び方にも異論が出ている。数学と AI の助言グループ AGMAI は10月25日、Tao のブログへの寄稿で、AI の成果を会社が選んだ数学者に確かめさせるやり方を批判した。材料に触れられる人が偏ること、会社が選んだ人の評判を盾にできることなどを挙げている。今回の PSI の主張も、同じ物差しで見られることになる。
公開していないモデルという、もう1つの壁
今回は、ETH のときより確かめるのが難しい点がある。使ったモデルを、外の人が使えないことだ。証明の文章と Lean のファイルが公開されていれば、証明そのものは誰でも確かめられる。しかし、同じモデルで同じ結果が出るか、どれだけの試行の中から選んだ結果なのか、人がどこで手を入れたのかは、外からは確かめにくい。
Anthropic のまだ出していないモデルの力が、自社ではなく外の組織の発表を通じて見えてきた点も目を引く。ラボが公開する前に、外部の組織が強いモデルで大きな成果を出したと名乗る形は、これからも増えそうである。
次に何を見るか
見るべき点は3つある。1つ目は、量子計算量の研究者、とりわけ予想を出した Aaronson と Ambainis が、証明をどう評価するか。2つ目は、Lean で書いた言明が、予想の標準の形と同じ強さかどうかを、第三者が突き合わせるか。3つ目は、PSI か Anthropic が、使ったモデルと証明に至った過程を、どこまで明かすかである。
なお、この記事を書くにあたって、PSI のページの細部は確かめられていない。発表の日時、PSI がどんな組織か、使ったモデルの名前と使えるようになった経緯、証明の長さや検査に使った Lean の版、人がどこまでかかわったかは、ここでは書いていない。PSI が主張していることと、Lean の検査を通ったと PSI が書いていることだけを、事実として扱った。
