- OpenAIの新しい言語モデル o3 が、難関数学ベンチマーク FrontierMath で25%を記録し、数学AIが学部レベルを超えられるのかという評価が改めて揺さぶられている
- FrontierMathはEpoch AIが作成した非公開データセットで、「定理を証明せよ」ではなく 自動検証可能な数値の答え を求める数百問の難問数学問題で構成されている
- 公開された5つのサンプルは研究数学者にとっても容易ではなく、Taoは「きわめて挑戦的」と評価した一方、Borcherdsは数値の答えを出すことは 独創的な証明 と同じではないと見ている
- Epoch AIのElliot Glazerが、問題の25%は「IMO/学部スタイルの問題」だと述べたことで、o3の25%というスコアが実際にどの難易度まで到達したことを意味するのかは、非公開データセットという性質上確認が難しい
- 数学者にとってより重要な目標は、「この数を見つけよ」よりも 定理を正しく証明し、人間が理解できるように説明すること であり、言語モデルとLeanベースのアプローチにはそれぞれ異なる限界がある
o3とFrontierMathが揺さぶった基準線
- o3 はOpenAIの新しい言語モデルであり、FrontierMathで25%のスコアを記録した
- ChatGPT以降、公開された言語モデルは急速に改善しており、数学問題の解決能力もその流れの中で評価されている
- FrontierMath はEpoch AIが作成した非公開の数学問題データセットで、論文アブストラクトでは「数百」の難しい数学問題があるとされている
- データセットを公開すると、言語モデルが問題と答えを学習してしまうため、問題数のような基本情報ですら慎重に扱われている
- 問題と答えが公開されると、モデルは既に見た答えを再生できてしまう
- このため、非公開ベンチマークの実際の難易度や代表性を外部から検証することは難しい
FrontierMath問題の形式と難易度
- FrontierMathの問題は「この定理を証明せよ」ではなく、「この数を見つけよ」という形式に近い
- 問題は明確で計算可能な答えを持ち、自動検証が可能でなければならない
- 公開された5つのサンプル問題の答えは、すべて正の整数である
- 例としての答えには9811、367707がある
- 残る3つの答えはさらに大きく、無作為な推測では当たりにくいよう設計されている
- 公開サンプルは研究数学者にとっても自明ではない
- 筆者は5問すべての問題文を理解した
- 3問目は比較的早く解け、5問目はWeil conjectures for curvesを使う標準的手法で解く方法は分かったが、13桁の答えまでは計算しなかった
- 1問目と2問目は解けないと判断し、4問目は努力すれば前進できるかもしれないと見たが、試さずに解説を読んだ
- 一般的な優秀な数学専攻の学部生でも、これらの問題は1問も解けない可能性がある
- 1問目は解析的整数論の博士課程レベル以上を要すると見られる
数値解答ベンチマークの利点と限界
- FrontierMathが数値解答問題を採用する主な理由は 採点コスト にある
- 「定理を証明せよ」型の数百件の解答を評価するには人間の専門家が必要になる
- 2024年時点では、このレベルの採点を機械に任せるのは難しいと見られている
- 一方で、数値解答の一覧ならコンピュータが非常に高速に照合できる
- Borcherdsは、研究数学者は時間の大半を数値ではなく 証明とアイデア を見つけることに使っていると考えている
- それでもFrontierMathは数学AI分野で価値がある
- 難しいデータセットが極めて不足している
- こうしたデータセットを作るのは非常に難しいか、費用がかかる
- Friederらの最近の文章は、数学AIデータセットの限界をさらに深く扱っている
o3の25%が驚きだった理由
- 従来の認識では、数学AIは 学部レベルまたはそれ以前 に近かった
- AIは、数学オリンピック型の問題を解く才能ある高校生レベルの課題には非常に強くなっている
- 1年以内にAIが学部数学の試験に合格するのは確実だと見られている
- 学部試験には、授業を基本的に理解した学生が合格できるよう標準的な問題が含まれることがある
- 機械はそのような問題を容易に正答できる
- しかし、標準的なアイデアの再利用を超えて、高度な学部・博士課程初期レベルの革新的なアイデアへ飛躍するのは大きな段差だと見られている
- 最近のPutnam試験に対するChatGPTの解答は期待外れだった
- 機械が適切に答えられていたように見えたのはB4だけだった
- 他の解答の大半は、10点満点で1〜2点程度だと見なされた
- このため、FrontierMathは数年間ほぼ攻略不可能だろうと予想されていた
非公開データセットが残す不確実性
- Epoch AIのElliot GlazerはRedditで、FrontierMathの問題の25%が IMO/学部スタイルの問題 だと述べた
- この発言は、公開された5問の問題とはあまり整合していないように見える
- 公開サンプルで最も易しい問題ですら、Weil conjectures for curvesを使う方法があった
- あるいは、有限体上で次数10^12の三次多項式を因数分解するような、苦痛を伴う総当たりが必要かもしれない
- この情報は、実際の非公開データセットの難易度や、公開された5問が代表的サンプルなのかという疑問を残す
- データセットが非公開であるため、この疑問を簡単に確認することはできない
- 25%が学部レベルの問題なら、o3の25%というスコアはそれほど驚くべきものではないかもしれない
- 期待される大きな突破口は、「qual level」と表現された次の50%の問題でAIが意味のある性能を示す時点である
「定理を証明せよ」は依然として別問題
- 研究数学で重要な問いは、通常「この定理を証明せよ」である
- 数値を見つける問題で超人的性能を示す機械が現れても、多くの研究数学分野では適用可能性が限られるかもしれない
- 2024年最大の成功例としては、DeepMindの AlphaProof が挙げられる
- AlphaProofは2024年IMOの6問中4問を解いた
- 問題は「定理を証明せよ」または「数を見つけ、それが正しいことを証明せよ」というタイプだった
- そのうち3問は、完全に形式化されたLean証明として出力された
- Lean は対話型定理証明支援系であり、mathlib はIMO問題の解決に必要な多くの手法と、それ以上を含む数学ライブラリである
- DeepMindシステムの解答は人間が確認し、「満点」の解答として検証された
- ただし、IMOの問題は非常に難しくても、解法自体は学校レベルの技法しか使わないため、再び高校レベルの問題に戻ったとも言える
- 2025年には、機械がIMO金メダル級の性能を示すだろうと予想されている
機械の答えを誰が採点するのか
- 2025年7月のIMOに、人間の学生だけでなく機械も参加する状況は想像できる
- 機械システムは2つのタイプに分かれうる
- Lean、Rocq、Isabelleのような コンピュータ証明検査系 の言語で解答を提出するシステム
- 人間の言語で解答を提出する言語モデル
- 証明検査系言語で提出された解答は、問題文が正しく翻訳されているかだけ確認すればよい
- その後、証明がコンパイルできれば、実質的に「満点」の解答だと分かる
- 自然言語で解答を提出する言語モデルは事情が異なる
- 解答がもっともらしく見えても、人間の採点者が注意深く読んで評価しなければならない
- 満点の解答である保証はない
- 言語モデルは、論理推論において専門家の人間より少なくとも一桁程度は精度が低いと見られている
- リーマン予想に関する言語モデルの「証明」が、10ページ分の正しい数学の途中に曖昧または不正確な主張を混ぜ込むおそれがある
- 逆に定理証明器は、少なくとも一桁程度は高い精度を持つと見られている
- Leanが人間の数学文献の議論を受け入れなかったとき、筆者が見た事例では人間側が間違っていた
残された目標: 正しい証明と人間の理解
- 数学者が求めているのは単に「定理を証明せよ」ではなく、正確な証明 と人間が理解できる説明である
- 言語モデルのアプローチでは、「正確性」が大きな懸念として残っている
- 定理証明器のアプローチでは、「人間が理解できる形」が懸念となる
- まだやるべきことは非常に多い
- 進歩の速度は速いが、学部の壁 をいつ越えるのかは誰にも分からない
まだコメントはありません。