何が起きたか

OpenAIが8月1日、数学と理論計算機科学の未解決問題10件について、AIが出した結果を公開しました。対象は、公式の表現で「主要な結果について少なくとも10年、多くの場合はもっと長く進展がなかった」問題です。

分野は高次元幾何、符号理論、算術回路の複雑性、群論、作用素環、量子計算量、格子暗号、極値組合せ論にまたがります。個別の名前を挙げると、球の詰め込み密度の上界、コンヌの剛性予想の反証、エルデシュの問題183・146・180などが並んでいます。

ここが大事なのですが、使われたのは今のChatGPTではありません。次の主力モデルとされる「Astra」の社内版です。つまり、いま同じことを手元で試せる話ではありません。

手順も公開されています。モデルが数学的な議論を生成し、論文の形に整えたのは人間（同じモデルを使いながら）、そのあとモデルが各証明をLeanという形式検証の仕組みに変換して、GitHubで公開しています。解を見つけるまでに必要だったトークン量は、同社のSol APIの料金に換算して合計およそ2,000ドル相当だったとのことです。

生活で何が変わるか

正直に言うと、今日の家事や仕事が変わる発表ではありません。球の詰め込みの上界が改善しても、献立は決まりません。

それでも取り上げたのは、AIを説明するときによく使われる「結局は既にある文章を混ぜて出しているだけ」という言い方が、この件についてはそのままでは当てはまりにくいからです。まだ誰も書いていない問題への答えを出した、という主張になっています。

ただし、受け取り方には慎重さが要ります。

  • 中身の評価はこれからです。OpenAIは「数学コミュニティがこれらの結果に深く関わり、文脈の中に位置づけてほしい」と呼びかけている段階で、外部の専門家の判断はまだこれからということになります
  • 10件すべてが「完全解決」ではありません。球の詰め込みの上界、算術回路の下界のように、既存の限界を押し上げた結果も含まれます。原題も「10 advances（10の前進）」です
  • Leanで公開されている点は重いです。形式検証は、証明の筋が通っているかを機械がチェックできる形にするもので、「すごい結果が出ました」という発表よりは検証しやすい状態になっています
  • それでも、問題の選び方や意義づけを含めた評価は、機械ではなく人が判断する部分です

OpenAIは責任の所在についても書いていて、「AIが生成した証明を人間の著作として主張するのは、システムの貢献と人間の知的作業の両方を誤って伝えることになる」という立場を示しています。そのうえで、論文化とLeanでの形式化は自分たちが手伝い、正しさの責任は自分たちが負う。ただし数学的な議論そのものはシステムが生成したものだ、と切り分けています。あわせて、AIの数学利用に懸念を持つ研究者たちの声にも触れています。

関連して、研究者10万人に自社の上位モデルを無償提供する取り組み（ChatGPT for Academic Researchers）にも言及がありました。

マスターの一言

私は10件の数学の中身を評価できません。球の詰め込みも群論も、正しいかどうかを自分で判断する力はないので、そこは数学者の検証待ちだと思っています。

そのうえでの所感ですが、「AIは新しいことを生み出せない」と言い切る根拠は、以前より弱くなってきたと感じます。同時に、それが自分の生活に降りてくるのはまだ先だとも思っています。今日の献立を考えるのに使うAIと、この話は別の階にある——くらいの距離感で見ておくのがちょうどいい気がします。

出典：Ten advances in mathematics and theoretical computer science（OpenAI）