論文の概要: LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

• arxiv url: http://arxiv.org/abs/2407.17227v1
• Date: Wed, 24 Jul 2024 12:28:03 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-25 13:54:30.611939
• Title: LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover
• Title（参考訳）: LEAN-GitHub: 汎用LEAN証明のためにGitHub LEANリポジトリをコンパイルする
• Authors: Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen,
• Abstract要約: 我々は、GitHub上のLean 4リポジトリから抽出された大規模なフォーマルデータからなるデータセットであるLEAN-GitHubを提案する。 我々のモデルは1回のパスで48.8%、64回のパスで54.5%、Lean 4 miniF2Fテストで54.5%に達し、最先端のメソッドを52%上回った。
• 参考スコア（独自算出の注目度）: 56.34998574538897
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be extracted from raw formal language corpora. Meanwhile, a significant amount of human-written formal language corpora remains underutilized. To address this issue, we propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from almost all Lean 4 repositories on GitHub. After fine-tuning InternLM-math-plus on this dataset, our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%. And it also achieves state-of-the-art on two other Lean 4 benchmarks (ProofNet and Putnam) targeting different fields/levels of math. These results demonstrate that our proposed dataset is beneficial for formal reasoning on a wide range of math topics. We open-source our model at https://GitHub. com/InternLM/InternLM-Math and our data at https://huggingface.co/ datasets/InternLM/Lean-GitHub
• Abstract（参考訳）: 近年,大規模言語モデルは形式的数学的推論を支援する上で有望な結果をもたらしている。 しかし、それらの性能は、形式的定理証明データが不足しているために制限されており、これは生の形式的言語コーパスから追加の労力を必要とする。 一方、人文言語コーパスの大量使用は未使用のままである。 この問題に対処するため、私たちは、GitHub上のほぼすべてのLean 4リポジトリから抽出された大規模なフォーマルデータからなるデータセットであるLEAN-GitHubを提案する。 このデータセットを微調整した後、我々のモデルは1回のパスで48.8%、64回のパスで54.5%、Lean 4 miniF2Fテストで54.5%に達し、最先端のメソッドを52%上回った。 他にも2つのLean 4ベンチマーク(ProofNetとPutnam)で、さまざまな分野や数学レベルをターゲットにしています。 これらの結果から,提案したデータセットは,幅広い数学トピックに関する公式な推論に有用であることが示唆された。 当社のモデルをhttps://GitHub.comで公開しています。 https://huggingface.co/ datas/InternLM/Lean-GitHub

関連論文リスト

• Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
  本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。 私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。 また,Heraldを微調整したHerald Translatorを提案する。
  論文  参考訳（メタデータ） (2024-10-09T10:11:24Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
  大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。 この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。 本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
  論文  参考訳（メタデータ） (2024-06-06T08:25:43Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
  InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。 我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。 我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
  論文  参考訳（メタデータ） (2024-02-09T11:22:08Z)
• MathCoder: Seamless Code Integration in LLMs for Enhanced Mathematical Reasoning [52.97768001837269]
  本稿では,オープンソース言語モデルを微調整する手法を提案する。 本稿では,問題のある新しい,高品質なデータセットを生成する手法とそのコードベースソリューションを提案する。 このアプローチは、問題の解決にコードベースのソリューションを生成することができるモデルのファミリーであるMathCoderモデルを生成する。
  論文  参考訳（メタデータ） (2023-10-05T17:52:09Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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