MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

要約

最近の大規模言語モデル (LLM) は、数学的推論や定理証明などのさまざまなタスクで大幅な進歩を遂げています。
これら 2 つのタスクは厳密で形式的な複数ステップの推論を必要とするため、LLM の推論能力を探求するには魅力的な領域ですが、依然として重要な課題に直面しています。
思考連鎖 (CoT) などのこれまでの研究により、中間ステップのガイダンスの有効性が明らかになりました。
ただし、このような段階的なアノテーションには多大な労力が必要であり、現在のベンチマークのトレーニング ステップが不十分になります。
このギャップを埋めるために、この研究では、高品質で多様性のある定理と証明データの均一な合成を習得するデータ生成フレームワークである MUSTARD を紹介します。
MUSTARD は 3 つの段階でデータを合成します。 (1) いくつかの数学的概念のシードを問題カテゴリとしてサンプリングします。
(2) 次に、サンプリングされた概念を使用して生成言語モデルを生成し、問題とその段階的な形式的解決策の両方を取得します。
(3) 最後に、フレームワークは証明アシスタント (Lean Prover など) を利用して有効な証明をフィルタリングします。
提案された MUSTARD では、5,866 個の有効なデータ ポイントを持つ定理と証明のベンチマーク MUSTARDSAUCE を提示します。
各データ ポイントには、非公式のステートメント、非公式の証明、および証明者の検証に合格した翻訳された正式な証明が含まれています。
私たちは広範な分析を実行し、MUSTARD が検証済みの高品質な段階的なデータを生成することを実証します。
さらに、小さな言語モデルを微調整するために MUSTARDSAUCE を適用します。
微調整された Llama 2-7B は、自動化された定理証明で平均 15.41%、数学の文章問題で 8.18% の平均相対パフォーマンス向上を達成しました。
コードとデータは https://github.com/Eleanor-H/MUSTARD で入手できます。

要約(オリジナル)

Recent large language models (LLMs) have witnessed significant advancement in various tasks, including mathematical reasoning and theorem proving. As these two tasks require strict and formal multi-step inference, they are appealing domains for exploring the reasoning ability of LLMs but still face important challenges. Previous studies such as Chain-of-Thought (CoT) have revealed the effectiveness of intermediate steps guidance. However, such step-wise annotation requires heavy labor, leading to insufficient training steps for current benchmarks. To fill this gap, this work introduces MUSTARD, a data generation framework that masters uniform synthesis of theorem and proof data of high quality and diversity. MUSTARD synthesizes data in three stages: (1) It samples a few mathematical concept seeds as the problem category. (2) Then, it prompts a generative language model with the sampled concepts to obtain both the problems and their step-wise formal solutions. (3) Lastly, the framework utilizes a proof assistant (e.g., Lean Prover) to filter the valid proofs. With the proposed MUSTARD, we present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. Each data point contains an informal statement, an informal proof, and a translated formal proof that passes the prover validation. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data. We further apply the MUSTARDSAUCE for fine-tuning smaller language models. The fine-tuned Llama 2-7B achieves a 15.41% average relative performance gain in automated theorem proving, and 8.18% in math word problems. Codes and data are available at https://github.com/Eleanor-H/MUSTARD.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google