数学は科学の基礎として、常に研究と革新の重要な分野となってきました。 最近、プリンストン大学と他の 7 つの機関が共同で、Google Minerva 62B に匹敵するパフォーマンスを持つ、数学専用の大規模言語モデル LLEMMA をリリースしました。また、モデル、データセット、コードを公開し、数学研究に前例のない機会とリソースをもたらしました。 論文アドレス: https://arxiv.org/abs/2310.10631 データセットアドレス: https://huggingface.co/datasets/EleutherAI/proof-pile-2 プロジェクトアドレス: https://github.com/EleutherAI/math-lm LLEMMA は Code Llama の基礎を継承し、Proof-Pile-2 で事前トレーニングされています。 Proof-Pile-2 は、科学論文、数学的に豊富な Web ページ、数学コードなど、550 億のトークンに関する情報を含む大規模なハイブリッド データセットです。 このデータセットの一部である Algebraic Stack には、数値、記号、数学の証明を網羅した 17 の言語からの 110 億のデータセットがまとめられています。 7 億と 34 億のパラメータを備え、MATH ベンチマークで非常に優れたパフォーマンスを発揮し、既知のすべてのオープン ソース ベース モデルを上回ります。 Llemma 34B は、Google Research が開発した数学的に閉じたモデルと比較して、パラメータの数が半分で Minerva 62B とほぼ同じパフォーマンスを達成しました。 Llemma は、等パラメータベースで Minerva の問題解決パフォーマンスを上回り、計算ツールを適用して正式な定理証明を実行することで、数学の問題を解決するための無限の可能性を提供します。 Python インタープリターと形式定理証明器を簡単に使用できるため、数学の問題を解決する能力がさらに実証されます。 Algebraic Stack では形式証明データに特に重点が置かれているため、Llemma は少数ショットの定理証明機能を実証する最初のオープンソースの基礎モデルです。 写真 研究者らは、LLEMMA のトレーニング データとコードもすべて公開しました。 LLEMMA は、これまでの数学モデルとは異なり、科学研究コミュニティ全体に門戸を開いたオープンソースで公開共有されたモデルです。 研究者たちはモデル記憶の効果を定量化しようとした。驚いたことに、彼らは、トレーニング セットで提示された問題に対して Llemma の精度が向上しなかったことを発見しました。コードとデータはオープンソースであるため、研究者たちは他の人に分析を再現し拡張することを奨励しています。 トレーニングデータと実験構成LLEMMA は数学に特化した大規模な言語モデルです。Code Llama をベースに構築されており、科学論文、数学コンテンツを含む Web ページ、数学コードを含む 550 億トークンの混合データセットである Proof-Pile-2 で事前トレーニングされています。 コード部分である AlgebraicStack には、数値、記号、形式数学を網羅した 17 言語のソース コードの 11B データ セットが含まれており、オープン ソース化されています。 LLEMMA の各モデルは Code Llama から初期化されます。 Code Llama モデルは、Llama 2 から初期化されたデコーダー専用の言語モデルです。 著者らは、標準的な自己回帰言語モデリング目標を使用して Proof-Pile-2 で Code Llama モデルのトレーニングを継続し、7B モデルを 200B トークンで、34B モデルを 50B トークンでトレーニングしました。 評価方法と実験結果著者らは、Proof-Pile-2 を使用して Code Llama の事前トレーニングを継続し、MATH や GSM8k などの複数の数学的問題解決タスクで LLEMMA の少数ショット評価を実行しました。 研究者たちは、LLEMMA がこれらのタスクで大幅な改善を達成し、さまざまな問題の種類や困難に適応できることを発見しました。 非常に難しい数学の問題でも、LLEMMA 34B は他のオープンベースのモデルよりも強力な数学的能力を発揮できます。 数学ベンチマークでは、Proof-Pile-2 での LLEMMA の継続的な事前トレーニングにより、5 つの数学ベンチマークでの少数ショットのパフォーマンスが向上します。 LLEMMA 34B は、GSM8k では Code Llama より 20 パーセント ポイントの改善を達成し、MATH では 13 パーセント ポイントの改善を達成しました。 LLEMMA 7B は、同様のサイズの独自の Minerva モデルよりも優れたパフォーマンスを発揮し、Proof-Pile-2 での事前トレーニングによって大規模モデルの数学的問題解決能力を効果的に向上できることを実証しています。 Python などのコンピューティング ツールを使用して数学の問題を解決するという点では、LLEMMA は MATH+Python タスクと GSM8k+Python タスクの両方で Code Llama よりも優れています。 ツールを使用した MATH および GSM8k データセットでは、LLEMMA のパフォーマンスもツールを使用しない場合よりも高くなります。 LLEMMA は数学的な証明タスクでも優れたパフォーマンスを発揮します。 非公式から公式への証明タスクの目標は、正式なステートメント、非公式の LATEX ステートメント、および非公式の LATEX 証明が与えられた場合に、証明アシスタントによって検証できる正式な証明を生成することです。 形式的証明から形式的証明への変換は、一連の証明手順 (戦略) を生成することによって形式的なステートメントを証明することです。結果は、Proof-Pile-2 での LLEMMA の継続的な事前トレーニングにより、これら 2 つの正式な定理証明タスクにおける少数ショットのパフォーマンスが向上することを示しています。 LLEMMA は優れたパフォーマンスを発揮するだけでなく、革新的なデータセットを公開し、驚くべき問題解決能力を発揮します。 オープンソース共有の精神は、数学における新しい時代の始まりを示しています。数学の未来はここにあり、数学愛好家、研究者、教育者全員がその恩恵を受けるでしょう。 LLEMMA の出現により、数学の問題をより効率的かつ革新的に解決するための前例のないツールが提供されます。 さらに、オープンシェアリングの概念は、世界の科学研究コミュニティ間のより深い協力を促進し、科学の進歩を共同で促進することにもなります。 |
>>: HKU がオープンソースの推奨システムの新しいパラダイム RLMRec を公開!ユーザー/製品のテキストポートレートを正確に抽出するための大規模なモデルサポート
人類が科学技術の時代に入り、初期の単純な産業時代から複雑で多面的なハイテク産業時代へと進化して数百年...
今日はAIがどのように音楽を作曲するのかを見ていきたいと思います。この記事では、TensorFlow...
例と視覚化による 10 個の基本的なグラフ アルゴリズムの簡単な紹介グラフは、ソーシャル メディア ...
無人ヘリコプター自体は目新しいものではないが、現在市販されている無人ヘリコプターは、第一に誰かが遠隔...
現在、多くの自動運転車開発者は米国カリフォルニア州(以下、「カリフォルニア」という)で路上試験を行う...
1956年にコンピューターの専門家ジョン・マッカーシーが「人工知能」という言葉を作り出して以来、わず...
海外メディアの報道によると、マイクロソフトは水曜日、小規模な人工知能スタートアップ企業であるボンサイ...
7月24日、Appleは社内で従業員の業務を支援するためにチャットボットを使用しており、将来的には顧...