FrontierMath Erdős｜Epoch AI 日本語版

数学者Paul Erdősが提起または研究した問題のうち、2026年8月時点で未解決で、特に興味深く難しいものを選んだ問題集。

概要

FrontierMath Erdősは、数学者Paul Erdősが提起または研究した68の問題からなる。問題はLeanで定式化されており、AIは完全なLeanの証明または反証を書かなければならない。問題の出典はErdősProblems.comである。このウェブサイトを管理している数学者のThomas Bloomが、特に興味深く難しいと考える68の問題の選定に協力した。これらの問題はすべて、私たちが最初にベンチマークを定式化した2026年8月の時点で未解決だった。Bloomの見積もりでは、この水準のErdős問題のうち、それまでにAIが解いたものは3〜5問にすぎない。

詳しくは、発表のブログ記事、論文、またはオープンソースのリポジトリを参照のこと。リポジトリには、各予想のLeanによる記述と評価用のスキャフォールドを収めている。

方法論

方法論の全体は論文に記載している。要点は次のとおりである。

問題の選定。 問題は、Thomas Bloomが自身の管理するerdosproblems.comの問題のうち、2026年8月時点で未解決だったものから選んだ。未解決のまま残っているErdős問題のうち、見たところ最も難しく興味深いものを代表するように選んでいる。必要条件として、どの問題についても、その解決（肯定的なものでも否定的なものでも）を人間が成し遂げたなら、一流の学術誌に載る論文に値し、関連分野の多くの人々の関心を集めるものであることを求めた。また、問題どうしが独立になるように選んだ。つまり、どれか1問を（肯定的にであれ否定的にであれ）解いても、ほかの問題がただちに解けることにはならないようにしている。

Leanによる記述。 各予想は、Lean 4とその数学ライブラリMathlibを使った命題として記述されている。ベンチマークの68の予想は、erdosproblems.comの番号で65の異なる問題に対応する。Hadwiger–Nelson問題（#508）は、平面の彩色数の候補値ごとに1つずつ、3つの予想で表されている。また、#713の2つの部分は別々の予想になっている。68の予想のうち50（48問に対応）の記述は、Google DeepMindが管理する、形式化された未解決問題のオープンソースライブラリFormal Conjecturesから取った。残りの17問は、Formal Conjecturesに記述がなかった。これらは自動形式化のパイプラインを使って私たち自身が形式化し、自動形式化した各記述が元の問題を忠実に表していることを、Bloomが確認して検証した。

証明の検証。 モデルが予想を解決したとみなすのは、その予想またはその否定の証明を提出し、それが検証を通過したときである。提出を受け入れるのは、Leanを開発する組織であるLean FROが管理する証明検査器Comparatorを通過した場合に限る。Comparatorは、私たちが信頼する予想のLeanによる記述と、信頼されていない提出物を受け取り、それぞれを隔離されたサンドボックスでコンパイルする。そして、提出物が許可された公理だけを使い、Leanのカーネルで再検査できる証明によって、まったく同じ命題を証明している場合にだけ受け入れる。各試行は2つのDockerコンテナに分けて行い、どちらもネットワークにアクセスできない。1つはエージェントコンテナで、モデルはここで証明に取り組み、シェルを完全に使える。もう1つはcomparatorコンテナで、手を加えていないLeanのツールチェーンを置き、ここでComparatorが提出物を検査する。信頼に依拠する部分として残るのは、Leanのカーネル、Comparator自体、そのサンドボックスである。

AIエージェント。 私たちのエージェントは、Inspect評価フレームワークのdeepagentをもとに作っている。モデルにはbash、テキストエディター、残り時間とトークン予算を知らせるツールが与えられ、deepagentがサブエージェントへの委任、永続的なメモリ、ToDoリストのツールを加える。エージェントコンテナには、Mathlibを含むLean 4のツールチェーン、数式処理システムのSageMath、sympy・mpmath・numpy・pantographを備えたPythonがある。コンテナはネットワークにアクセスできないので、数学文献のオフラインのスナップショットを用意している。2022年までの純粋数学のarXiv論文47万6,000本のLaTeXソース一式である。

エージェントは各問題に1回だけ挑戦する。挑戦の間、エージェントは予想を解決するか、2つの上限、すなわち支出300ドルと作業時間72時間のどちらかに達するまで、試行を繰り返す。正答率は68の予想のうち解決したものの割合で、エラーバーは±1標準誤差である。支出は各モデルの標準のAPI価格で計る。評価の時点で価格が公表されていなかったモデルについては、事後に実際の価格で各試行のコストを計算し直し、その価格で解決のコストが300ドル以下だった場合に限って、予算内で解決したと数える（詳しくは論文を参照）。

データの汚染。 予想は、AIシステムによってであれ人間の数学者によってであれ、いったん解決されると、その証明が将来のモデルの事前学習データに入る可能性がある。2026年8月時点で68の予想のいずれにも証明は知られていなかったので、学習データの締め切りがそれより前のモデルが証明を学習したことはありえない。将来のモデルについては、そのモデルの学習データの締め切りより前に解決された予想を除外し、残った小さな集合ですべてのモデルを比較できる。