コンピューティングの限界をめぐる数十年来の仮定に、思いがけない挑戦者が現れたのかもしれない。それは人工知能だ。
同社は10月26日、同社のモデルが指数時間仮説（ETH）に反する証明を生成したと発表した。ETHは、特定の計算問題を解く難しさに関する長年の仮定だ。研究者たちは数百件の研究でETHに依拠しており、今回の新たな成果によって、これまでの結論の一部を見直す必要が生じる可能性がある。
ただし、数学上の画期的な成果が、そのまま高速なコンピューターにつながるわけではない。独立した研究者がなお証明を検証する必要があり、その成果に基づく実用的なアルゴリズムを見つけるには、さらにかなりの作業が必要になる可能性がある。
OpenAIのAIは、計算分野の基盤となる仮定にどう挑んだのか
OpenAIの発表によると、同社のAIモデルは10月16日、ETHに挑む証明を生成した。同社は翌日、数学的証明を検証するツールであるLeanを使って、その成果を形式化した。
ETHは、特定の計算問題、特にブール充足可能性問題、すなわちSATを解くのに必要な時間に関する仮説だ。簡単に言えば、変数の数が増えるにつれて、標準的な3-SAT問題のすべての例を劣指数時間で解けるアルゴリズムは存在しないとする仮説である。
この仮説は、ほかの計算問題をどれほど効率的に解けるかについて、条件付きの限界を研究者が示すのに役立ってきた。ETHが誤りなら、こうした結論の一部は再検討が必要になる。
OpenAIはETHについて「広く正しいと信じられている」と表現した。研究者たちは数十年にわたり、グラフ理論、計算生物学、データベースなどの分野で、計算の限界を研究するためにETHに依拠してきた。
OpenAIは、2種類の証明をともに公開した。UC San DiegoのRussell Impagliazzo氏とRamamohan Paturi氏、そしてMITのRyan Williams氏が、成果を検証する独立グループを率いる。
反証がアルゴリズム研究を変える可能性
OpenAIの証明が正しいと確認されれば、研究者は、どの計算問題を解くのが難しいかを示すためにETHに依拠した過去の研究を見直す必要に迫られるかもしれない。
しかし、 計算量の仮説に異議を唱えても、既存のソフトウェアが突然高速に動いたり、複雑な問題が解きやすくなったりするわけではない。
OpenAIも、さらなる作業が必要だと認めている。「こうしたアルゴリズムを見つけ、理論上の進展を実用的な改善につなげるには、今後かなりの研究が必要になる」
Interesting Engineeringも、局所平滑化予想と量子場理論に関する、AIが生成した別の2つの証明を報じている。研究者たちは、これらの成果を別々の審査プロセスで検証している。
eWeekが見いだしたこと：証明がコンピューティングを変える前に必要な3つの検証
OpenAIは証明を公開し、独立した検証の計画を示した。しかし、この成果が現実のコンピューティングの改善につながるには、研究者がなおいくつもの疑問に答える必要がある。
研究上の節目 | これまでに行われたこと | 今後必要なこと |
| 形式的証明 | 自然言語版とLean版が公開されている | 独立した研究者が証明を検証し、解釈しなければならない |
| 科学的含意 | ETHに基づく仮定に異議を唱える証明 | 過去のどの成果を見直す必要があるか、研究者が判断しなければならない |
| 実用的なアルゴリズム | より高速な実運用アルゴリズムはまだ実証されていない | コンピューティング性能を向上させる可能性のあるアルゴリズムを、研究者が開発・検証する必要がある |
OpenAIが報告した証明の意義は、難しい数学の問題を解いたことにとどまらない。ETHは計算量理論に関する数十年にわたる研究を形作り、特定の問題をどれほど効率的に解けるかについて、科学者が限界を示すのに役立ってきた。
反証が検証されれば、研究者はこの仮説に依存する成果を見直す必要に迫られる可能性がある。ただし、別の数学的議論によって裏付けられた成果はそのまま維持される。
より大きな問題は、この発見が最終的により優れたアルゴリズムにつながるかどうかだ。ETHを反証できれば、特定の計算問題を理論上はより高速に解けることが示される。しかし、それだけで現実の用途に適したアルゴリズムが生まれるわけではない。
その数学的な洞察を、測定可能な性能向上へとつなげるには、さらに何年もの研究が必要になる可能性がある。
この成果は、AIを活用した科学的発見が抱える課題も浮き彫りにしている。OpenAIによると、同社の証明はLeanを使って形式化された。Leanは、数学的な議論が指定された論理規則に従っているかを検証する。
しかし、形式検証は、証明の前提や解釈、より広範な意味について独立した精査に取って代わるものではない。研究者は、この成果が計算量理論にとって何を意味するのか、またアルゴリズム開発に意義のある新たな方向性を開くのかを、なお明らかにしなければならない
以前の Scientific Americanによる調査は、 AIを活用した数学について、形式的な検証が正しさを裏付けている場合でも、数学者がAI生成の証明を解釈することがいかに難しいかを示した。
課題は、証明が有効かどうかを確かめることだけではない。それが機能する理由を理解し、その洞察を今後の研究にどう生かせるかを見極めることも必要だ。
OpenAIの証明が開発者と企業にとって意味すること
企業は、OpenAIの発表を理由にソフトウェアが高速化すると期待すべきではない。同社は、データベースの性能や最適化ツール、その他の本番環境で使われるソフトウェアについて、改善を実証していない。
開発者や研究チームにとっては、さらに調査すべきことがある。公開された証明を確認し、自分たちの既存研究がETHに依存しているかどうかを調べ、独立した研究グループの成果を追うことができる。
一方、IT部門の責任者が、この発表だけを根拠にインフラ計画やソフトウェア予算を変更する理由はほとんどない。将来的なコンピューティングの改善も、既存のソリューションと比較しながら開発、検証、測定する必要がある。
研究者が最終的にこの証明を使って高速なアルゴリズムを開発できれば、その恩恵は複雑な計算や大規模データセットに依存する業界にまで広がる可能性がある。
それまでは、企業はAIが生成した 数学上の発見が可能にするかもしれないことではなく、自社のシステムが実際に提供できる性能によって、コンピューティング性能を判断する方がよい。
関連記事：AIが生成した数学研究への懸念にOpenAIがどう対応しているかについては、 500万ドルの拠出で数学者と独立検証を支援しようとしている方法を読む。