FrontierMath Erdős を発表する

今年、AIの数学能力の動向を少しでも追っていたなら、エルデシュ問題のことはおそらく耳にしているだろう。AIが解いた最初の未解決の数学問題のいくつかは、エルデシュ問題だった。数学におけるAIの、誰の目にも明らかな最初の「すごい」瞬間も、エルデシュ問題で訪れた。エルデシュ問題は、AIの数学能力を追跡するための中心的なベンチマークのようなものになっているが、その位置づけは比較的非公式なものだ。

私たちの新しい数学ベンチマーク FrontierMath Erdős は、エルデシュ問題を使ってAIの数学能力を測ることに、ある程度の厳密さを持ち込むことを目指している。

エルデシュ問題とは何か

この言葉は、多作な数学者 Paul Erdős（1913-1996）が提起したあらゆる問題を指すようになった。特定の数学者と強く結びついた数学の問題の多くは「誰それが提起した問題」と呼ばれるが、エルデシュは何百もの問題を提起した点で異例だった。2023年、数学者の Thomas Bloom は、エルデシュがこれまでに提起したすべての問題を目録にする取り組みを始め、そのためにウェブサイト erdosproblems.com を作った。Bloom のサイトには現在1217問が収録されており、そのうち652問が未解決である。これらの問題は、早くも2025年初めにはAIシステムの試金石になりうると認識されており、2025年末までにそうした取り組みは劇的に増えていた。

選定、検証、再現性という課題への対応

このベンチマークは、主に三つの課題に取り組む。

選定：エルデシュ問題は数学的な重要性も難しさも大きくばらつく

「エルデシュ問題」という名前は、「ミレニアム懸賞問題」のように均質なものを思わせるが、実際はそうではない。エルデシュ問題の多くは数学者からさほど注目されず、結局は（人間によるものであれ、AIによるものであれ）ほどほどの労力で簡単に解けることが分かった。一方で、徹底的に研究され、数学の下位分野全体の中心的な問題になったものもある。AIの能力を追跡するには、その違いを知る必要がある。

私たちの貢献は単純だ。Bloom に、未解決のエルデシュ問題のうち、数学的に重要でかつ難しいと彼が考える、お気に入りの問題を選んでもらった。彼が選んだのは68問で、いずれも2026年8月時点で未解決であり、当時の未解決問題の約10%に当たる。Bloom は評価の高い数学者で、エルデシュ問題を熟知しているとはいえ、この方法は極めて主観的である。未解決の数学問題からなる私たちの別のベンチマークの選定に協力してくれた際、Bloom はこう語っていた。

どの数学者も、このリストのいくつかの問題を見て「いったいなぜこれを入れたんだ？」と思うのは間違いない。だが、ほかの問題を見て「これが入るのは当然だ、深くて重要な問題だ」とも思ってくれるなら、私たちはよい仕事をしたことになると思う。

この68問のエルデシュ問題についても同じことが言えるのは確かだが、大まかな分類であっても、これまでの状況に比べれば明らかな改善だと私たちは考えている。Bloom の大まかな見積もりでは、2026年8月時点でAIが解いたこの水準のエルデシュ問題は3〜5問程度であり、したがってこのベンチマークはAIによる解決にかなり高いハードルを課すことになる。

検証：エルデシュ問題の解答は検証が難しい

研究数学では、人間は解答を自然言語の証明として示す。そうした自然言語の証明を検証するのは極めて手間がかかり、AIシステムを大規模に評価するうえで課題となる。目立った方法の一つは、数学の証明を表現するための専用のプログラミング言語である Lean を使うことだ。Lean で書かれた証明はどれも、正しさをプログラムで確認できる。問題文が正しく形式化されている限り、Lean の検査を通ったAIの解答はどれも健全だと確信できる。¹

この点での私たちの貢献は小さく、主に既存の二つのプロジェクトに基づいている。一つ目は Google の Formal Conjectures プロジェクトで、Lean で形式化された数学の予想を集めたものである。私たちが収録した68問のうち50問は、このプロジェクトの一部としてすでに形式化されている。残る18問はAIに形式化させた。この18問の命題はかなり単純で、形式化はこれまでのところ私たちの最初の確認を通っている。それでも私たちは Lean の専門家ではないので、誤りがあるかもしれない。現在、専門家による追加の確認を求めているところだ。二つ目は Comparator で、Lean を開発する組織 Lean FRO が作った証明検査器である。積極的に不正をしようとする提出物に対しても頑健であるよう設計されている。

再現性：AIにエルデシュ問題を解かせる方法は不透明だった

AIにエルデシュ問題を解かせようとした人はどれだけいるのか。どの問題に挑んだのか。どのAIモデルを使ったのか。どんなスキャフォールド（モデルを動かす周辺の仕組み）で。推論実行の計算資源にどれだけ費やしたのか。愛好家であれ数学者であれ、誰でもこれらの問題に挑戦できるので、網羅的な答えは期待できない。しかしこれまでのところ、最も目覚ましい結果はAI企業の内部から出てきており、そうした企業は、結果を得た実験についてあまり明らかにしていない。

私たちの貢献は透明性である。これらの問いに明確に答える。ベンチマークを実行するためのコード一式はこちらでオープンソースとして公開しており、主要な実行環境はこちら、68問の一覧はこちらとこちらにある。標準では、各AIシステムを1問あたり300ドルの推論実行予算で実行する。これまでに実行した具体的なモデルについては、以下で報告する。

注意点

FrontierMath Erdős の三つの限界を挙げておく。

形式化はAIシステムに追加の負担を課す

重要な数学の研究課題で突破口を開くことは、それだけでも十分に難しい注文である。そうした結果を形式化するのは、事実上まったく別のプロジェクトを付け足すことに等しい。数学で大きな突破口を開けるAIシステムなら、それを形式化することもできると期待したいところだが、それが保証されているわけでは決してない。仮にできるとしても、形式化には膨大な労力がかかるかもしれない。

たとえば、OpenAI のモデルがエルデシュの単位距離予想（Bloom のサイトの問題90）の解決を生み出したとき、自然言語の証明は18ページだったが、その結果を Lean で形式化した後続の取り組みは120万行のコードになった。これは主に、Lean の標準ライブラリでまだ形式化されていなかった「深い」結果を使う必要があったためである。18ページの論文ではこの結果を参照するだけで済んだが、Lean での形式化では第一原理から導かなければならなかった。

これは、AIシステムに未解決問題を解かせる、Lean ベースのあらゆるベンチマークに共通する限界である。

データ汚染はいずれ問題になる

当初、私たちはこのベンチマークを「古典的な」公開ベンチマークとして扱う。つまり、モデルが公開されるたびに実行し、データ汚染に対する強い防御策は設けない。どの問題についても、解答はおそらく公開され議論されるだろうし、場合によっては広く知られることになる。私たちが評価するモデルはインターネットにアクセスできない（代わりに、オフラインの数学論文集と、数式処理システムのようなツールを与える）が、解答はいずれ学習データに入り込む。これがどの程度問題になるかを監視していく予定だ。

現時点では、これは懸念に当たらない。2026年8月時点で、68問のどれについても解答は知られていなかったので、学習データがそれより前で終わっているモデルが解答を学習したはずはない。将来のモデルについては、事後的に汚染を補正できる。あるモデルの学習データの締め切り以前に解かれた問題を除外し、残りの問題ですべてのモデルを比較すればよい。

少なくとも、否定的な結果は依然として有益なはずだ。以前のモデルが解いた問題を後のモデルが解けなければ、それはおそらく、後のモデルの数学能力のほうが劣ることを示唆するデータ点になる。

エルデシュ問題は数学のすべてではない

エルデシュの関心は幅広かったが、数学はそれよりはるかに広い。このベンチマークを、数学の全分野からの標本と受け取るべきではない。このベンチマークでの進歩は、数学能力全般の進歩と少なくともある程度は相関すると予想しているが、この推論は盤石ではない。

最初の結果

これまでに五つのモデルを実行した。GPT-6 Astra の公開前の版、GPT-5.6 Sol、GPT-5.5、Claude Fable 5.1、Claude Fable 5 である。各モデルは各問題に1回ずつ挑戦し、1回の挑戦あたりの予算は300ドル、作業時間は72時間とした。モデルが検証を通る Lean の証明または反証を生成した場合に、その問題を解いたとみなす。

モデル	スコア
GPT-6 Astra	3%
GPT-5.6 Sol	0%
GPT-5.5	0%
Claude Fable 5.1	0%
Claude Fable 5	0%

FrontierMath Erdős のスコア

何かを解いたのは GPT-6 Astra だけで、68問中2問だった。問題74は反例を見つけて反証し、費用は222ドル、作業時間は10時間だった。問題126は証明し、費用は172ドル、作業時間は10時間だった。それ以外の同モデルの挑戦と、ほかの四つのモデルのすべての挑戦は、検証済みの証明に至らないまま予算を使い切った。

追加の挑戦

ベンチマークの実行とは別に、同じ GPT-6 Astra の公開前の版を使い、1回あたりの予算を増やしたり、エージェントの構成を変えたりして、同じ問題にさらに何度か、それほど体系的でない形で挑戦させた。これらの挑戦は FrontierMath Erdős のスコアではない。ベンチマークの固定された手順には従っていない。予算はより大きく、エージェントの構成はまちまちで、問題ごとの挑戦回数も異なる。GPT-6 Astra の FrontierMath Erdős のスコアは、上のベンチマーク実行による3%のままである。それでも追加の挑戦を報告するのは、これらの問題のいずれかの解答は、どのように得られたものであれ数学的に興味深いからであり、また繰り返し挑戦させることで、結果が挑戦ごとにどれだけばらつくかがある程度分かるからである。今後の研究では、この推論実行のスケーリングをより体系的に調べ、1回あたりの予算や挑戦回数に応じて解答の数がどう増えるかを測定できるだろう。

すべての挑戦を通じて、GPT-6 Astra は68問中5問を少なくとも1回は解いた。上の2問に加え、反証した問題1と、証明した問題548と問題571である。残りの問題の大半には合計で2〜6回挑戦させたが（269回）、どれも解けなかった。この五つの解答に至るまでに、すべての挑戦を合わせて22万ドルを超える計算資源を使った。ベンチマーク実行そのものにかかったのはおよそ2万ドルである。

問題	結果	解けた回数	各解答の費用
1	反証	5回中2回	405ドルと1,384ドル
74	反証	7回中7回	47〜271ドル
126	証明	5回中5回	154〜249ドル
548	証明	4回中1回	363ドル
571	証明	4回中1回	617ドル

繰り返しになるが、上の表はベンチマークの結果ではない。FrontierMath Erdős のスコアは最初の表に示したものである。

五つの解答の簡単な要約を含む詳細は、論文にある。今後も新しいモデルが公開されるたびに評価を続け、最新の結果は FrontierMath Erdős のベンチマークページに掲載する。

結論

AIによる最も目覚ましい数学の成果はAI企業内部の取り組みから生まれてきたが、それがどのように得られたのかはほとんど明らかにされてこなかった。FrontierMath Erdős がこの状況を明らかにする助けになることを願っている。最初の実行結果から見て、その役割は果たせていると考えている。このスキャフォールドとこの予算のもとで、Astra は、この重要な未解決数学問題のリストの約3%を解いた。これは、AIによる数学の突破口がどれほど起きているかについての有用なデータ点になる。実際に起きているが、まだかなりまれだということだ。この水準の問題がそもそもAIに解けること自体は注目に値するが、この種の問題を任意に一つ選んだときにAIが解ける見込みが特に高いという段階には、まだ至っていない。少なくとも、1問あたり300ドルの予算内で結果を形式化しなければならない場合はそうである。

この五つの問題に対するAIの解答がどのような性質のものかも、多くのことを教えてくれるだろう。それについては、数学者が結果を消化し、論評するのを待つ必要がある。