最も包括的な大規模モデルデータセット共有：パート1、数学データセット

現在、大規模モデルは数学の分野でまだ大幅な改善の余地があり、その数学的能力をトレーニングするための基盤は、高品質の数学データセットにあります。以下に、オープンソースの数学データセットをいくつか紹介します。

GSM8K

https://huggingface.co/datasets/openai/gsm8k

GSM8Kデータセットは、大規模モデルの数学的能力を評価するための一般的なベンチマークの1つです。GSM8Kデータセットは、8.5Kの高品質で言語的に多様な小中学校の数学の文章問題で構成されています。その主な特徴は、多数の問題を提供し、各問題に自然言語の解答が付随していることです。このデータセットの主な用途は、現在のモデルの推論の欠陥の診断をサポートし、関連する研究の進歩を促進することです。GSM8Kを通じて、研究者は、特に複雑な推論を必要とするシナリオにおいて、多段階の数学的推論タスクにおけるモデルのパフォーマンスをテストおよび改善できます。GSM8Kは、モデルのパフォーマンスを評価および向上させるための効果的なベンチマークとして機能します。

MATH

https://github.com/hendrycks/math

MATHデータセットは、代数、幾何学、確率、数論など、数学のさまざまな分野をカバーする12,500の複雑な数学コンテスト問題で構成されています。このデータセットの注目すべき特徴は、各問題に詳細な段階的な解答が付いていることです。これにより、機械学習モデルが正解を見つける能力をテストするだけでなく、論理的な推論と問題解決プロセスを生成する能力を評価することもできます。問題の難易度が数学コンテストの難易度と一致しているため、このデータセットは非常に挑戦的であり、高度な数学的問題解決技術を進歩させ、検証するのに適しています。さらに、データセットの段階的な解答は、自動評価とモデルトレーニングのための豊富なリソースを提供し、数学分野における機械学習アルゴリズムのさらなる発展に貢献します。

Orca-Math-200K

https://huggingface.co/datasets/microsoft/orca-math-word-problems-200k

Orca-Math-200Kデータセットは、20万の数学の文章問題を含む大規模な合成数学問題集です。このデータセットは、主に数学の問題を解く言語モデルの能力をトレーニングおよび評価するために使用されます。モデルの推論と問題解決スキルに挑戦し、向上させるために、簡単なものから難しいものまで、さまざまな数学の問題を提供します。データセットの生成プロセスには、最初のシード問題の収集と、共同エージェントを使用した新しい問題の言い換えと作成が含まれ、それによって問題セットの多様性と難易度が豊かになります。このプロセスは、データセットの品質を向上させるだけでなく、モデルトレーニングの可能性と柔軟性を高め、データの鮮度と多様性を確保しながら、数学分野におけるモデルのパフォーマンスを効果的に向上させるのに役立ちます。

NaturalProofs

https://github.com/wellecks/naturalproofs

NaturalProofsは、基本的な計算や応用問題から、より抽象的で理論的な数学的証明へと移行します。NaturalProofsは、32kの定理のステートメントと証明、14kの定義、および2kのその他の種類のページ（公理、系など）で構成される大規模な形式的数学的証明データセットです。これらのページは、貢献者のコミュニティによって書かれた数学的証明のオンラインコンピレーションであるProofWiki、Webベースの代数および幾何学の教科書であるStacks Project、および数学の教科書からのデータの3つのドメインから供給されています。NaturalProofsの出現は、高度な数学的推論と証明生成における人工知能の能力を研究するための貴重なリソースを提供します。大規模モデルの論理的推論能力に挑戦するだけでなく、人間が読める数学的証明を理解し生成する能力もテストします。このデータセットの規模と品質は、高度な数学における大規模モデルのパフォーマンスを評価および改善するための重要なベンチマークとなります。

LeanDojo

https://github.com/lean-dojo/LeanDojo

LeanDojoは、学習ベースの定理証明器専用に設計されたリソースであり、Leanプログラミング言語の数学ライブラリから大量のトレーニングデータを抽出します。このデータセットには、98,734の定理とその証明、および130,262の前提の定義が含まれており、定理証明の分野で最大のデータセットの1つとなっています。定理証明は、形式数学および検証における機械学習の中心的なタスクであり、LeanDojoデータセットは、自動定理証明システムのトレーニングと評価のための豊富なリソースを提供するために構築されています。

LeanDojoデータセットの構築プロセスでは、プログラム分析技術を採用してデータの品質と関連性を確保しており、特に定理証明における重要なボトルネックである前提選択において重要です。細かく注釈付けされた証明の前提を提供することで、データセットは前提選択のトレーニングと評価をサポートします。さらに、LeanDojoデータセットは、「novel_premises split」と呼ばれる新しい分割戦略を導入しており、テストセットの証明がトレーニングセットで見たことのない前提を少なくとも1つ使用する必要があることを要求します。これにより、モデルがトレーニングデータを記憶することに過度に依存するのを防ぎ、汎化能力を高めるのに役立ちます。

LeanDojoは単なるデータセットではなく、大規模言語モデル（LLM）支援の定理証明に関する学術コミュニティの研究を促進するためのツール、モデル、ベンチマークのスイートを提供する完全なオープンソースプラットフォームです。コードとモデルをオープンソース化することで、LeanDojoは定理証明における機械学習研究への参入障壁を下げ、再現可能なベンチマークと将来の研究のための強力な基盤を提供することを目指しています。

NuminaMath

https://huggingface.co/datasets/AI-MO/NuminaMath-CoT

NuminaMathデータセットは、さまざまな数学コンテスト、フォーラム、教育リソースから86万の問題と解答のペアを集約し、数学分野における人工知能の能力を向上させる画期的な取り組みです。このデータセットの構築プロセスには、MATH、GSM8K、AMC、AIMEなどの幅広いソースと、OCR、翻訳、洗練、思考の連鎖（CoT）フォーマットなどの技術の応用が含まれます。NuminaMathデータセットは大規模であるだけでなく、綿密に設計されたCoTフォーマットを通じて思考の連鎖推論をサポートしており、これは大規模言語モデル（GPT-4など）が複雑な数学の問題を解決するためにトレーニングする上で不可欠です。このデータセットの成功した応用は、AIMOプログレス賞を受賞したモデルの微調整で明らかであり、AIの数学的推論能力を向上させる効果を示しています。NuminaMathデータセットの作成と利用は、数学教育と技術的課題における人工知能の大きな前進を示しています。

DART-Math

https://github.com/hkust-nlp/dart-math

DART-Mathデータセットは、大規模言語モデルの数学的問題解決能力を向上させるために特別に設計された合成データセットです。難易度を考慮した拒否チューニング（DART）法を使用して生成されており、困難な問題により多くの生成試行を割り当てることで、困難な数学の問題に対するトレーニングサンプルをより多く確保しています。DART-Mathデータセットには約59万の例が含まれており、これは以前のデータセットよりも少ないですが、その設計と生成戦略により、モデルが困難な問題を処理する能力が大幅に向上します。このデータセットは、GPT-4のような大規模な独自モデルに頼ることなく、7BパラメータのオープンソースモデルDeepSeekMath-7B-RLのみを使用して作成されました。7Bから70Bパラメータの範囲のベースモデルを微調整することで、DART-Mathという名前の一連のモデルが作成されました。これらのモデルは、MATHやGSM8Kを含む6つの数学ベンチマークで、従来のリジェクションファインチューニング法を大幅に上回り、一部のテストでは、より小さなデータセットと非独自モデルを使用しているにもかかわらず、最先端の技術を上回っています。したがって、DART-Mathデータセットは、数学的問題解決能力を向上させるための非常に効果的で費用対効果の高い公開リソースであることが証明されています。

DeepSeekMath

DeepSeekMathはデータセットをオープンソース化していませんが、高品質な数学データセットを生成するための道筋を提供しています。

DeepSeekMathデータセット生成プロセス

• データソース: データセットの構築は、毎月更新されるWebページのコピーを含むデータセットであるCommon Crawlプロジェクトから始まります。この広大なデータソースを活用することで、数学関連の潜在的なコンテンツを大量に抽出できます。
• 初期スクリーニングプロセス: 数学関連のコンテンツをフィルタリングするために、研究チームはまずOpenWebMathからシードデータセットを構築しました。このシードデータセットを使用して、より多くの数学関連のWebページを識別および取得するためのfastTextモデルをトレーニングしました。\
• 分類とフィルタリング: トレーニングされたfastTextモデルをCommon Crawlデータセットに適用してページを分類およびフィルタリングし、数学に関連するページのみを保持しました。このプロセスは、モデルがCommon Crawlからより多くの数学関連コンテンツを継続的に識別できるようにするために、複数回繰り返されました。
• データセットの規模: 数回の反復の後、3,550万の数学関連のWebページが収集され、合計で1,200億の数学関連のトークンが含まれていました。この膨大なデータセットは、言語モデルのさらなるトレーニングのための生データとして機能します。
• 重複排除とスクリーニング: データ品質を確保するために、生データは重複排除を受けました。さらに、トレーニングデータがテストセットまたは検証セットで汚染されるのを避けるために、評価ベンチマークに一致するページは除外されました。
• 反復的な最適化: データセットの構築プロセス全体を通じて、研究チームはデータフィルタリングモデルを継続的に反復および最適化し、データセットの多様性、カバレッジ、および品質を確保しました。最終的なDeepSeekMathデータセットは、高い数学的関連性を示し、数学的推論における言語モデルに豊富なトレーニング資料を提供します。

4回の反復の後、3,550万の数学関連のWebページと1,200億の数学関連のトークンを含むコーパスが編集されました。このプロセス中、ベンチマークの汚染を避けるために、評価ベンチマークに一致するWebページは除外されました。さらに、DeepSeekMathデータセットの品質は、MathPile、OpenWebMath、Proof-Pile-2などの他のデータセットとの比較を通じて検証され、高品質、多言語コンテンツカバレッジ、および大規模における利点が示されました。下流の数学的推論タスクのパフォーマンス向上に大きく貢献しています。

AlphaProof

GoogleのDeepMindチームは、AlphaProofに関する技術共有を公開しました。これは、AlphaGeometryとともに、今年のIMO（国際数学オリンピック）から4つの問題を解決し、銀メダルに相当するパフォーマンスを達成しました。

AlphaProof強化学習トレーニングサイクルフローチャート

AlphaProofモデルのトレーニング用データセットの生成プロセスは、事前トレーニング済みのGemini言語モデルを基盤として使用することから始まります。このモデルは、数学の問題の自然言語記述をLean形式言語のステートメントに自動的に変換するように微調整され、それによってさまざまな難易度レベルの形式的な数学的問題の大規模なライブラリが作成されます。次に、AlphaProofシステムはこれらの問題の解決策候補を生成し、Leanで可能な証明ステップを検索してこれらの候補を証明または反証します。発見および検証された各証明は、AlphaProofの言語モデルを強化するために使用され、より困難な問題を解決する能力を高めます。IMOコンテストの数週間前、AlphaProofは、さまざまな難易度と数学のトピックをカバーする数百万の問題を証明または反証することによって広範なトレーニングを受けました。さらに重要なことに、このトレーニングプロセスはコンテスト中も継続され、モデルは完全な解決策が見つかるまで、自己生成されたコンテスト問題のバリアントを証明することによって継続的に強化されました。このプロセスは、自然言語処理、形式的な数学的推論、および強化学習を巧みに組み合わせて、自己改善型の数学的問題解決システムを作成します。