OpenAI、AIが導いた数学・計算機科学・物理の証明をノーベル賞受賞者ら外部専門家に検証依頼

OpenAIは外部の専門家を「shepherds」として招き、助言に基づいて分野ごとに異なる扱いをしている。数学と計算機科学の証明はLeanに翻訳されたが、Leanは記述された命題が証明されたかを確かめるだけで、その命題が本来の問題を捉えているかは専門家の判断が要る。

計算機科学では、OpenAIがETHは偽だと証明したと主張している。ETHはSATが最悪の場合に指数時間かかることを述べる仮説で、多くの論文の前提になってきた。成立しなければそれらの結果は証明済みでなくなるが、直ちに誤りになるわけではない。MITのRyan Williamsは、実用的なSAT求解が12か月以内に大きく進む可能性もあるが、何も起きないかもしれないと述べた。WilliamsはRussell Impagliazzo、Ramamohan Paturiと独立に検証する。無報酬でNDAも結ばず、途中経過を共有する方針だ。三人は関与が主張の支持ではないとする公開書簡も出し、OpenAIは証明の全データを公開し、会議の資金提供も約束した。

数学では、1991年にChristopher Soggeが提唱したlocal smoothing conjectureを全次元で証明したとされる。従来は2019年のGuth、Wang、Zhangによる二次元までだった。これによりKakeya予想とStein's restriction conjectureも全次元で解決されることになるという。この証明には専任の検証グループはなく、外部専門家の助言で証明文とLean版をそのまま公開した。

物理では、四次元で相互作用する特定の量子場理論が存在することを証明したとする。対象はYang-Mills理論、QCD、最も単純な大統一理論の三つである。Yang-Millsについてはミレニアム懸賞問題の存在証明の部分のみで、質量ギャップは解いていないとOpenAIは明言している。2004年ノーベル物理学賞のDavid Grossらが検証し、このグループはAIの資料を当面非公開とし、結果は自分たちで書き上げる予定だ。

OpenAIは、最初の検証者の選び方が誰に先に情報が渡るかを左右するなど、この方式のトレードオフを認めている。科学的功績は主張せず、結果を説明するグループに帰すべきだとし、Simons Foundationに500万ドルを拠出するとも述べた。Williamsらの書簡は、AIの成果をどう検証し、誰がアクセスし、誰の功績とするかという議論も求めている。