本文へスキップ
MameTechNews
AI

OpenAI、指数時間仮説の反証をLean形式化して公開

## POINTS

  • ETHの反証はLean形式化済みとされるが、提案者を含む外部グループが公開データで検証する段階にあり、計算量の前提をすぐ捨てる話ではない。
  • 局所平滑化の証明は全次元版で、掛谷予想とSteinの制限予想も導くとされ、自然言語とLeanがGitHubで公開されている。
  • 物理側はQCDと純粋Yang-Millsの存在を含むが、ミレニアム問題の質量ギャップを解いたとは書かれておらず、成果物の公開はグループが保留している。

OpenAIは10月26日、調和解析、計算量理論、場の量子論に関する3件の結果を公開した。いずれも社内モデルの出力を未整理の研究データと位置づけ、外部の専門家が公開の仕方を選ぶ試行だ。

指数時間仮説

計算機科学の結果は、ブール充足可能性の計算量に関する指数時間仮説(ETH)が偽だ、というものだ。OpenAIは、自然言語の反証を10月16日に得て、翌17日にLeanで形式化したと説明している。ETHはグラフ理論やデータベースなど、多くの条件付き困難性の前提になってきた。検証は、ETHの提案者であるImpagliazzo氏とPaturi氏、およびWilliams氏が率いる。3氏の求めに応じ生データは公開され、OpenAIは分野全体の含意を議論する会議の費用も負担する。実用的に速いアルゴリズムが直ちに得られるとは書かれていない。

数学と物理

数学では、局所平滑化予想をすべての次元で示したとし、掛谷予想とSteinの制限予想も全次元で解決すると説明している。出力は10月18日、Lean化は翌19日で、補助的な偏微分方程式を使う新しい証明だという。10月6日の公開と同じ方針で、リポジトリに置かれた。

物理は、ゲージ場とフェルミオンを含む4次元の場の量子論の存在証明で、量子色力学(QCD)、標準模型を含む最も単純な大統一理論、純粋Yang-Millsの存在が対象だ。純粋Yang-Millsの存在はクレイ数学研究所のミレニアム問題の一部に当たると書かれている。質量ギャップまで解いたとは書かれていない。David Gross氏らのグループはAIの成果物をすぐ出さず、自ら書き起こす。Yang-Millsの存在の形式化は10月16日に終わったとしている。

参加者に秘密保持は求めず、報酬もなく、OpenAIは発見そのものの学術的クレジットを求めない。ETH依存の「これ以上は無理」という説明は、公開の検証が一段落するまで暫定扱いになる。