論文の概要: Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization

• arxiv url: http://arxiv.org/abs/2502.15795v1
• Date: Tue, 18 Feb 2025 19:16:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-25 15:59:30.707060
• Title: Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization
• Title（参考訳）: 品質のリーン化: 高品質なデータが多言語データのオートフォーマル化にいかに勝るか
• Authors: Willy Chan, Michael Souliman, Jakob Nordhagen, Brando Miranda, Elyas Obbad, Kai Fronsdal Sanmi Koyejo,
• Abstract要約: 本稿では,言語モデルの数学的能力を高めるために,手書きのプロンプトを用いた逆翻訳を利用する新しい手法を提案する。 提案手法は,広範囲な多言語データセットを用いた微調整性能を上回ることを示す。 まとめると、我々の手法は、形式化に必要なリソースを大幅に削減し、数学のためのAIを加速する、有望な新しいアプローチを示す。
• 参考スコア（独自算出の注目度）: 1.204553980682492
• License:
• Abstract: Autoformalization, the process of transforming informal mathematical language into formal specifications and proofs remains a difficult task for state-of-the-art (large) language models. Existing works point to competing explanations for the performance gap. To this end, we introduce a novel methodology that leverages back-translation with hand-curated prompts to enhance the mathematical capabilities of language models, particularly addressing the challenge posed by the scarcity of labeled data. Specifically, we evaluate three primary variations of this strategy: (1) on-the-fly (online) backtranslation, (2) distilled (offline) backtranslation with few-shot amplification, and (3) line-by-line proof analysis integrated with proof state information. Each variant is designed to optimize data quality over quantity, focusing on the high fidelity of generated proofs rather than sheer data scale. Our findings provide evidence that employing our proposed approaches to generate synthetic data, which prioritizes quality over volume, improves the Autoformalization performance of LLMs as measured by standard benchmarks such as ProofNet. Crucially, our approach outperforms pretrained models using a minimal number of tokens. We also show, through strategic prompting and backtranslation, that our approaches surpass the performance of fine-tuning with extensive multilingual datasets such as MMA on ProofNet with only 1/150th of the tokens. Taken together, our methods show a promising new approach to significantly reduce the resources required to formalize proofs, thereby accelerating AI for math.
• Abstract（参考訳）: オートフォーマル化(Autoformalization)は、非公式な数学的言語を形式的な仕様や証明に変換するプロセスであり、最先端の(大規模な)言語モデルにとって難しい課題である。 既存の作業は、パフォーマンスギャップについて、競合する説明を示している。 そこで本稿では,手書きのプロンプトによるバックトランスレーションを利用して,言語モデルの数学的能力を高める手法を紹介し,特にラベル付きデータの不足による課題に対処する。 具体的には,(1)オンザフライ(オンライン)バックトランスレーション,(2)少数ショット増幅による蒸留(オフライン)バックトランスレーション,(3)証明状態情報と統合されたライン・バイ・ライン証明分析の3つの戦略について検討した。 各変種は、データスケールではなく、生成した証明の忠実度に重点を置いて、量よりもデータ品質を最適化するように設計されている。 この結果から,提案手法を用いて合成データを生成することにより,ProofNetなどの標準ベンチマークによるLCMの自動形式化性能が向上することを示す。 重要なことに、我々のアプローチは最小限のトークンを使って事前訓練されたモデルより優れている。 また、戦略的プロンプトやバックトランスレーションを通じて、トークンの1/150しか持たないProofNet上のMMAのような多言語データセットによる微調整の性能を上回ることを示す。 この手法は,証明の形式化に必要な資源を大幅に削減し,数学のAIを高速化する,有望な新しい手法を示す。

関連論文リスト

• Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques [0.0]
  本稿では,ChatGPTと基本探索技術を統合し,形式的証明の簡易化について検討する。 私たちはChatGPTのような大きな言語モデルとLeanのような形式的な言語を組み合わせることで、検証可能なメリットが加わり、形式的な証明生成の効率性とアクセシビリティが向上することを示す。
  論文  参考訳（メタデータ） (2025-02-05T16:21:10Z)
• Unsupervised Pre-training with Language-Vision Prompts for Low-Data Instance Segmentation [105.23631749213729]
  低データ体制における教師なし事前学習のための新しい手法を提案する。 最近成功したプロンプト技術に触発されて,言語ビジョンプロンプトを用いた教師なし事前学習法を導入した。 提案手法は,低データ方式のCNNモデルよりも高速に収束し,性能がよいことを示す。
  論文  参考訳（メタデータ） (2024-05-22T06:48:43Z)
• Improving Attributed Text Generation of Large Language Models via Preference Learning [28.09715554543885]
  属性タスクを選好学習としてモデル化し,自動選好最適化フレームワークを導入する。 APOは、回答品質の高い最先端の引用F1を達成する。
  論文  参考訳（メタデータ） (2024-03-27T09:19:13Z)
• Ensemble Transfer Learning for Multilingual Coreference Resolution [60.409789753164944]
  非英語で作業する場合に頻繁に発生する問題は、注釈付きトレーニングデータの不足である。 我々は,様々なトランスファー学習技術を組み合わせた,シンプルだが効果的なアンサンブルベースのフレームワークを設計する。 また、ウィキペディアアンカーテキストを利用して、コア参照解決モデルをブートストラップする低コストのTL手法を提案する。
  論文  参考訳（メタデータ） (2023-01-22T18:22:55Z)
• On the Usability of Transformers-based models for a French Question-Answering task [2.44288434255221]
  本稿では,大規模学習問題におけるトランスフォーマーに基づく言語モデルのユーザビリティに着目した。 本稿では,低リソース環境下での競合性を示すFrALBERTの新しいコンパクトモデルを提案する。
  論文  参考訳（メタデータ） (2022-07-19T09:46:15Z)
• Efficient Entity Candidate Generation for Low-Resource Languages [13.789451365205665]
  候補生成はエンティティリンクにおいて重要なモジュールである。 知識ベースを効果的に活用することが証明された複数のNLPタスクにおいて重要な役割を果たす。 本稿では,言語間エンティティリンクの文脈における候補生成問題の詳細な分析を行う。
  論文  参考訳（メタデータ） (2022-06-30T09:49:53Z)
• Improving Pre-trained Language Model Fine-tuning with Noise Stability Regularization [94.4409074435894]
  本稿では,LNSR(Layerwise Noise Stability Regularization)という,新規かつ効果的な微調整フレームワークを提案する。 具体的には、標準ガウス雑音を注入し、微調整モデルの隠れ表現を正規化することを提案する。 提案手法は,L2-SP,Mixout,SMARTなど他の最先端アルゴリズムよりも優れていることを示す。
  論文  参考訳（メタデータ） (2022-06-12T04:42:49Z)
• Unsupervised Domain Adaptation of a Pretrained Cross-Lingual Language Model [58.27176041092891]
  最近の研究は、大規模未ラベルテキストに対する言語間言語モデルの事前学習が、大幅な性能向上をもたらすことを示唆している。 本稿では,絡み合った事前学習した言語間表現からドメイン固有の特徴を自動的に抽出する,教師なし特徴分解手法を提案する。 提案モデルでは、相互情報推定を利用して、言語間モデルによって計算された表現をドメイン不変部分とドメイン固有部分に分解する。
  論文  参考訳（メタデータ） (2020-11-23T16:00:42Z)
• Unsupervised Paraphrasing with Pretrained Language Models [85.03373221588707]
  教師なし環境で,事前学習した言語モデルを用いて高品質なパラフレーズを生成する訓練パイプラインを提案する。 提案手法は,タスク適応,自己スーパービジョン,動的ブロッキング(Dynamic Blocking)という新しい復号アルゴリズムから構成される。 提案手法は,Quora Question PairとParaNMTの両方のデータセット上で,最先端の性能を達成できることを示す。
  論文  参考訳（メタデータ） (2020-10-24T11:55:28Z)
• Dynamic Data Selection and Weighting for Iterative Back-Translation [116.14378571769045]
  本稿では,反復的バックトランスレーションモデルのためのカリキュラム学習戦略を提案する。 我々は、ドメイン適応、低リソース、高リソースMT設定に関するモデルを評価する。 実験の結果,提案手法は競争基準値よりも最大1.8 BLEU点の改善を達成できた。
  論文  参考訳（メタデータ） (2020-04-07T19:49:58Z)

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

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