パラメータとパフォーマンスがGoogle Minervaのほぼ半分に近づき、新たな数学モデルがオープンソース化されました。

現在、さまざまなテキスト混合でトレーニングされた言語モデルは、非常に一般的な言語理解および生成機能を示し、さまざまなアプリケーションの基本モデルとして使用できます。オープンエンドの会話やコマンド追跡などのアプリケーションでは、自然なテキスト分布全体にわたってバランスの取れたパフォーマンスが求められるため、汎用モデルが好まれます。

ただし、特定のドメイン (医療、金融、科学など) 内でパフォーマンスを最大化したい場合は、ドメイン固有の言語モデルによって、特定の計算コストで優れた機能を提供したり、より低い計算コストで特定のレベルの機能を提供したりすることができます。

プリンストン大学、EleutherAIなどの研究者らは、数学の問題を解決するためにドメイン固有言語モデルをトレーニングしました。彼らは、第一に、数学の問題を解くには大量の専門的な事前知識とのパターンマッチングが必要であり、したがってドメイン適応トレーニングには理想的な環境である、第二に、数学的推論自体が AI の中核タスクである、最後に、強力な数学的推論が可能な言語モデルは、報酬モデリング、推論強化学習、アルゴリズム推論など、多くの研究テーマの上流にある、と考えています。

そこで彼らは、Proof-Pile-2を継続的に事前学習することで、言語モデルを数学に適応させる手法を提案した。 Proof-Pile-2 は数学関連のテキストとコードの組み合わせです。この方法を Code Llama に適用すると、数学的機能が大幅に向上した LLEMMA:7B および 34B の基本言語モデルを取得できます。

論文アドレス: https://arxiv.org/pdf/2310.10631.pdf

プロジェクトアドレス: https://github.com/EleutherAI/math-lm

LLEMMA 7B の 4 ショット Math パフォーマンスは Google Minerva 8B をはるかに上回り、LLEMMA 34B のパフォーマンスはパラメーター数がほぼ半分である Minerva 62B のパフォーマンスに近いものとなっています。

具体的には、この論文の貢献は次のとおりです。

• 1. 数学に特化した LLEMMA モデル (7B および 34B 言語モデル) をトレーニングしてリリースしました。 LLEMMA モデルは、MATH で公開されている最先端の基本モデルです。
• 2. 数学に特化した 11B コード トークンを含むデータセット AlgebraicStack をリリースしました。
• 3. LLEMMA は、計算ツール、つまり Python インタープリタと形式定理証明器を使用して数学の問題を解決できることを実証します。
• 4. これまでの数学的言語モデル（Minerva など）とは異なり、LLEMMA モデルはオープンエンドです。研究者たちはトレーニングデータとコードをオープンソース化した。これにより、LLEMMA は数学的推論の将来の研究のためのプラットフォームとなります。

方法の概要

LLEMMA は、数学に特化した 70B および 34B 言語モデルです。これは、Proof-Pile-2 でコード Llama の事前トレーニングを継続することによって取得されます。

データ: 証拠資料-2

研究者らは、科学論文、数学を含むウェブデータ、数学コードをトークン化した55Bの混合物であるProof-Pile-2を作成した。 Lean proofsteps サブセットを除き、Proof-Pile-2 の知識カットオフは 2023 年 4 月です。

数値シミュレーション、コンピュータ代数システム、形式定理証明器などの計算ツールは、数学者にとってますます重要になっています。そこで研究者らは、数値数学、記号数学、形式数学を網羅した 17 言語のソースコードの 110 億トークンのデータセットである AlgebraicStack を作成しました。データセットは、Stack、GitHub パブリック リポジトリからのフィルタリングされたコード、および正式な証明ステップ データで構成されています。表 9 は、AlgebraicStack における各言語のトークンの数を示しています。

AlgebraicStack 内の各言語のトークンの数。

研究者らは、数学的なコンテンツがフィルタリングされた高品質のウェブページで構成される 150 億トークンのデータセットである OpenWebMath を使用しました。 OpenWebMath は、数学関連のキーワードと分類子ベースの数学スコアに基づいて CommonCrawl Web ページをフィルタリングし、数学形式 (LATEX、AsciiMath など) を保持し、追加の品質フィルター (複雑性、ドメイン、長さなど) とほぼ重複したものを含めます。

さらに、研究者らは、LLaMA トレーニング データセットのオープン複製である RedPajama の ArXiv サブセットを使用しました。 ArXiv サブセットには 290 億のチャンクが含まれています。トレーニング混合データは、正規化の役割を果たす少量の一般ドメインデータで構成されます。 LLaMA 2 の事前トレーニング データセットはまだ公開されていないため、研究者は代替のトレーニング データセットとして Pile を使用しました。

モデルとトレーニング

各モデルは Code Llama から初期化され、Code Llama は Llama 2 から初期化され、デコーダーのみのトランスフォーマー構造を使用して 500B コード トークンでトレーニングされます。研究者らは、標準的な自己回帰言語モデリング目標を使用して、Proof-Pile-2 上で Code Llama モデルのトレーニングを継続しました。ここで、LLEMMA 7B モデルには 200B トークンがあり、LLEMMA 34B モデルには 50B トークンがあります。

研究者らは、GPT-NeoX ライブラリを使用して、bfloat16 混合精度の 256 個の A100 40GB GPU 上で上記 2 つのモデルをトレーニングしました。彼らは、LLEMMA-7B ではワールド サイズ 2、34B ではワールド サイズ 8 のテンソル並列処理と、データ並列レプリカ全体での ZeRO ステージ 1 シャーディング オプティマイザー状態を使用しました。 Flash Attention 2 は、スループットを向上させ、メモリ要件をさらに削減するためにも使用されます。

LLEMMA 7B は、グローバル バッチ サイズ 400 万トークン、コンテキスト長 4,096 トークンで 42,000 ステップトレーニングされました。これは 23,000 A100 時間に相当します。学習率は500ステップ後に1.10^−4まで上昇し、その後48,000ステップ後にはコサインが最大学習率の1/30まで減少しました。

LLEMMA 34B は、同じグローバル バッチ サイズ 400 万トークン、コンテキスト長 4,096 で、12,000 ステップにわたってトレーニングされました。これは 47,000 A100 時間に相当します。学習率は 500 ステップ後に 5.10^−5 まで上昇し、その後ピーク学習率の 1/30 まで低下します。

評価結果

実験部分では、研究者らは LLEMMA が数学テキストの基本モデルとして使用できるかどうかを評価することを目指しています。彼らは、数学的タスクの教師ありサンプルで微調整されていない SOTA モデルに主に焦点を当て、少数ショット評価を使用して LLEMMA モデルを比較しました。

研究者らはまず連鎖推論法と多数決法を用いて、LLEMMA の数学問題を解く能力を評価した。評価ベンチマークには MATH と GSM8k が含まれていた。次に、少数ショットツールと定理証明器の使用について説明します。最後に、メモリとデータの混合の影響について研究します。

Chain of Thought (CoT) を使って数学の問題を解く

これらのタスクは、外部ツールを使用せずに、LATEX または自然言語で表現された質問に対するスタンドアロンのテキスト回答を生成することから構成されます。研究者が使用した評価ベンチマークには、MATH、GSM8k、OCWCourses、SAT、MMLU-STEM などがあります。

結果は表 1 に示されています。Proof-Pile-2 コーパスでの LLEMMA の継続的な事前トレーニングにより、5 つの数学ベンチマークでの少数ショットのパフォーマンスが向上しました。LLEMMA 34B は、GSM8k では Code Llama より 20 パーセントポイント優れており、MATH では Code Llama より 13 パーセントポイント優れています。同時に、LLEMMA 7B は独自の Minerva モデルよりも優れたパフォーマンスを発揮します。

したがって、研究者らは、Proof-Pile-2 での継続的な事前トレーニングが、事前トレーニング済みモデルの数学の問題を解く能力の向上に役立つと結論付けました。

ツールを使って数学の問題を解く

これらのタスクでは、計算ツールを使用して問題を解決します。研究者が使用した評価ベンチマークは、MATH+Python と GSM8k+Python です。

結果を下の表 3 に示します。LLEMMA は両方のタスクで Code Llama よりも優れています。ツールを一緒に使用した後の MATH および GSM8k のパフォーマンスも、ツールを使用しない場合よりも向上します。

形式数学

Proof-Pile-2 の AlgebraicStack データセットには、Lean と Isabelle から抽出された正式な証明を含む、15 億トークンの正式な数学データが含まれています。形式的な数学の包括的な研究は本論文の範囲を超えていますが、次の 2 つのタスクで LLEMMA の少数ショットのパフォーマンスを評価します。

非公式から公式への証明タスク、つまり、正式な命題、非公式の LATEX 命題、および非公式の LATEX 証明が与えられた場合に、正式な証明を生成します。

フォームツーフォーム証明タスクには、一連の証明手順 (または戦略) を生成することによって正式な命題を証明することが含まれます。

結果を下の表 4 に示します。Proof-Pile-2 での LLEMMA の継続的な事前トレーニングにより、2 つの形式定理証明タスクにおける少数ショットのパフォーマンスが向上します。

データブレンディングの影響

言語モデルをトレーニングする場合、混合重みに応じてトレーニング データの高品質なサブセットをアップサンプリングするのが一般的な方法です。研究者たちは、慎重に選ばれたいくつかの混合重量に対して短いトレーニングを実行することによって、混合重量を選択しました。次に、高品質の保留テキストのセット（ここでは MATH トレーニング セットを使用）の困惑を最小化する混合重みを選択します。

以下の表 5 は、arXiv、Web、コードなどのさまざまなデータを混合してトレーニングした後のモデルの MATH トレーニング セットのパープレキシティを示しています。

より詳細な技術的詳細と評価結果については、原著論文を参照してください。