ICLR 2024 スポットライト | 中間ステップを気にする必要がなく、MUSTARD は高品質の数学的推論データを生成できます

AIxivコラムは、当サイトが学術的・技術的な内容を掲載するコラムです。過去数年間で、このサイトの AIxiv コラムには 2,000 件を超えるレポートが寄せられ、世界中の主要な大学や企業のトップ研究室がカバーされ、学術交流と普及を効果的に促進しています。共有したい優れた作品がある場合は、お気軽に寄稿するか、報告のために当社までご連絡ください。提出電子メール: liyazhou@jiqizhixin.com; zhaoyunfeng@jiqizhixin.com。

近年、大規模言語モデル (LLM) は、数学的応用問題や数学的定理の証明などのタスクにおいて大きな進歩を遂げました。数学的推論には、厳密で形式化された複数ステップの推論プロセスが必要であるため、LLM の推論能力の向上における重要なマイルストーンですが、依然として重要な課題に直面しています。

思考連鎖 (CoT) などのこれまでの研究成果では、中間ステップのガイダンスの有効性が明らかになりました。ただし、このような中間ステップに手動で注釈を付けるには多くの人力と時間が必要であり、自動合成されたデータは正確性や人間の可読性の点で問題が発生しやすくなります。

この記事では、香港城市大学、中山大学、ファーウェイ・ノアの方舟研究所およびその他の機関の研究者が、多数の正しいデータを生成できる統一数理推論データ合成フレームワークMUSTARDを提案しています。読みやすく理解できる高品質の数的推論データ。

• 論文タイトル: MUSTARD: Mastering Unique Synthesis of Theorem and Proof Data
• 論文リンク: https://openreview.net/forum?id=8xliOUg9EW
• コードリンク: https:/ // /github.com/Eleanor-H/MUSTARD
• データセットリンク: https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view
• 著者ホームページ: https://eleanor - h.github.io/

形式証明者を活用した高品質なデータ合成フレームワーク

MUSTARDフレームワークは、

フェーズ1、

コンセプト取得の3つのフェーズで構成されています : まず、小学校、中学校、高校、高等教育の 4 つの教育段階の概念をカバーする数学概念ライブラリが定義および確立されます。各教育段階には 5 ～ 9 の数学領域があり、次のようなさまざまな種類の数学問題をカバーします。代数と幾何学として。各領域には、多項式演算や因数分解などの詳細な数学的概念が含まれています。次に、生成された質問カテゴリを特定するためのシードとして、数学的概念データベースから 1 つ以上の数学的概念が抽出されます。

第 2 段階、

データ生成: 大規模な言語モデルに、数学的概念に基づいた数学的問題と複数ステップの解決プロセスを生成させます。具体的には、MUSTARD は大規模言語モデルの機能を活用して自然言語とコードを生成し、大規模言語モデルに次の 3 つのタスクを完了させます。(T1) 特定の概念に関連する数学的問題を生成します。 (T3) 自動形式化。自然言語ソリューションをリーン 3 形式ソリューションに変換します。

第 3 段階、

形式的検証: インタラクティブな形式的定理証明器の検証を使用して、正確な解法プロセスを選別します。 MUSTARD が Lean 3 の形式解を Lean 形式検証者に渡した後、定理証明者がエラー情報を返さなかった場合、対応するデータは有効なセットに収集されます。それ以外の場合、MUSTARD は定理証明者からエラー メッセージを収集し、言語モデルに形式的解を変更するよう促します。 MUSTARD は、有効な正式な解決策が得られるまで、複数回の検証と自己修正を実行します。 MUSTARD フレームワークは、コンセプト収集、データ生成、形式的検証の 3 つの段階で構成されます。

データ品質の人による評価

MUSTARDによって生成されたデータの品質を調査するために、研究チームは数学とリーン3言語を熟知した専門家に品質チェックを依頼しました。データ上で。生成されたデータから 200 項目をランダムに選択し、そのうち 100 項目がリーン定理証明者の検証に合格し (有効グループ)、100 項目が検証に合格しなかった (無効グループ) としました。品質チェックは、正確性と一貫性のチェックを含め、各データの 4 つの部分 (つまり、自然言語の問題の説明、自然言語の解決策、形式的な問題の説明、形式的な解決策) を対象とします。具体的には、高品質のデータには、正しい自然言語の問題記述 (D1) と正しい問題解決 (D4) が含まれている必要があります。正式な問題の説明と解決策は、自然言語の問題の説明と解決策と一致している必要があります (D5、D6)。さらに、データは指定された数学的概念 (D2) および問題の種類 (D3) に準拠している必要があります。表 3 に、これら 6 つの検査寸法と要件を示します。データが要件を満たしている場合、ディメンションでスコア 1 が取得され、要件を満たしていない場合はスコア 0 が取得されます。

表 3 は、各次元における有効グループと無効グループの精度と対応する p 値を示しています。 (D1) と (D4) の大きな違いは、MUSTARD によって生成された質問と回答の正しさを示しています。 (D6) の大きな違いは、自然言語記述と生成されたデータの形式的記述の間の高い一貫性を示しています。

モデルの数学的推論能力に対するデータの有効性

数学的推論能力の向上に対するMUSTARDSAUCEの影響を評価するために、研究チームはこれらのデータを使用して小規模な言語を微調整しました数学的文章問題 (MWP) と自動定理証明 (ATP) で評価されます。この記事では、MUSTARDSAUCE データ セットの次の結合データの有効性を比較します。

• MUSTARDSAUCE-有効: リーン形式証明者によって検証された 5866 個のデータ
• MUSTARDSAUCE-無効: リーンに合格できませんでした。正式証明者によって検証された 5866 個のデータ;
• MUSTARDSAUCE-random: 5866 個のランダム データ;
• MUSTARDSAUCE-tt: MUSTARD によって生成されたすべての 28316 個のデータ。

研究チームは、オープンソース GPT2-large [2]、Llama 2-7B、Llama 2-70B [3] をそれぞれの結合データに対して微調整するために LoRA [1] を採用しました。数学的な文章問題のタスクでは、GSM8K [4] および MATH [5][6] データセットを評価に使用しました。自動化された定理証明を評価する際、研究チームは Mathlib [8] と miniF2F [7] ベンチマークを使用しました。さらに、MUSTARDSAUCE テストでも評価されました。

一般に、MUSTARDSAUCE でモデルを微調整すると、モデルの数学的推論能力が向上します。自動定理証明 (以下の表 5) および数学的応用問題解決 (以下の表 4) では、微調整に MUSTARDSAUCE-valid を使用した場合、微調整に MUSTARDSAUCE-random を使用した場合と比較して、平均相対パフォーマンスが 18.15% 向上しました (表 5)以下）および 11.01% %（以下の表 4）。

自動定理証明の場合、微調整された Llama 2-7B の平均パフォーマンス向上は 15.41%、微調整された GPT 2-large の平均パフォーマンス向上は 20.89% です。

数学的応用問題を解く場合、微調整された Llama 2-7B の平均パフォーマンスは 8.18% 向上し、微調整された GPT 2-large の平均パフォーマンスは 15.41% 向上しました。また、MUSTARDSAUCE-ttで微調整したモデルは、微調整データ量では絶対的に有利ですが、性能はMUSTARDSAUCE-validで微調整したモデルには及びません。

ラマ 2-70B のその他の結果。 MUSTARDSAUCE データは、より大きな言語モデルを微調整する場合にも有効なままです。

MUSTARDSAUCEデータセット

この記事は、MUSTARDSAUCEデータセットをオープンソース化しました。各データには、自然言語による問題の説明と複数ステップの解決策に加え、二重形式言語 Lean 3 による問題の説明と複数ステップの解決策が含まれています。 MUSTARDSAUCEのデータには、数学の応用問題や定理証明問題が含まれており、小学校から高等教育までの難易度をカバーしています。質問の推論ステップの数は、質問の難易度に応じて増加します。最も難しい問題には、解くのに約 30 のステップが必要で、リーン 3 戦略は約 20 個必要です。

データセットのダウンロード: https://drive.google.com/file/d/1yIVAVqpkC2Op7LhisG6BJJ_-MavAMr1B/view

自動形式化/非形式化チャレンジ

研究チームはまた、 MUSTARDSAUCE データセット内の自然言語とリーン形式言語の二重データに基づく自動形式化 (autoformalization) と自動非形式化 (auto-informalization) チャレンジ。さらに、研究チームは、定理の自動生成と証明、およびコードを使用したコード支援の自動最適化問題解決という 2 つのチャレンジ トラックを同時に開始しました。コンテストは2024年4月3日から5月27日まで行われます。優勝チームには、7 月 26 日にオーストリアのウィーンで開催される ICML 2024 AI for Math ワークショップに参加する機会が与えられます。

• トラック 1-1 (自動形式化): https://www.codabench.org/competitions/2436/
• トラック 1-2 (自動形式化): https://www.codabench .org/competitions/2484/
• トラック 2 (定理の自動生成と証明): https://www.codabench.org/competitions/2437/
• トラック 3 (コード支援によるオペレーション リサーチ最適化の自動ソリューション)問題): https://www.codabench.org/competitions/2438/

^{参考文献:}

^{[1] Edward J Hu、Yelong Shen、Phillip Wallis、Zeyuan Allen- Zhu、Yuanzhi Li、Shean Wang、Lu Wang、および Weizhu Chen Lora: arXiv プレプリント arXiv:2106.09685、2021.}

^{[2] Alec Radford、Jeffrey Wu、Rewon。 Child、David Luan、Dario Amodei、Ilya Sutskever、他、言語モデルは教師なしマルチタスク学習者、1 (8):9、2019 年。}

^{[3] Hugo Touvron、Louis Martin、Kevin Stone。 、ピーター・アルバート、アムジャド・アルマハイリ、ヤスミン・ババエイ、ニコライ・バシリコフ、ソウミャ・バトラ、プラジワル・バルガヴァ、シュルティ・ボサレ、ダン・ビケル、ルーカス・ブレッチャー、クリスティアン・カントン＝フェラー、モヤ・チェン、ギレム・ククルル、デヴィッド・エシオブ、ジュード・フェルナンデス、ジェレミー・フー、ウェニン・フー、ブライアン・フラー、シンシア・ガオ、ヴェダヌジ・ゴスワミ、ナマン・ゴヤル、アンソニー・ハーツホルン、サガー・ホッセイニ、ルイ・ホウ、ハカン・イナン、マルシン・カルダス、ヴィクトル・ケルケズ、マディアン・カブサ、イザベル・クルーマン、アルテム・コレネフ、プニット・シン・コウラ、マリー＝アン・ラショー、ティボー・ラブリル、ジェーニャ・リー、ダイアナ・リスコビッチ、インハイ・ルー、ユーニン・マオ、ザビエル・マルティネット、トドール・ミハイロフ、プシュカル・ミシュラ、イゴール・モリボグ、イーシン・ニー、アンドリュー・ポールトン、ジェレミー・ライゼンスタイン、ラシ・ルンタ、カリヤン・サラディ、アラン・シェルテン、ルアン・シルバ、エリックマイケル・スミス、ランジャン・スブラマニアン、シャオチン・エレン・タン、ビン・タン、ロス・テイラー、アディナ・ウィリアムズ、ジャン・シャン・クアン、プシン・シュー、ジェン・ヤン、イリヤーン・ザロフ、ユチェン・チャン、アンジェラ・ファン、メラニー・カンバドゥル、シャラン・ナラン、オーレ・リエン・ロドリゲス、ロバート・ストジニッチ、Sergey Edunov、および Thomas Scialom。Llama 2: オープン基盤と微調整されたチャット モデル、abs/2307.09288。URL https://doi. .}

^{[4] Karl Cobbe、Vineet Kosaraju、Mohammad Bavarian、Mark Chen、Heewoo Jun、Lukasz Kaiser、Matthias Prappert、Jerry Tworek、Jacob Hilton、中野礼一郎、Christopher Hesse、John Schulman へのトレーニング検証者。数学の文章問題を解く。CoRR、abs/2110.14168、2021。}

^{[5] Dan Hendrycks、Collin Burns、Saurav Kadavath、Akul Arora、Steven Basart、Eric Tang、Dawn Song、Jacob Steinhardt の測定。 Joaquin Vanschoren および Sai-Kit Yeung (編)、Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1、NeurIPS Datasets and Benchmarks 2021、2021 年 12 月、仮想、2021 年。} [6] Hunter Lightman、Vineet Kosaraju、Yura Burda、Harri Edwards、Bowen Baker、Teddy Lee、Jan Leike、John Schulman、Ilya Sutskever、Karl Cobbe arXiv:2305.20050、2023 を段階的に検証してみましょう。 .

^{[7] Kunhao Zheng、Jesse Michael Han、および Stanislas Polu。minif2f: 正式なオリンピックレベルの数学のクロスシステムベンチマーク、ICLR 2022、仮想。イベント、2022 年 4 月 25 ～ 29 日。OpenReview.net、2022 年。}

^{[8] https://github.com/leanprover-community/mathlib}

以上がICLR 2024 スポットライト | 中間ステップを気にする必要がなく、MUSTARD は高品質の数学的推論データを生成できますの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。