論文の概要: 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トランスレータを開発した。 データセット、モデル、コードはまもなく一般公開される予定だ。

関連論文リスト

• Learning Like Humans: Resource-Efficient Federated Fine-Tuning through Cognitive Developmental Stages [10.715400075722004]
  フェデレートされた微調整により、Large Language Models(LLM)は、データプライバシを保持しながら、下流タスクに適応することができる。 本稿では,認知発達にインスパイアされた資源効率の高い手法であるDevFTを紹介する。 DevFTは微調整プロセスを発達段階に分解し、各サブモデルをパラメータ容量の増大で最適化する。
  論文  参考訳（メタデータ） (2025-07-31T09:36:43Z)
• KIT's Low-resource Speech Translation Systems for IWSLT2025: System Enhancement with Synthetic Data and Model Regularization [57.08591486199925]
  本稿では,KIT の低リソーストラック IWSLT 2025 への提出について述べる。 ケースドシステムとエンド・ツー・エンド(E2E)音声翻訳システムを開発した。 事前訓練されたモデルに基づいて、リソースを効率的に活用するためのさまざまな戦略でシステムを微調整します。
  論文  参考訳（メタデータ） (2025-05-26T08:38:02Z)
• 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)
• Align to Structure: Aligning Large Language Models with Structural Information [26.960069076925386]
  本研究では,大規模言語モデルと人間のような談話構造を整合させて長文生成を向上する構造アライメントを提案する。 提案手法では,人間の文章に対する言論的特質に基づいて,詳細なトークンレベルの報酬を割り当てる。
  論文  参考訳（メタデータ） (2025-04-04T17:40:04Z)
• Scaling Laws of Synthetic Data for Language Models [132.67350443447611]
  プレトレーニングコーパスを多種多様な高品質な合成データセットに変換するスケーラブルなフレームワークであるSynthLLMを紹介した。 提案手法は,グラフアルゴリズムを用いて複数の文書にまたがるハイレベルな概念を自動的に抽出し,再結合することで実現している。
  論文  参考訳（メタデータ） (2025-03-25T11:07:12Z)
• A Survey on Post-training of Large Language Models [185.51013463503946]
  大規模言語モデル(LLM)は、自然言語処理を根本的に変革し、会話システムから科学的探索まで、さまざまな領域で欠かせないものにしている。 これらの課題は、制限された推論能力、倫理的不確実性、最適なドメイン固有のパフォーマンスといった欠点に対処するために、先進的な訓練後言語モデル(PoLM)を必要とする。 本稿では,タスク固有の精度を向上するファインチューニング,倫理的コヒーレンスと人間の嗜好との整合性を保証するアライメント,報酬設計の課題によらず多段階の推論を進める推論,統合と適応の5つのパラダイムを体系的に追跡したPoLMの総合的な調査について述べる。
  論文  参考訳（メタデータ） (2025-03-08T05:41:42Z)
• Enhancing RWKV-based Language Models for Long-Sequence Text Generation [0.0]
  本稿では、長文言語モデリングを改善するための適応時間ゲーティング機構を備えた拡張RWKVアーキテクチャを提案する。 本研究では,(1)グローバルコヒーレンスを保ちながら局所的な統語パターンを捉える位置認識畳み込みシフト演算子,(2)知識間の情報の流れを動的に制御する神経伝達情報ルーティング機構を提案する。
  論文  参考訳（メタデータ） (2025-02-21T14:18:18Z)
• 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)
• Generation of Asset Administration Shell with Large Language Model Agents: Toward Semantic Interoperability in Digital Twins in the Context of Industry 4.0 [0.6749750044497732]
  本研究は,デジタル双生児におけるセマンティック・インターオペラビリティを実現するための新しいアプローチを提案する。 業界 4.0 におけるデジタル双対モデルとしてアセット管理シェル (AAS) の作成を支援する。
  論文  参考訳（メタデータ） (2024-03-25T21:37:30Z)
• Contextualization Distillation from Large Language Model for Knowledge Graph Completion [51.126166442122546]
  我々は、差別的かつ生成的なKGCフレームワークと互換性のあるプラグイン・アンド・プレイ方式であるContextualization Distillation戦略を導入する。 提案手法は,大規模言語モデルに対して,コンパクトで構造的な三重項を文脈に富んだセグメントに変換するように指示することから始まる。 多様なデータセットとKGC技術にわたる総合的な評価は、我々のアプローチの有効性と適応性を強調している。
  論文  参考訳（メタデータ） (2024-01-28T08:56:49Z)
• 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)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Exploiting Asymmetry for Synthetic Training Data Generation: SynthIE and the Case of Information Extraction [28.51694365908817]
  本研究は,大規模言語モデルでは直接解けないタスクに対しても,有用なデータを合成的に生成できることを示唆する。 我々は、1.8Mのデータポイントのデータセットを合成的に生成し、人間の評価において既存のデータセットと比較して優れた品質を確立する。
  論文  参考訳（メタデータ） (2023-03-07T18:48:55Z)
• Improving Distantly Supervised Relation Extraction by Natural Language Inference [9.181270251524866]
  本稿では,既存の知識ベースから遠ざかる監視と,事前学習した言語モデルから他のタスクへ間接的に監督するDSRE-NLIフレームワークを提案する。 DSRE-NLIは、半自動的関係言語化(SARV)機構により、市販の自然言語推論(NLI)エンジンをエネルギ化し、間接的な監視を提供する。 2つのシンプルで効果的なデータ統合戦略により、トレーニングデータの質が大幅に向上する。
  論文  参考訳（メタデータ） (2022-07-31T02:48:34Z)
• The USYD-JD Speech Translation System for IWSLT 2021 [85.64797317290349]
  本稿では,シドニー大学とJDが共同でIWSLT 2021低リソース音声翻訳タスクを提出したことを述べる。 私たちは、公式に提供されたASRとMTデータセットでモデルをトレーニングしました。 翻訳性能の向上を目的として, バック翻訳, 知識蒸留, 多機能再構成, トランスダクティブファインタニングなど, 最新の効果的な手法について検討した。
  論文  参考訳（メタデータ） (2021-07-24T09:53:34Z)

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

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