論文の概要: Herald: A Natural Language Annotated Lean 4 Dataset

• arxiv url: http://arxiv.org/abs/2410.10878v1
• Date: Wed, 09 Oct 2024 10:11:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-16 14:04:39.649462
• Title: Herald: A Natural Language Annotated Lean 4 Dataset
• Title（参考訳）: Herald: 自然言語によるリーン4データセット
• Authors: Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, Bin Dong,
• Abstract要約: 本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。 私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。 また,Heraldを微調整したHerald Translatorを提案する。
• 参考スコア（独自算出の注目度）: 15.42247133378869
• License:
• Abstract: Verifiable formal languages like Lean have profoundly impacted mathematical reasoning, particularly through the use of large language models (LLMs) for automated reasoning. A significant challenge in training LLMs for these formal languages is the lack of parallel datasets that align natural language with formal language proofs. To address this challenge, this paper introduces a novel framework for translating the Mathlib4 corpus (a unified library of mathematics in formal language Lean 4) into natural language. Building upon this, we employ a dual augmentation strategy that combines tactic-based and informal-based approaches, leveraging the Lean-jixia system, a Lean 4 analyzer. We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-based Translated Lean Dataset). We also propose the Herald Translator, which is fine-tuned on Herald. Herald translator achieves a 93.2% accuracy (Pass@128) on formalizing statements in the miniF2F-test and a 22.5% accuracy on our internal graduate-level textbook dataset, outperforming InternLM2-Math-Plus-7B (74.0% and 7.5%) and TheoremLlama (50.1% and 4.0%). Furthermore, we propose a section-level translation framework for real-world applications. As a direct application of Herald translator, we have successfully translated a template section in the Stack project, marking a notable progress in the automatic formalization of graduate-level mathematical literature. Our model, along with the datasets, will be open-sourced to the public soon.
• Abstract（参考訳）: リーンのような検証可能な形式言語は、特に自動推論に大規模言語モデル(LLM)を使用することによって、数学的推論に大きな影響を与えています。 これらの形式言語のためのLLMのトレーニングにおける重要な課題は、自然言語と形式言語証明を整列する並列データセットの欠如である。 この課題に対処するため,本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳する新しいフレームワークを提案する。 これに基づいて、戦術ベースと非公式ベースのアプローチを組み合わせて、リーン4アナライザであるLean-jixiaシステムを活用する、二重強化戦略を採用しています。 私たちは、このパイプラインの結果をHerald(階層とレトリバルベースのトランスレーショナルリーンデータセット)としてMathlib4に示します。 また,Heraldを微調整したHerald Translatorを提案する。 Herald Translatorは、MiniF2F-testにおけるステートメントの形式化に関する93.2%の精度(Pass@128)と、内部の大学院レベルの教科書データセットの22.5%の精度、InternLM2-Math-Plus-7B(74.0%と7.5%)とTheoremLlama(50.1%と4.0%)を上回ります。 さらに,実世界のアプリケーションを対象としたセクションレベルの翻訳フレームワークを提案する。 Herald Translatorの直接的な応用として、Stackプロジェクトにおけるテンプレートセクションの翻訳に成功した。 当社のモデルとデータセットは,近く一般公開される予定です。

関連論文リスト

• 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)
• 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)
• Process-Driven Autoformalization in Lean 4 [30.056591518828554]
  大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。 また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。 実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
  論文  参考訳（メタデータ） (2024-06-04T03:48:08Z)
• 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)
• Zero-Shot Cross-Lingual Reranking with Large Language Models for Low-Resource Languages [51.301942056881146]
  アフリカ語における言語間情報検索システムにおいて,大規模言語モデル (LLM) がリランカーとしてどのように機能するかを検討する。 私たちの実装は、英語と4つのアフリカの言語(ハウサ語、ソマリ語、スワヒリ語、ヨルバ語)を対象としています。 我々は、英語のクェリとアフリカの言葉の文節による言語横断的な格付けについて検討する。
  論文  参考訳（メタデータ） (2023-12-26T18:38:54Z)
• Cross-Lingual NER for Financial Transaction Data in Low-Resource Languages [70.25418443146435]
  半構造化テキストデータにおける言語間名前認識のための効率的なモデリングフレームワークを提案する。 我々は2つの独立したSMSデータセットを英語とアラビア語で使用し、それぞれが半構造化された銀行取引情報を持っている。 わずか30のラベル付きサンプルにアクセスすることで、我々のモデルは、英語からアラビア語までの商人、金額、その他の分野の認識を一般化することができる。
  論文  参考訳（メタデータ） (2023-07-16T00:45:42Z)
• Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis [103.89753784762445]
  大規模言語モデル(LLM)は多言語機械翻訳(MMT)の処理において顕著な可能性を示した。 本稿では, MMT における LLM の利点と課題を体系的に検討する。 また,ChatGPTとGPT-4を含む8つのLLMを徹底的に評価した。
  論文  参考訳（メタデータ） (2023-04-10T15:51:30Z)
• A Commonsense-Infused Language-Agnostic Learning Framework for Enhancing Prediction of Political Polarity in Multilingual News Headlines [0.0]
  対象言語における推論知識を取得するために,翻訳と検索の手法を用いる。 次に、重要な推論を強調するために注意機構を使用します。 我々は、それぞれの政治的極性に注釈を付けた5つのヨーロッパ言語で62.6K以上の多言語ニュースの見出しを提示する。
  論文  参考訳（メタデータ） (2022-12-01T06:07:01Z)

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

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