論文の概要: ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

• arxiv url: http://arxiv.org/abs/2502.05567v1
• Date: Sat, 08 Feb 2025 13:28:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-11 14:36:11.185258
• Title: ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data
• Title（参考訳）: ATLAS: データのリフティング、拡張、合成による自己形式化理論
• Authors: Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo,
• Abstract要約: ATLASは大規模で高品質な並列定理文を生成するために設計された反復データ生成フレームワークである。 我々は300kの定理文からなる学部レベルのデータセットを構築し,ATLASトランスレータを開発し,ProofNet上で80.59%(pass@8)および92.99%(pass@128)の精度を達成した。 ATLASトランスレータは、高学年のminiF2Fデータセットと、この研究で導入された大学院レベルのMathQualデータセットの両方で最先端のパフォーマンスを達成する。
• 参考スコア（独自算出の注目度）: 14.409949582947435
• License:
• Abstract: Autoformalization, the process of automatically translating natural language mathematics into machine-verifiable formal language, has demonstrated advancements with the progress of large language models (LLMs). However, a key obstacle to further advancements is the scarcity of paired datasets that align natural language with formal language. To address this challenge, we introduce ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data), an iterative data generation framework designed to produce large-scale, high-quality parallel theorem statements. With the proposed ATLAS running for 10 iterations, we construct an undergraduate-level dataset comprising 300k theorem statements and develop the ATLAS translator, achieving accuracies of 80.59% (pass@8) and 92.99% (pass@128) on ProofNet, significantly outperforming the base model (23.99% and 47.17%) and InternLM2-Math-Plus-7B (50.94% and 80.32%). Furthermore, the ATLAS translator also achieves state-of-the-art performance on both the high-school-level miniF2F dataset and the graduate-level MathQual dataset introduced in this work. The datasets, model, and code will be released to the public soon.
• Abstract（参考訳）: 自然言語を機械で検証可能な形式言語に自動翻訳する手法であるオートフォーマル化(Autoformalization)は,大規模言語モデル(LLM)の進歩とともに進歩を見せている。 しかし、さらなる進歩の鍵となる障害は、自然言語と形式言語を整列するペアデータセットの不足である。 この課題に対処するために,大規模かつ高品質な並列定理文を生成するために設計された反復データ生成フレームワークであるATLAS(Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data)を紹介する。 提案したATLASを10回に分けて,300kの定理文からなる学部レベルのデータセットを構築し,80.59%(pass@8)と92.99%(pass@128)の精度をProofNet上で達成し,ベースモデル(23.99%,47.17%)とInternLM2-Math-Plus-7B(50.94%,80.32%)を大きく上回った。 さらに、ATLASトランスレータは、高学年のminiF2Fデータセットと、本研究で導入された大学院レベルのMathQualデータセットの両方で最先端のパフォーマンスを達成する。 データセット、モデル、コードはまもなく一般公開される予定だ。

関連論文リスト

• Building Math Agents with Multi-Turn Iterative Preference Learning [56.71330214021884]
  本稿では,モデル性能をさらに向上させるために,補完的な直接選好学習手法について検討する。 既存の直接選好学習アルゴリズムは、もともとシングルターンチャットタスク用に設計されている。 この文脈に合わせたマルチターン直接選好学習フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-09-04T02:41:04Z)
• SUMIE: A Synthetic Benchmark for Incremental Entity Summarization [6.149024468471498]
  既存のデータセットは、言語モデルがエンティティの要約を段階的に更新できるかどうかを適切にテストしていません。 我々は、実世界のIES課題を明らかにするために設計された、完全に合成されたデータセットであるSUMIEを紹介する。 このデータセットは、誤ったエンティティアソシエーションや不完全な情報提示といった問題を効果的に強調する。
  論文  参考訳（メタデータ） (2024-06-07T16:49:21Z)
• 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)
• Improving Attributed Text Generation of Large Language Models via Preference Learning [28.09715554543885]
  属性タスクを選好学習としてモデル化し,自動選好最適化フレームワークを導入する。 APOは、回答品質の高い最先端の引用F1を達成する。
  論文  参考訳（メタデータ） (2024-03-27T09:19:13Z)
• ILLUMINER: Instruction-tuned Large Language Models as Few-shot Intent Classifier and Slot Filler [1.9015367254988451]
  本研究では、インテント分類(IC)とスロットフィリング(SF)のための人気のあるベンチマークデータセット上で、命令調整モデル(インストラクション-LLM)を評価する。 Instruct-LLM の言語生成タスクとして IC と SF をフレーミングする ILLUMINER を導入する。 FLAN-T5 11Bモデルを用いた複数のベースラインとの総合的な比較から,本手法は最先端のジョイントIC+SF法やGPT3.5 (175B) を用いたテキスト内学習よりも優れていた。
  論文  参考訳（メタデータ） (2024-03-26T09:41:21Z)
• Instructed Language Models with Retrievers Are Powerful Entity Linkers [87.16283281290053]
  Instructed Generative Entity Linker (INSGENEL)は、カジュアル言語モデルが知識ベース上でエンティティリンクを実行することを可能にする最初のアプローチである。 INSGENEL は、+6.8 F1 点が平均的に上昇する以前の生成的代替よりも優れていた。
  論文  参考訳（メタデータ） (2023-11-06T16:38:51Z)
• TarGEN: Targeted Data Generation with Large Language Models [51.87504111286201]
  TarGENは、高品質な合成データセットを生成するための、多段階のプロンプト戦略である。 我々は,LLMが不正確なラベル付きインスタンスを修正できるようにする自己補正法により,TarGENを増強する。 合成データセットを元のデータセットと比較した包括的な分析により、データセットの複雑さと多様性の類似または高いレベルが明らかになる。
  論文  参考訳（メタデータ） (2023-10-27T03:32:17Z)
• Text Classification via Large Language Models [63.1874290788797]
  テキスト分類に関わる複雑な言語現象に対処するために、Clue And Reasoning Prompting (CARP)を導入する。 注目すべきは、CARPが5つの広く使用されているテキスト分類ベンチマークのうち4つで新しいSOTAパフォーマンスを得ることだ。 さらに重要なのは、CARPが低リソースとドメイン適応のセットアップで素晴らしい能力を提供します。
  論文  参考訳（メタデータ） (2023-05-15T06:24:45Z)
• Exploiting Asymmetry for Synthetic Training Data Generation: SynthIE and the Case of Information Extraction [28.51694365908817]
  本研究は,大規模言語モデルでは直接解けないタスクに対しても,有用なデータを合成的に生成できることを示唆する。 我々は、1.8Mのデータポイントのデータセットを合成的に生成し、人間の評価において既存のデータセットと比較して優れた品質を確立する。
  論文  参考訳（メタデータ） (2023-03-07T18:48:55Z)
• The USYD-JD Speech Translation System for IWSLT 2021 [85.64797317290349]
  本稿では,シドニー大学とJDが共同でIWSLT 2021低リソース音声翻訳タスクを提出したことを述べる。 私たちは、公式に提供されたASRとMTデータセットでモデルをトレーニングしました。 翻訳性能の向上を目的として, バック翻訳, 知識蒸留, 多機能再構成, トランスダクティブファインタニングなど, 最新の効果的な手法について検討した。
  論文  参考訳（メタデータ） (2021-07-24T09:53:34Z)

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

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