AIと数学 -- 「数学と理論計算機科学における10の進展」
【 AIと数学 -- 「数学と理論計算機科学における10の進展」 】 AIと数学の領域の現状を知るうえで、先日OpenAIが公開した"Ten Advances in Mathematics and Theoretical Computer Science(「数学と理論計算機科学における10の進展」)" という論文(正確にはAIが解いたという10の問題についての10の個別論文を束ねてひとつにまとめたものです)は重要なものです。 Fable 5が登場したときに、彼との対話で彼は面白い表現で証明の二つのタイプを区別していました。一つは、自然言語の上で数学的証明を行う昔からある「手書きの証明」と、もうひとつは、leanやCoqといった形式的証明検証システムを用いた「形式的証明」の区別です。 この区別に従えば、先に上げた10本の論文は、いずれも、昔ながらの数学論文、「手書きの証明」にほかなりません。この10本の論文を読んでも、そこには、表現のレベルでは、さしたる「進展」はありません。 ただ、重要な「進展」があるのです。それは、OpenAIが10個の数学の問題すべてに対するlean上での「形式的証明」を、GitHubで公開したことです。AIと数学の領域では、AIはLLMベースの生成AIから、Neuro+Formal ベースのAIに進化・発展しているのです。この変化は重要です。 興味深いことは、OpenAIは先の文書の公開と同時に、"How the Ideas Came Together(「これらのアイデアがどのようにまとまったか」)" という文書を公開しています。この文書は、いわば、「手書きの証明」と「形式的証明」の「隙間」を埋めるために作られたものだと思います。 この文書を見て僕が感じたことは、AIが自律的に数学の問題の「形式的証明」を完成させたというよりも、数学者がAIを利用して、懸命に(ある意味では賢明に)、形式的証明を完成させたというイメージでした。僕は、それでいいと思います。みなさんは、何を感じましたか? ---------------------------- Ten Advances in Mathematics and Theoretical Computer Science https://cdn.openai.com/...