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

• arxiv url: http://arxiv.org/abs/2502.05567v2
• Date: Mon, 19 May 2025 04:17:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-20 14:57:10.439496
• Title: ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data
• Title（参考訳）: ATLAS: データのリフティング、拡張、合成による自己形式化理論
• Authors: Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, Tao Luo,
• Abstract要約: ATLASは、定理文の大規模かつ高品質な並列コーパスを生成するために設計された、新しいデータ生成フレームワークである。 我々は,117kの定理文からなる学部レベルのデータセットを構築し,HALALDトランスレータとKimina-Autoformalizerの両方に対して統計的に有意な改善を示すATLASトランスレータを開発した。 データセット、モデル、コードはまもなく一般公開される予定だ。
• 参考スコア（独自算出の注目度）: 14.409949582947435
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization, the automatic translation of mathematical content from natural language into machine-verifiable formal languages, has seen significant progress driven by advances in large language models (LLMs). Nonetheless, a primary barrier to further improvements is the limited availability of parallel corpora that map informal mathematical text to its formal counterpart. To address this limitation, we propose ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data), a novel data generation framework designed to produce large-scale, high-quality parallel corpora of theorem statements. Distinct from prior approaches, ATLAS begins with a concept repository, accelerates the improvement of student model through expert iteration combined with knowledge distillation, and introduces two novel augmentation strategies that exploit the structural characteristics of formal languages. With the proposed ATLAS running for 10 iterations, we construct an undergraduate-level dataset comprising 117k theorem statements and develop ATLAS Translator, which demonstrates statistically significant improvements over both the HERALD Translator and the Kimina-Autoformalizer across all benchmarks ($p<0.05$, two-sided t-test), achieving a new state of the art. The datasets, model, and code will be released to the public soon.
• Abstract（参考訳）: 自然言語から機械で検証可能な形式言語への数学的内容の自動翻訳であるオートフォーマル化は、大規模言語モデル(LLM)の進歩によって大きく進歩している。 それでも、さらなる改善のための主要な障壁は、形式的な数学的テキストを形式的なテキストにマッピングする並列コーパスの可用性が限られていることである。 この制限に対処するため、我々は、定理文の大規模かつ高品質な並列コーパスを生成するために設計された新しいデータ生成フレームワークであるATLAS(Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data)を提案する。 従来のアプローチとは対照的に、ATLASは概念リポジトリから始まり、知識蒸留と専門家の反復によって学生モデルの改善を加速し、形式言語の構造的特性を利用する2つの新しい拡張戦略を導入する。 提案したATLASを10回のイテレーションで実行することにより,117kの定理文からなる学部レベルのデータセットを構築し,HERALDトランスレータとKimina-Autoformalizerの両ベンチマーク(p<0.05$, two-sided t-test)に対して統計的に有意な改善を示すATLASトランスレータを開発した。 データセット、モデル、コードはまもなく一般公開される予定だ。

関連論文リスト

• A Large-scale Class-level Benchmark Dataset for Code Generation with LLMs [3.458772578520879]
  我々は、13,174ドルのオープンソースのプロジェクトから収集した大規模なPythonクラスレベルのデータセットを紹介します。 データセットには842,000以上のクラススケルトンが含まれている。 抽出されたクラススケルトンを,全クラス実装を生成するためのGPT-4のプロンプトとして使用する。 その結果, LLM 生成クラスは, 平均 ROUGE@L, BLEU, TSED スコア0.80, 0.59, 0.73 と強い語彙的および構造的類似性を示した。
  論文  参考訳（メタデータ） (2025-04-22T03:33:57Z)
• Fine-tuning a Large Language Model for Automating Computational Fluid Dynamics Simulations [11.902947290205645]
  大規模言語モデル(LLM)は高度な科学計算を持ち、CFDでの使用は自動化されている。 ドメイン固有LLM適応に着目した新しいアプローチを提案する。 マルチエージェントフレームワークはプロセスをオーケストレーションし、入力を自律的に検証し、構成を生成し、シミュレーションを実行し、エラーを修正する。
  論文  参考訳（メタデータ） (2025-04-13T14:35:30Z)
• Scaling Laws of Synthetic Data for Language Models [132.67350443447611]
  プレトレーニングコーパスを多種多様な高品質な合成データセットに変換するスケーラブルなフレームワークであるSynthLLMを紹介した。 提案手法は,グラフアルゴリズムを用いて複数の文書にまたがるハイレベルな概念を自動的に抽出し,再結合することで実現している。
  論文  参考訳（メタデータ） (2025-03-25T11:07:12Z)
• MAmmoTH-VL: Eliciting Multimodal Reasoning with Instruction Tuning at Scale [66.73529246309033]
  MLLM(Multimodal large language model)は、多モーダルタスクにおいて大きな可能性を秘めている。 既存の命令チューニングデータセットは、中間的合理性のないフレーズレベルの答えのみを提供する。 そこで本研究では,大規模マルチモーダル・インストラクション・チューニング・データセットを構築するためのスケーラブルで費用対効果の高い手法を提案する。
  論文  参考訳（メタデータ） (2024-12-06T18:14:24Z)
• Building Math Agents with Multi-Turn Iterative Preference Learning [56.71330214021884]
  本稿では,モデル性能をさらに向上させるために,補完的な直接選好学習手法について検討する。 既存の直接選好学習アルゴリズムは、もともとシングルターンチャットタスク用に設計されている。 この文脈に合わせたマルチターン直接選好学習フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-09-04T02:41:04Z)
• 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)
• 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)
• TarGEN: Targeted Data Generation with Large Language Models [51.87504111286201]
  TarGENは、高品質な合成データセットを生成するための、多段階のプロンプト戦略である。 我々は,LLMが不正確なラベル付きインスタンスを修正できるようにする自己補正法により,TarGENを増強する。 合成データセットを元のデータセットと比較した包括的な分析により、データセットの複雑さと多様性の類似または高いレベルが明らかになる。
  論文  参考訳（メタデータ） (2023-10-27T03:32:17Z)
• 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)

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

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