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

要約

大規模な言語モデルは、さまざまな自然言語処理タスク、特に数学的問題の解決において優れた能力を実証しています。
ただし、大規模な言語モデルは、Lean のような形式言語を使用した数学の定理の証明が苦手です。
この分野における重大な課題は、これらの形式言語で利用できるトレーニング データが不足していることです。
この問題に対処するために、合成データを繰り返し生成してフィルタリングし、自然言語の数学的問題をリーン 4 ステートメントに変換したり、その逆を行ったりする新しいパイプラインを提案します。
私たちの結果は、合成データ パイプラインが有用なトレーニング データを提供し、複雑な数学的問題と証明を翻訳および理解する際の LLM のパフォーマンスを向上させることができることを示しています。
私たちの最終的なデータセットには、約 57,000 の公式質問と非公式質問のペアのほか、数学コンテスト フォーラムから検索された証明と 21 の新しい IMO 質問が含まれています。
コードは 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