OpenAIとAnthropicのモデル、長年の指数時間仮説を反証

OpenAIとAnthropicはともに、計算量理論における長年の予想である指数時間仮説を反証したとする、AIによる成果を発表した。

10月26日、OpenAIは、発表したところによると、同社のモデルは指数時間仮説が誤りであることの証明を生成した。2000年代初頭に提唱されたこの仮説は、3-SATは劣指数時間では解けない、つまり一部の一般的な論理パズルは、考えられるすべての答えを総当たりするより大幅に速く解くことはできない、と主張する。

この仮説は広く受け入れられ、さまざまな分野で条件付きの計算困難性の結果を導くため、数百本の論文で利用されてきた。そのため、これが反証されれば、そうした結果のかなりの部分が無効になり、アルゴリズム、グラフ理論、計算生物学などの分野における問題の計算上の難しさを研究者が再評価する必要が生じる。

このAI企業によると、同社のモデルは10月16日に自然言語による反証を生成し、翌日にLeanの数学証明支援系で形式化した。いずれも公開GitHubリポジトリで入手できる。

OpenAIによると、この成果は、仮説を最初に提唱した人物のうち2人であるカリフォルニア大学サンディエゴ校のRussell ImpagliazzoとRamamohan Paturi、およびMITのRyan Williamsが率いる外部グループによって検証されている。

WilliamsはXで、述べたところによると、研究者たちはこの発見が実用面でどのような意味を持つのか、まだ見極めている段階だという。

「現在の進展ペースなら、今後12カ月以内に実用的なSAT求解について大きな進展が見られる可能性はあります。あるいは、そのようなものは何も見られないかもしれません。正直なところ、私には分かりません」とWilliamsは述べた。

一方、Anthropicは、指数時間仮説を反証することになる形で、決定性アルゴリズムが3-SATを解くことを示す論文とLean 4による形式化を、公開した。同社によると、社内のClaude研究モデルが10月16日、OpenAIのモデルが発見したのと同じ日に、14 million output tokensを使い、人間の入力なしで中核となるアルゴリズムを発見したという。

「この結果は漸近的な性質に限られたもので、実際に公式を解くことについては何も示していない」とAnthropicは指摘した。

これとは別に、OpenAIはAIが生成した別の2つの成果も発表した。調和解析における全次元での局所平滑化予想の証明と、量子色力学や純Yang-Mills理論を含む特定の量子場理論について、数学的に厳密な存在証明を示した。