論文の概要: Autoformalizer with Tool Feedback

• arxiv url: http://arxiv.org/abs/2510.06857v1
• Date: Wed, 08 Oct 2025 10:25:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-09 16:41:20.423492
• Title: Autoformalizer with Tool Feedback
• Title（参考訳）: ツールフィードバックによるオートフォーマライザ
• Authors: Qi Guo, Jianing Wang, Jianfei Zhang, Deyang Kong, Xiangzhou Huang, Xiangyu Xi, Wei Wang, Jingang Wang, Xunliang Cai, Shikun Zhang, Wei Ye,
• Abstract要約: 自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
• 参考スコア（独自算出の注目度）: 52.334957386319864
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements. Efforts in recent work shift from directly prompting large language models to training an end-to-end formalizer model from scratch, achieving remarkable advancements. However, existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency. To address this issue, we propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process. By integrating Lean 4 compilers for syntax corrections and employing a multi-LLMs-as-judge approach for consistency validation, the model is able to adaptively refine generated statements according to the tool feedback, enhancing both syntactic validity and semantic consistency. The training of ATF involves a cold-start phase on synthetic tool-calling data, an expert iteration phase to improve formalization capabilities, and Direct Preference Optimization to alleviate ineffective revisions. Experimental results show that ATF markedly outperforms a range of baseline formalizer models, with its superior performance further validated by human evaluations. Subsequent analysis reveals that ATF demonstrates excellent inference scaling properties. Moreover, we open-source Numina-ATF, a dataset containing 750K synthetic formal statements to facilitate advancements in autoformalization and ATP research.
• Abstract（参考訳）: 自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 最近の作業では、大きな言語モデルを直接的に促すことから、エンドツーエンドのフォーミュラモデルをゼロからトレーニングすることへの取り組みが、目覚ましい進歩を遂げています。 しかし、既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 この問題に対処するため,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。 構文修正のためにLean 4コンパイラを統合し、一貫性検証のためにマルチLLMs-as-judgeアプローチを採用することで、このモデルは、ツールフィードバックに従って生成されたステートメントを適応的に洗練し、構文的妥当性とセマンティック一貫性の両方を向上させることができる。 ATFのトレーニングには、合成ツールコールデータに対するコールドスタートフェーズ、フォーマル化機能を改善するためのエキスパートイテレーションフェーズ、非効率なリビジョンを緩和するためのダイレクトプレフレクション最適化が含まれる。 実験結果から,ATFはベースラインフォーミュラモデルよりも優れた性能を示し,その性能は人体評価によりさらに向上した。 その後の解析により、ATFは優れた推論スケーリング特性を示すことが明らかとなった。 さらに, 750K の合成形式文を含むデータセットである Numina-ATF をオープンソースとして公開した。

関連論文リスト

• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
  論文  参考訳（メタデータ） (2025-09-28T06:32:14Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
  論文  参考訳（メタデータ） (2025-07-07T10:30:05Z)
• Unveiling the Flaws: Exploring Imperfections in Synthetic Data and Mitigation Strategies for Large Language Models [89.88010750772413]
  大規模言語モデル(LLM)の学習における高品質なデータ不足問題に対する解決法として,合成データを提案する。 我々の研究は、Q-A(Q-A)ペア、一般的な合成データに関連するこれらの特定の欠陥を掘り下げ、これらの欠陥を軽減するための未学習技術に基づく方法を提案する。 我々の研究は、より堅牢で効率的なLLMトレーニングを促進することを目的として、合成データの効果的な利用に関する重要な洞察を得た。
  論文  参考訳（メタデータ） (2024-06-18T08:38:59Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Prompting to Distill: Boosting Data-Free Knowledge Distillation via Reinforced Prompt [52.6946016535059]
  データフリー知識蒸留(DFKD)は、元のトレーニングデータの依存をなくし、知識蒸留を行う。 本稿では,PmptDFD(PromptDFD)と呼ばれるプロンプトベースの手法を提案する。 本実験で示すように, 本手法は, 合成品質を大幅に向上し, 蒸留性能を著しく向上させる。
  論文  参考訳（メタデータ） (2022-05-16T08:56:53Z)
• NoiER: An Approach for Training more Reliable Fine-TunedDownstream Task Models [54.184609286094044]
  補助モデルと付加データなしで問題を解くための学習パラダイムとして,ノイズエントロピー正規化(NoiER)を提案する。 提案手法は,従来の微調整モデルと比較して平均55%改善した。
  論文  参考訳（メタデータ） (2021-08-29T06:58:28Z)

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

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