Fugu-MT 論文翻訳(概要): ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

論文の概要: 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 18:57:49.954077
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: http://creativecommons.org/licenses/by/4.0/
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データセットの両方で最先端のパフォーマンスを達成する。データセット、モデル、コードはまもなく一般公開される予定だ。

関連論文リスト

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)

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

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