Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

要約

大規模な言語モデルは、特に数学的な問題を解決する際に、さまざまな自然言語処理タスクにわたって印象的な機能を実証しています。
ただし、大規模な言語モデルは、Leanのような正式な言語を使用して証明するMath Theoremでは良くありません。
この分野での重要な課題は、これらの正式な言語で利用可能なトレーニングデータが不足していることです。
この問題に対処するために、自然言語の数学的問題をリーン4ステートメントに変換するために合成データを繰り返し生成およびフィルタリングする新しいパイプラインを提案します。
私たちの結果は、合成データパイプラインが有用なトレーニングデータを提供し、複雑な数学的問題と証明を翻訳および理解する際のLLMのパフォーマンスを改善できることを示しています。
最終的なデータセットには、数学コンテストフォーラムからの検索された証明と21の新しいIMO質問とともに、約57kの正式な情報ペアが含まれています。
https://github.com/internlm/internlm-mathでコードをオープンソースし、https：//huggingface.co/datasets/internlm/lean-workbookでデータをオープンソースします。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google