論文の概要: Towards a Common Framework for Autoformalization
- arxiv url: http://arxiv.org/abs/2509.09810v1
- Date: Thu, 11 Sep 2025 19:28:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-15 16:03:07.906534
- Title: Towards a Common Framework for Autoformalization
- Title(参考訳): オートフォーマル化のための共通フレームワークを目指して
- Authors: Agnieszka Mensfelt, David Tena Cucala, Santiago Franco, Angeliki Koutsoukou-Argyraki, Vince Trencsenyi, Kostas Stathis,
- Abstract要約: オートフォーマル化(Autoformalization)は、フォーマル化の自動化を指す用語として登場した。
本稿の目的は、オートフォーマライゼーション(autoformalization)と見なせるものの-明示的または暗黙的な-インスタンスをレビューすることである。
- 参考スコア(独自算出の注目度): 2.487142846438629
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, the term has expanded beyond mathematics to describe the broader task of translating informal input into formal logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation - often without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems.
- Abstract(参考訳): 自己形式化は形式化の自動化を意味する用語として登場し、特に対話型定理証明器(英語版)を用いた数学の形式化(英語版)を指す。
その急速な開発は、ディープラーニング、特に大きな言語モデル(LLM)の進歩によって進められている。
最近では、非公式な入力を形式的な論理的表現に変換するというより広範なタスクを記述するために、数学を超えてこの用語が拡張されている。
同時に、LLMを用いて非公式言語を推論、計画、知識表現の形式表現に翻訳する研究団体が増えている。
結果として、同様の課題に対処しながらも、これらの研究領域のほぼ独立した開発は、進歩を加速できる共有方法論、ベンチマーク、理論的フレームワークに限られた機会を与えている。
本稿の目的は、自動形式化とみなせるものの-明示的または暗黙的な-インスタンスのレビューと統合されたフレームワークの提案であり、次世代AIシステムの開発を進めるために、異なる分野間の相互補完を促進することである。
関連論文リスト
- Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。
最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。
本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
論文 参考訳(メタデータ) (2025-09-02T14:16:02Z) - Autoformalization in the Era of Large Language Models: A Survey [16.503090931443687]
自己形式化は、非公式な数学的命題を検証可能な形式表現に変換する過程である。
本稿では,様々な数学領域における自己形式化の適用方法と難易度について検討する。
LLM出力の信頼性向上における自己形式化の役割について検討する。
論文 参考訳(メタデータ) (2025-05-29T14:34:54Z) - LogiDynamics: Unraveling the Dynamics of Logical Inference in Large Language Model Reasoning [74.0242521818214]
本稿では、類似推論のための制御された評価環境を導入することにより、探索的アプローチを採用する。
帰納的,帰納的,帰納的,帰納的な推論パイプラインの比較力学を解析する。
仮説選択や検証,洗練といった高度なパラダイムを考察し,論理的推論のスケールアップの可能性を明らかにする。
論文 参考訳(メタデータ) (2025-02-16T15:54:53Z) - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳(メタデータ) (2024-10-28T11:37:39Z) - Consistent Autoformalization for Constructing Mathematical Libraries [4.559523879294721]
オートフォーマル化(Autoformalization)は、自然言語で書かれた数学的内容を自動的に形式言語表現に翻訳するタスクである。
本稿では,MS-RAG(Mult-similar search augmented generation),デノナイズステップ(denoising steps),自動誤りフィードバック(Auto-SEF)による自動補正という3つのメカニズムの協調的利用を提案する。
論文 参考訳(メタデータ) (2024-10-05T15:13:22Z) - Improving Factuality and Reasoning in Language Models through Multiagent
Debate [95.10641301155232]
複数の言語モデルインスタンスが共通の最終回答に到達するために、複数のラウンドで個別の応答と推論プロセスを提案し、議論する言語応答を改善するための補完的なアプローチを提案する。
以上の結果から,本手法は様々なタスクにおける数学的・戦略的推論を著しく向上させることが示唆された。
我々のアプローチは、既存のブラックボックスモデルに直接適用され、調査するすべてのタスクに対して、同じ手順とプロンプトを使用することができる。
論文 参考訳(メタデータ) (2023-05-23T17:55:11Z) - Rationale-Augmented Ensembles in Language Models [53.45015291520658]
我々は、数発のテキスト内学習のための合理化促進策を再考する。
我々は、出力空間における合理的サンプリングを、性能を確実に向上させるキーコンポーネントとして特定する。
有理拡張アンサンブルは既存のプロンプト手法よりも正確で解釈可能な結果が得られることを示す。
論文 参考訳(メタデータ) (2022-07-02T06:20:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。