論文の概要: Improving Autoformalization Using Direct Dependency Retrieval

• arxiv url: http://arxiv.org/abs/2511.11990v1
• Date: Sat, 15 Nov 2025 02:05:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-18 14:36:23.485472
• Title: Improving Autoformalization Using Direct Dependency Retrieval
• Title（参考訳）: 直接依存検索を用いたオートフォーマライゼーションの改善
• Authors: Shaoqi Wang, Lu Yu, Chunjie Yang,
• Abstract要約: ステートメントの自動形式化は、非公式な記述を機械で検証可能な表現に変換することを目的としている。 既存の方法はしばしば文脈認識の欠如に悩まされ、形式的定義や定理の幻覚に繋がる。 文の自動形式化のためのDDR(textitDirect Dependency Retrieval)に基づく新しい検索拡張フレームワークを提案する。
• 参考スコア（独自算出の注目度）: 13.211237165431777
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: The convergence of deep learning and formal mathematics has spurred research in formal verification. Statement autoformalization, a crucial first step in this process, aims to translate informal descriptions into machine-verifiable representations but remains a significant challenge. The core difficulty lies in the fact that existing methods often suffer from a lack of contextual awareness, leading to hallucination of formal definitions and theorems. Furthermore, current retrieval-augmented approaches exhibit poor precision and recall for formal library dependency retrieval, and lack the scalability to effectively leverage ever-growing public datasets. To bridge this gap, we propose a novel retrieval-augmented framework based on DDR (\textit{Direct Dependency Retrieval}) for statement autoformalization. Our DDR method directly generates candidate library dependencies from natural language mathematical descriptions and subsequently verifies their existence within the formal library via an efficient suffix array check. Leveraging this efficient search mechanism, we constructed a dependency retrieval dataset of over 500,000 samples and fine-tuned a high-precision DDR model. Experimental results demonstrate that our DDR model significantly outperforms SOTA methods in both retrieval precision and recall. Consequently, an autoformalizer equipped with DDR shows consistent performance advantages in both single-attempt accuracy and multi-attempt stability compared to models using traditional selection-based RAG methods.
• Abstract（参考訳）: 深層学習と形式数学の収束は、形式的検証の研究を刺激している。 このプロセスにおける重要な第一歩であるステートメントの自動形式化は、非公式な記述を機械で検証可能な表現に変換することを目的としているが、依然として重要な課題である。 主要な難しさは、既存の方法が文脈的認識の欠如に悩まされることがしばしばあり、形式的定義や定理の幻覚につながるという事実にある。 さらに、現在の検索強化アプローチでは、形式的なライブラリ依存検索の精度やリコールが低く、成長を続けるパブリックデータセットを効果的に活用するスケーラビリティが欠如している。 このギャップを埋めるために、文の自動形式化のためのDDR(\textit{Direct Dependency Retrieval})に基づく新しい検索拡張フレームワークを提案する。 DDR法は,自然言語の数学的記述から直接ライブラリ依存関係を生成し,その後,効率的な接尾辞配列チェックによって形式ライブラリ内に存在することを検証する。 この効率的な探索機構を活用し,50万以上のサンプルの依存関係検索データセットを構築し,高精度DDRモデルを微調整した。 実験の結果,DDRモデルは,検索精度とリコール精度の両方でSOTA法より有意に優れていた。 その結果、DDRを内蔵したオートフォーマライザは、従来の選択型RAG法と比較すると、単対流精度と多対流安定性の両方において一貫した性能上の優位性を示した。

関連論文リスト

• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• Large Reasoning Embedding Models: Towards Next-Generation Dense Retrieval Paradigm [16.78399933831573]
  本稿では、推論過程を表現学習に統合するLarge Reasoning Embedding Model(LREM)を提案する。 難解なクエリに対して、LREMはまず、元のクエリの深い理解を達成するために推論を行い、その後、検索のための推論拡張クエリ埋め込みを生成する。 この推論プロセスは、元のクエリとターゲットアイテム間のセマンティックギャップを効果的にブリッジし、検索精度を大幅に向上させる。
  論文  参考訳（メタデータ） (2025-10-16T05:37:39Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  線形木探索はLarge Language Model (LLM) 研究の基盤となっている。 本稿では,検索アルゴリズムを3つのコアコンポーネントに分解する統合フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-11T03:29:18Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Lightweight and Direct Document Relevance Optimization for Generative Information Retrieval [49.669503570350166]
  生成情報検索(GenIR)は、文書識別子(ドシデント)生成タスクとして文書検索を定式化する有望なニューラル検索パラダイムである。 既存のGenIRモデルはトークンレベルのミスアライメントに悩まされており、次のトークンを予測するためにトレーニングされたモデルは、ドキュメントレベルの関連性を効果的にキャプチャできないことが多い。 本稿では,トークンレベルのドシデント生成と文書レベルのドシデンス推定をペアのランク付けによる直接最適化により整合するダイレクトドキュメントレバレンス最適化(DDRO)を提案する。
  論文  参考訳（メタデータ） (2025-04-07T15:27:37Z)
• Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
  本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。 このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。 実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
  論文  参考訳（メタデータ） (2025-01-21T06:32:25Z)
• Distributional Robustness and Regularization in Reinforcement Learning [62.23012916708608]
  経験値関数の新しい正規化器を導入し、ワッサーシュタイン分布のロバストな値関数を下限とすることを示す。 強化学習における$textitexternalな不確実性に対処するための実用的なツールとして正規化を使用することを提案する。
  論文  参考訳（メタデータ） (2020-03-05T19:56:23Z)

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

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