8/2のセバスチャン・ブベックさんのポスト、この方はもともとMicrosoftにいて、GPT-4が出た時に有名な報告書を出して、今はOpenAIの中にいるのですが、その人がGPT-5-Proを使って数学の新しい証明、ちゃんと意味のある証明ができた、というようなことをツイートして、話題になっているので紹介します。

◆証明された問題と成果

これはどういう問題かというと、基本的にはよくある最適化問題で「バウンドを出してください（この最適化手法でアップデートしていったら、どれぐらいの性能が出ますか）」というような、理論的な証明をする問題の1つ。

この中で、機械学習における基本的な重要な問題に関して、今年の3月ぐらいに論文が出ていました。

この論文を丸ごと読み込ませて、「これに対して、もっと改善できないか」と指示したら、実際、改善した結果を20分ぐらいで出してきて、ブベック氏がそれを確認したところあっていたと。なので、実際に改善できたというようなことを言っています。

証明自体は、難しそうには見えますが、最適化をやっている人からすると「まあ、こんなもんだよね」というような感じなのですが、元の論文を書いた人たちももちろんすごい人たちだと思うので、その人たちがちゃんと考えた方法と比べて「それを改善するようなものを出すことができました」ということです。

もともと言われていたような「LLMを使って色々な重要な科学の分野が前進しますよ」、その1つの目標として、「数学の証明で、新しい、まだ人が出していないようなものを出す」ことができるんじゃないかと言われていたところで、ちゃんと意味のあることが今回出たのかなとは思います。

ちなみに、この直後に人間も頑張ってすぐにこれをさらに改善して、これより良いものを出しているので、まだ人間が負けたというような話ではないです。

なので、AIが出した証明が必ずしも一番最適ではないし、まだまだ伸びしろがあるような方法です。少なくとも、こういう自明ではないが役に立つような証明を「考えてください」と言って、20分ぐらいで出して、それが正しくて、元のものよりかなり改善したものを出した、というようなことが報告されています。

◆AIによる「証明のゴールドラッシュ」

私が思ったのは、これはGPT-5-Proの成果で、このLLMは確かにすごいのですが、そういう短期的な話ではなく、今後こういうことが増えてきた時にどうなるかですね。

例えば、今世の中にあるたくさんの問題、まだ解けていないものも無数にあるので、それを網羅的に証明させてみて、その中からザクザクと、まだ改善できるものを改善するみたいなことが出てくるのかなと。

一種のゴールドラッシュじゃないですけど、いくらでもやりたい放題でやれる時期が1年ぐらい来るのかな、と思います。