-
o3とFrontierMathの紹介
- o3はOpenAIの新しい言語モデルで、FrontierMathと呼ばれる非公開データセットで25%の点数を記録した。
- FrontierMathはEpoch AIが発表した難しい数学問題で構成される非公開データセットである。
- データセットには「この数字を見つけろ!」のような問題が含まれ、自動で検証可能な明確な回答を要求する。
-
FrontierMathデータセットの難易度
- FrontierMathの問題は研究数学者にとっても非典型的で、一部は博士課程レベルの知識を必要とする。
- データセットの問題は数学的な証明よりも、数字を見つけることに重点を置いている。
- 数学研究者は主に証明やアイデアを見つけることに時間を使うため、FrontierMathはAI数学研究において重要なデータセットである。
-
AIの数学的能力
- AIは現在、高校レベルの数学問題をうまく解決しており、まもなく大学数学の試験も合格できると見込まれている。
- しかし、高度な学部上級以上の革新的なアイデアを生み出すことは依然として挑戦的だ。
- o3が25%の点数を記録したことは驚くべきだが、一部の問題は大学生レベルだという主張もある。
-
数学研究におけるAIの役割
- 数学研究で重要なのは「この定理を証明せよ!」といった問題を解決することである。
- DeepMindのAlphaProofは2024年の国際数学オリンピックの問題のうち4問を解き、いくつかは完全なLean証明で検証された。
- AIが数学研究でより大きな役割を果たすには、人間が理解できる形で証明を説明できる必要がある。
-
将来の展望
- AIが数学研究でより大きな役割を果たすためには、人間が理解できる形で証明を説明できる必要がある。
- AIの発展は速いが、なお道のりは長い。
- AIが学部レベルの壁を越える時期は依然として不確実である。
1件のコメント
Hacker News の意見
Reddit のスレッドでは、3 つの難易度ランクのうち 25% が T1(最も易しい)で、50% が T2 でした。著者が確認した5つの公開問題のうち2つは T1、2つは T2 でした。Glazer は T1 を「IMO/学部レベルの問題」と説明しましたが、記事の執筆者はそれを学部レベル問題とは見なしません。LLM はすでに、著者が驚くだろうと思っていたことを実際に行っています
ChatGPTを使って線形代数を理解しようとしましたが、実際の数学ではしばしば馬鹿げた誤りをします。たとえば、ベクトルの次元を超えてインデックスを参照したり、スカラーに対して行列分解を試みたり、次元が一致しない行列を掛けようとしたりします
O1 は 4o よりも誤りを見つけるのが得意ですが、なお、愚かな誤りを多くしています。一定の知識を持つ人が助けないと、一貫した結果を生成し続けるのは難しいでしょう
Akshay Venkatesh の講演で、理論証明の自動化がさらに一般化する場合の「数学者」の未来について議論しました。自動推論の発展によって研究数学の概念化と遂行方法がどのように変わるかに触れています
18歳の息子が数学を勉強したいと望む親として、自動化により職業が消えるのではないかと心配しています。しかし、LLMが完全に代替できるかは疑問です。LLMはすべて解決するための無限の時間・リソースを持っていないため、人間の役割はまだ残るだろうと考えています
LLMがほとんど全ての問題を解く問題セットを作れるかは分かりませんが、AI が人間のような独立した意味での社会的合理性を発達させるまで、推論可能な汎用的な問題解決者になるとは思いません
ChatGPTが基本的な誤りを犯した例を示しました。たとえば、Stop-and-Wait ARQ の効率の公式を導く際に誤ったステップを説明しました。別の例として、練習できる三段論法を要求したところ、整合性のない三段論法を提示しました
FrontierMath データセットが壊れている可能性があると指摘しました。OpenAI が質問を知っているなら、次のバージョンで FrontierMath テストで 80% 以上を達成できるだろうと見込まれます
Quantum 研究と同様の問題に直面しています。伝統的なコンピュータで不可能な計算を実行することでしか進展を示せない状況です。ChatGPT が 25% の点を取ったとき、その25%がトレーニングセットの質問とどれだけ近いかという疑問が提起されます
言語モデルがリーマン仮説の「証明」を提供する可能性が心配です。数学者たちがそれらの証明を検証しようとすれば、かなりの時間を要する可能性があります
IMO 2025 には機械は参加しないでしょう。IMO では「採点者」概念がなく、各国のチームリーダーと審査員の間の交渉で点数が決定されます。AI の仕事を採点するために、何百人もの人がさらに長く滞在することはありません