論文の概要: Autoformalization in the Era of Large Language Models: A Survey

• arxiv url: http://arxiv.org/abs/2505.23486v1
• Date: Thu, 29 May 2025 14:34:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-30 18:14:07.904301
• Title: Autoformalization in the Era of Large Language Models: A Survey
• Title（参考訳）: 大規模言語モデルの時代におけるオートフォーマル化:サーベイ
• Authors: Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, Tiancheng Zhang,
• Abstract要約: 自己形式化は、非公式な数学的命題を検証可能な形式表現に変換する過程である。 本稿では,様々な数学領域における自己形式化の適用方法と難易度について検討する。 LLM出力の信頼性向上における自己形式化の役割について検討する。
• 参考スコア（独自算出の注目度）: 16.503090931443687
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field.
• Abstract（参考訳）: 非公式な数学的命題を検証可能な形式表現に変換する過程であるオートフォーマル化(Autoformalization)は、自動定理証明における基礎的なタスクであり、理論と応用両方の領域における数学の使用に関する新しい視点を提供する。 人工知能、特に大規模言語モデル(LLM)の急速な進歩によって、この分野は大幅に成長し、新たな機会とユニークな課題がもたらされた。 本稿では, 数学とLLMの両面から, 近年の自己形式化の進歩を概観する。 本稿では,データ前処理からモデル設計,評価に至るまで,様々な数学的領域や難易度にオートフォーマル化を適用する方法について検討し,エンドツーエンドのワークフローを解析する。 さらに, LLM出力の信頼性向上における自己形式化の役割について考察し, LLM出力の信頼性と推論能力の向上の可能性を明らかにする。 最後に、現在の研究を支援する主要なオープンソースモデルとデータセットを要約し、オープンな課題とこの分野の将来的な方向性について論じる。

関連論文リスト

• ModelingAgent: Bridging LLMs and Mathematical Modeling for Real-World Challenges [72.19809898215857]
  ModelingBenchは、様々な領域にわたる数学モデリングの競争から、現実に着想を得たオープンエンドの問題を特徴付ける新しいベンチマークである。 これらのタスクには、自然言語を形式的な数学的定式化に翻訳し、適切なツールを適用し、構造化された防御可能なレポートを生成する必要がある。 ツール使用をコーディネートするマルチエージェントフレームワークである ModelingAgent も紹介します。
  論文  参考訳（メタデータ） (2025-05-21T03:33:23Z)
• Large Language Models Post-training: Surveying Techniques from Alignment to Reasoning [185.51013463503946]
  大規模言語モデル(LLM)は、自然言語処理を根本的に変革し、会話システムから科学的探索まで、さまざまな領域で欠かせないものにしている。 これらの課題は、制限された推論能力、倫理的不確実性、最適なドメイン固有のパフォーマンスといった欠点に対処するために、先進的な訓練後言語モデル(PoLM)を必要とする。 本稿では,タスク固有の精度を向上するファインチューニング,倫理的コヒーレンスと人間の嗜好との整合性を保証するアライメント,報酬設計の課題によらず多段階の推論を進める推論,統合と適応の5つのパラダイムを体系的に追跡したPoLMの総合的な調査について述べる。
  論文  参考訳（メタデータ） (2025-03-08T05:41:42Z)
• An Overview of Large Language Models for Statisticians [109.38601458831545]
  大規模言語モデル(LLM)は人工知能(AI)の変換ツールとして登場した。 本稿では, 統計学者がLLMの開発に重要な貢献できる可能性について考察する。 我々は不確実性定量化、解釈可能性、公正性、プライバシー、透かし、モデル適応といった問題に焦点を当てる。
  論文  参考訳（メタデータ） (2025-02-25T03:40:36Z)
• Large Language Model for Qualitative Research -- A Systematic Mapping Study [3.302912592091359]
  先進的な生成AIを駆使した大規模言語モデル(LLM)がトランスフォーメーションツールとして登場した。 本研究は, LLMを用いた定性的研究に関する文献を体系的にマッピングする。 LLMは様々な分野にまたがって利用されており、プロセスの自動化の可能性を示している。
  論文  参考訳（メタデータ） (2024-11-18T21:28:00Z)
• Unleashing LLM Reasoning Capability via Scalable Question Synthesis from Scratch [54.12139707822201]
  本稿では,新しい,スケーラブルで費用対効果の高いデータ合成手法であるScaleQuestを提案する。 スクラッチから多様な質問を生成することで、100万の問題解決ペアのデータセットを生成します。 私たちの実験では、データに基づいてトレーニングされたモデルが、既存のオープンソースデータセットより優れています。
  論文  参考訳（メタデータ） (2024-10-24T12:42:04Z)
• Solution-oriented Agent-based Models Generation with Verifier-assisted Iterative In-context Learning [10.67134969207797]
  エージェントベースのモデル(ABM)は、仮説的な解決策やポリシーの提案と検証に不可欠なパラダイムである。 大きな言語モデル(LLM)は、ドメイン間の知識とプログラミング能力をカプセル化することで、このプロセスの難しさを軽減できる可能性がある。 SAGEは、ターゲット問題に対する自動モデリングおよびソリューション生成のために設計された、汎用的なソリューション指向のABM生成フレームワークである。
  論文  参考訳（メタデータ） (2024-02-04T07:59:06Z)
• FinGPT: Instruction Tuning Benchmark for Open-Source Large Language Models in Financial Datasets [9.714447724811842]
  本稿では,オープンソースの大規模言語モデルに対して,インストラクションチューニングパラダイムに固有のアプローチを導入する。 私たちは、オープンソースのモデルの相互運用性に乗じて、シームレスで透過的な統合を確保します。 本稿では,エンドツーエンドのトレーニングとテストのためのベンチマーク手法を提案し,費用対効果を生かした。
  論文  参考訳（メタデータ） (2023-10-07T12:52:58Z)
• Model Reprogramming: Resource-Efficient Cross-Domain Machine Learning [65.268245109828]
  視覚、言語、音声などのデータに富む領域では、ディープラーニングが高性能なタスク固有モデルを提供するのが一般的である。 リソース制限されたドメインでのディープラーニングは、(i)限られたデータ、(ii)制約付きモデル開発コスト、(iii)効果的な微調整のための適切な事前学習モデルの欠如など、多くの課題に直面している。 モデル再プログラミングは、ソースドメインから十分に訓練されたモデルを再利用して、モデル微調整なしでターゲットドメインのタスクを解くことで、リソース効率のよいクロスドメイン機械学習を可能にする。
  論文  参考訳（メタデータ） (2022-02-22T02:33:54Z)

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

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