論文の概要: Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

• arxiv url: http://arxiv.org/abs/2406.03847v1
• Date: Thu, 6 Jun 2024 08:25:43 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-07 15:49:43.826307
• Title: Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
• Title（参考訳）: Lean Workbook: 自然言語の数学問題から形式化した大規模なリーン問題セット
• Authors: Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, Kai Chen,
• Abstract要約: 大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
• 参考スコア（独自算出の注目度）: 50.22847430754973
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large language models have demonstrated impressive capabilities across various natural language processing tasks, especially in solving mathematical problems. However, large language models are not good at math theorem proving using formal languages like Lean. A significant challenge in this area is the scarcity of training data available in these formal languages. To address this issue, we propose a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems into Lean 4 statements, and vice versa. Our results indicate that the synthetic data pipeline can provide useful training data and improve the performance of LLMs in translating and understanding complex mathematical problems and proofs. Our final dataset contains about 57K formal-informal question pairs along with searched proof from the math contest forum and 21 new IMO questions. We open-source our code at https://github.com/InternLM/InternLM-Math and our data at https://huggingface.co/datasets/InternLM/Lean-Workbook.
• Abstract（参考訳）: 大規模言語モデルは、特に数学的な問題を解く際に、様々な自然言語処理タスクにおいて印象的な能力を示してきた。 しかし、大きな言語モデルは、リーンのような形式的な言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 この問題に対処するために、我々は、自然言語の数学的問題をリーン4文に変換するために、合成データを反復的に生成し、フィルタする新しいパイプラインを提案します。 その結果, 合成データパイプラインは, 複雑な数学的問題や証明の翻訳・理解において, 有用な学習データを提供し, LLMの性能を向上させることが示唆された。 最終データセットには、約5万5千の形式的非形式的質問対と、数学コンテストフォーラムからの探索された証明と21の新しいIMO質問が含まれている。 当社のコードはhttps://github.com/InternLM/InternLM-Mathで、データはhttps://huggingface.co/datasets/InternLM/Lean-Workbookで公開しています。

関連論文リスト

• Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
  本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。 私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。 また,Heraldを微調整したHerald Translatorを提案する。
  論文  参考訳（メタデータ） (2024-10-09T10:11:24Z)
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover [56.34998574538897]
  我々は、GitHub上のLean 4リポジトリから抽出された大規模なフォーマルデータからなるデータセットであるLEAN-GitHubを提案する。 我々のモデルは1回のパスで48.8%、64回のパスで54.5%、Lean 4 miniF2Fテストで54.5%に達し、最先端のメソッドを52%上回った。
  論文  参考訳（メタデータ） (2024-07-24T12:28:03Z)
• JiuZhang3.0: Efficiently Improving Mathematical Reasoning by Training Small Data Synthesis Models [110.45794710162241]
  既存の研究は、事前学習のための大規模な数学関連のテキストを収集したり、巨大な数学問題を合成するために強力なLLMに依存している。 そこで本研究では,数学問題合成のための小さなLLMを効率的に学習し,高品質な事前学習データを効率的に生成する手法を提案する。 我々は、GPT-4 API 9.3k回の呼び出しと4.6Bデータの事前トレーニングのみを必要とする、JuZhang3.0モデルの事前トレーニングに600万の数学問題を合成する。
  論文  参考訳（メタデータ） (2024-05-23T09:43:19Z)
• ChatGLM-Math: Improving Math Problem-Solving in Large Language Models with a Self-Critique Pipeline [42.61538071832468]
  大規模言語モデル(LLM)は、人間の言語の優れた習得を示すが、数学的な問題解決を必要とする現実世界のアプリケーションでは依然として苦戦している。 LLMアライメントのフィードバック学習段階における課題に対処する自己批判パイプラインを調整します。
  論文  参考訳（メタデータ） (2024-04-03T17:51:18Z)
• Can LLM Generate Culturally Relevant Commonsense QA Data? Case Study in Indonesian and Sundanese [14.463110500907492]
  大規模言語モデル(LLM)は、モデルを訓練し、評価するために合成データを生成するために、ますます使われている。 言語に埋め込まれた知識と文化的ニュアンスを組み込んだQAデータセットを生成できるかどうかは不明だ。 本研究では,インドネシア語とスンダ語における文化関連コモンセンスQAデータセット作成におけるLLMの利用の有効性について検討した。
  論文  参考訳（メタデータ） (2024-02-27T08:24:32Z)
• MARIO: MAth Reasoning with code Interpreter Output -- A Reproducible Pipeline [12.186691561822256]
  我々は,大規模言語モデル(LLM)の本質的な性質が,数学的推論のモデル化における課題を提起していると仮定する。 本稿では,Pythonコードインタプリタを利用した新しい数学データセットを提案する。 本稿では,数学固有のLLMの微調整のための仮的かつ容易に複製可能なプロトコルを提案する。
  論文  参考訳（メタデータ） (2024-01-16T08:08:01Z)
• MathCoder: Seamless Code Integration in LLMs for Enhanced Mathematical Reasoning [52.97768001837269]
  本稿では,オープンソース言語モデルを微調整する手法を提案する。 本稿では,問題のある新しい,高品質なデータセットを生成する手法とそのコードベースソリューションを提案する。 このアプローチは、問題の解決にコードベースのソリューションを生成することができるモデルのファミリーであるMathCoderモデルを生成する。
  論文  参考訳（メタデータ） (2023-10-05T17:52:09Z)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  我々は,SimulMTタスクに大規模言語モデルを適用する可能性を検討する。 MUST-Cデータセットと異なる9言語でtextttLlama2-7b-chatモデルを用いて実験を行った。 その結果,LLM は BLEU と LAAL の指標で専用MT モデルよりも優れていた。
  論文  参考訳（メタデータ） (2023-09-13T04:06:47Z)
• PAL: Program-aided Language Models [112.94785609781503]
  自然言語問題を理解するために,プログラム支援言語モデル(PaL)を提案する。 PaLはソリューションステップをPythonインタプリタのようなプログラムランタイムにオフロードする。 私たちは12のベンチマークで新しい最先端の結果を設定しました。
  論文  参考訳（メタデータ） (2022-11-18T18:56:13Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。