5,596 文字
数学のベンチマークを構築するためにEpoch AIがこれほど多くの労力を注いでいる理由はいくつかあります。その一つは、数学が完全に客観的な学問分野だということです。私たちが作成している問題のすべてには、一意的な、あるいは客観的に検証可能な答えがあり、自動的に検証することができます。
AIの数学的推論能力が重要である理由については、特に私の見解では、AIの発展における大きなボトルネックの一つが、一貫した世界観や真実の概念を構築し、真実に関する長い連続的な推論を行う能力だからです。
そのため、私たちはAIの数学問題を解く能力が、このような問題における推論能力、さらには現実世界というはるかに一般的な文脈における推論能力の良い代理指標になると考えています。現在の多くのLLMモデルにおけるボトルネックは、彼らが言うことを導き出すためにアドホックなパターンマッチングを多用していることです。
しかし、これは信念や真実の概念を実際に持つこととは非常に異なります。私は、私たちが作成した問題、特に上位レベルの問題は、現在のLLMを単に拡大することによって解決されるとは思いません。このベンチマークを克服する可能性がある種類のパラダイムは、内部の客観的なクライアントにずっと大きく依存するものだと思います。
Leanのようなフォーマライズされた証明アシスタントか、あるいは人間が数学と客観的に関わる方法の何らかの内部的な類似物かもしれません。そして彼らがそのようなクライアントストアを持つと、彼らはエリートチェスや囲碁モデルを構築するために使用したテクニックを使って、そのシステム内で新しい証明を効率的に探索することができます。
利用可能なデータのみでトレーニングすることによってLLMがこれらの問題を解決できるようにすることには複数の困難があります。一つには、すべての数学の問題は本質的に独自の正確な実体です。AIが研究論文や教科書内の類似のトピックについてトレーニングできたとしても、数学問題の言い回しがわずかに変わるだけで、その問題の根底にある数学が非常に根本的に変わることがあります。
したがって、公開されているデータを見るだけで答えを単に推測することはできないでしょう。数学について公開されている文献に頼るだけのもう一つの問題は、それが数学的経験のほんの一部しかカバーしていないことです。どの数学者も、彼らが取り組んでいる問題を解決するプロセスの中で、たくさんの失敗に遭遇します。
私自身の研究でも、問題に取り組むためのアイデアの95%は行き詰まり、数学者たちはこれらの行き止まりについて、あるいは最終的に解決策に到達するためにどのようにして閃きを得たかについて話すことにあまり熱心ではありません。
実際、私たち多くの人は基本的に自分たちの足跡を隠し、問題に従うために行った重要なステップがまるで魔法のように突然現れるような論文を作り出すことを誇りにしています。数学を適切に行う方法についての実際の教育学は、主に仲間の数学者との会話や大学院での指導教官との対話を通じて習得されます。
したがって、適切な数学者になるという経験の多くは、単にインターネットのテキストでトレーニングするだけではLLMがアクセスできないと思います。私と同僚の現在の見解では、このベンチマークは、少なくとも現在の状態では、約5年持続するだろうということです。とはいえ、私たちはまだ新しい問題を収集しており、今年中も引き続きそうする予定です。また、私たちは積極的に難易度の最も高い範囲にある問題を探しています。私の意見では、データセットが最終決定されるとき、
それは現在持っているものよりもかなり難しくなり、さらに長く持続するでしょう。Frontier Mathベンチマークデータセットの問題は、研究数学の問題と多くの共通点があり、少なくとも以前のベンチマークで使用されてきたようなオリンピアド問題よりもはるかにそうだと思います。
彼らは確かに数学の主要分野すべてをカバーしています。それらに取り組み始めるには、少なくとも研究者レベルの分野の理解が必要です。とはいえ、私たちの最も難しい問題と実際のプロの数学者が直面する最も困難な研究プロジェクトとの間にはまだギャップがあることは確かです。
私たちの最も難しい問題でさえ、最大で1週間の努力で解決されるように設計されていますが、プロの数学者はしばしば一つの数学問題に文字通り何年もかけることがあります。したがって、私たちの最も難しい問題を解決するAIはプロの研究者レベルにかなり近いと思いますが、それらが人間の数学の技術を完全に習得したと本当に言えるようになる前に、乗り越えなければならないギャップはまだ確かにあります。
Frontier Mathベンチマークの問題と典型的な研究数学の問題を区別するもう一つのことは、事実上すべての研究数学が証明ベースであるということです。それはコミュニティ内で提起されたさまざまな予想、または私たち自身の研究アジェンダを進めるために考え出した問題に対する証明を考え出すことについてです。
一方、私たちのベンチマークでは、すべての問題が閉形式の解答を持っています。通常は整数、時には整数のペアや象徴的な実数ですが、常に閉形式の解答です。これは数学コンテストでは標準ですが、研究数学では確かに標準ではありません。私が自分の問題を作成するプロセスを経て、または他の数学者と話してこれらの問題を作る過程を説明すると、私たちは皆、証明ベースの
アジェンダをこの非常に制約のある形式に変換しようとするのに相当な苦労をしています。ベンチマークに数学の広い範囲をカバーする数学問題を得ようとすることの難しさは、一部の分野は他の分野よりもこの種の数値形式に適しているということです。数論家、グラフ理論家、または組合せ論者から非常に具体的な整数ベースの問題を考え出してもらうのにあまり困難はありませんでした。
しかし、私自身の分野である集合論のような他の分野では、これらは非常に抽象的な主題であり、私たち自身の研究では、一桁以上の整数に遭遇することはめったにありません。コインの裏側の問題について話しましょう。それは問題を入手した後、どのように検証するかということです。私たちには確かに非常に有能な数学者のレビューチームがあり、私たちは常に問題を検討する資格のある数学者に問題を割り当てようとしています。
そして、レビュアーが「この問題を扱えません、私の分野ではありません、他の誰かに与えてみてください」と言う場合、私たちは常にそれを完全に受け入れる用意があります。しかし、これらの問題を特に難しくレビューするもう一つの問題があります。それは、ほとんどの数学者が互いの研究を見るとき、彼らは研究アジェンダによって明らかにされた大きなアイデアや概念に、細かい部分よりも関心を持つ傾向があるということです。
数学コミュニティでは、ほとんどの論文にはエラーがあるというのは少し公然の秘密です。通常は論文の主要な定理を変えない小さなエラーですが、それでも至る所に散らばった小さなエラーがあります。そしてそれは私たちのコミュニティの数学的装置を本当に崩壊させるわけではありませんが、私たちの問題でそれが起こる時は確かに問題です。
問題が軽微な仮説を欠いていたり、答えを得るのに軽微な計算ミスがあった場合、どうすれば私たちのAIモデルが公式に入力した答えを得る可能性があるでしょうか？したがって、私たちの問題は、数学者がピアレビュープロセスに従事する際に通常与える以上の精査のレベルを必要とします。
これは私たちがまだ克服しようとしている困難ですが、私たちは今、レビュアーに単に賛成か反対かを尋ねる受動的なレビュープロセスから、より積極的なものに切り替えようとしています。そこでは、実際にレビュアーに問題の解決策を与える代わりに、私たちは著者が実際にこの問題を解決するために必要だと言う概念、一般的な枠組みだけを与え始めようとしています。
おそらく問題を解決するテクニックとステップの概要ですが、実際にはレビュアーに解決策を与えるつもりはありません。そして彼らが実際に自分で問題を解決し、著者が与えたのとまったく同じ答えを得た場合、それは彼らが完全に書かれた解決策を見て「はい、それは良い」と言うだけよりも、問題の正確さのはるかに強力な証拠となります。
私たちは難しい問題を得るのが難しいことを発見しました。それはあまり驚くべきことではないはずですが、本当に難しい数学問題を作るには多くの努力が必要です。特に、私たちの著者たちには、彼らの解決策が正しいことを別の専門家に正当化できる完全に書かれた解決策を提供することが要件だからです。
そのため、これには多くの努力が必要であり、また私たちのプロジェクトに貢献する非常に才能のある数学者を探し出す必要があります。このプロジェクトを開発する上での課題の一つは、私たちが受け取る問題の難易度を評価するための合理的なスケールを考え出すことです。現在、私たちは問題の難易度を測定するために3軸のスケールを使用しています。
一つ目は、問題を理解するため、そして問題を解決するために必要な概念を理解するために必要なバックグラウンド知識です。二つ目は、問題を解決するための重要なステップを考え出すために必要な創造性のレベルです。そして三つ目は、問題へのアプローチを理解した後、正確に答えを出すために必要な計算労力の量です。
私たちはこれが問題の難易度を分解するためのかなり良いシステムであることがわかりましたが、それでもある程度主観的であるという問題があり、私たちの内部レビュアーが問題の評価に関して互いに意見が一致しないことがわかりました。そのため、私たちは現在、より良い正規化されたシステムを考案して、これらの問題にかなり標準的な評価を割り当てることができるように取り組んでいます。
そして、そのシステムを解決したら、次のステップは、これらの評価をAIモデルがこの問題を解決できるようになるまでの時間に関する予測に、少なくとも相対的なスケールで変換する方法を理解することです。AIモデルが数学的推論をどれくらい速く改善するかについての良い予測がなくても、少なくとも各問題がどれくらい持続すると予想されるか、どの問題がAIモデルに最後まで残るかについての相対的なランキングを持ちたいと思います。
Frontier Mathプロジェクトが当初の構想から進化した大きな方法の一つは、難易度の高い範囲へのますます増加する重点です。プロジェクトの元のバージョンでは、かなり広い範囲の難易度をカバーする問題を作る予定でしたが、AIモデルが改善している速度と、それぞれの後続モデルが前のモデルをどれだけ改善したかを見ると、私たちが当初考えていたスケールの下位部分はかなり速く解決されるだろうとすぐに理解しました。
私たちは、製品がリリースされて数ヶ月以内に、もしくは製品が完成する前であっても、ベンチマークの大部分が飽和してしまうという状況を望んでいませんでした。そのため、それ以来、より難易度の高い部分に焦点を当ててきました。ほとんどの場合、私たちは現在、少なくとも1年、理想的にはそれ以上持続すると思われる問題のみを受け入れています。
そして、プロジェクトの終わりに近づくにつれて、現時点での私たちのリソースのほとんどは、スケールの上位にある問題を提供できると信じる著者や数学者を募集することに向けられています。今から5年、あるいはさらに長く持続すると感じる問題です。このプロジェクトには、数学者として私にとって特に興味深いことがいくつかあります。
私は集合論者であり、私の研究のほとんどはメタ数学の分野にあります。私は単一の形式的な数学システム内だけでなく、多くのシステムを見て、あるシステムでの問題の証明と別のシステムでの問題の証明がどのようなものかを比較し、また、様々なシステムにおける証明の難しさや長さがどうなるかを研究しています。
そして、数学と人工知能の関係を理解しようとすることについての興味深い点の一つは、ある意味で、これが数学的難しさがどこから来るのかについてより客観的な感覚を与えてくれることです。正確に定義された機械が問題を解決するのにどれくらい時間がかかるかを見ることは、人間の数学的推論のより主観的な性質と比較することができます。
このプロダクトが進化するにつれて、数学的難しさの性質自体への洞察を得ることに興奮してきました。そして、このプロジェクトについて私が楽しんでいるもう一つのこと、実は最初は楽しむとは思っていなかったことですが、これらの答えの純粋に数値的な形式から来るすべての制約です。
数学コンテストでは、長い形式の証明を考え出すのではなく、問題に単純な単一の答えがあるのが標準です。私と私の同僚のほとんどは、この形式の数学を軽視する傾向があります。私はそれには爽やかな正直さがあることに気づき始めています。なぜなら、具体的な質問に具体的な答えを出すことによって、単に数学が得意であることを証明することには本当に正直なところがあるからです。数学研究はとても専門化しています。
ほとんどの専門家は、彼らが同じサブサブサブフィールド内にいない限り、同僚が生み出す定理を理解することさえできません。だから、数学者が自分たちの能力の範囲内で最も具体的な問題を考え出し、お互いとマシンの両方にそれらを解決するよう挑戦するこのプロセスを見ることには、何か興奮するものがあります。
コメント