論文の概要: DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

• arxiv url: http://arxiv.org/abs/2510.10815v2
• Date: Tue, 14 Oct 2025 10:15:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-15 16:45:44.451602
• Title: DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems
• Title（参考訳）: DRIFT:分解、検索、イラスト、そして形式化理論
• Authors: Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras,
• Abstract要約: DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
• 参考スコア（独自算出の注目度）: 14.568293842955065
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean. Current retrieval-augmented autoformalization methods query external libraries using the informal statement directly, but overlook a fundamental limitation: informal mathematical statements are often complex and offer limited context on the underlying math concepts. To address this, we introduce DRIFT, a novel framework that enables LLMs to decompose informal mathematical statements into smaller, more tractable ''sub-components''. This facilitates targeted retrieval of premises from mathematical libraries such as Mathlib. Additionally, DRIFT retrieves illustrative theorems to help models use premises more effectively in formalization tasks. We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval, nearly doubling the F1 score compared to the DPR baseline on ProofNet. Notably, DRIFT demonstrates strong performance on the out-of-distribution ConNF benchmark, with BEq+@10 improvements of 37.14% and 42.25% using GPT-4.1 and DeepSeek-V3.1, respectively. Our analysis shows that retrieval effectiveness in mathematical autoformalization depends heavily on model-specific knowledge boundaries, highlighting the need for adaptive retrieval strategies aligned with each model's capabilities.
• Abstract（参考訳）: 定理証明のための数学的ステートメントの形式化を自動化することは、Large Language Models (LLMs) にとって大きな課題である。 LLMは、必要不可欠な数学的知識とそれに対応する形式的表現をリーンのような言語で識別し、利用するのに苦労している。 現在の検索拡張自動形式化手法は、非公式な文を使って外部ライブラリを直接クエリするが、基本的な制限を見落としている: 非公式な数学的ステートメントはしばしば複雑で、基礎となる数学概念について限定的な文脈を提供する。 そこで本稿では, LLM をより小さく, より扱いやすい ''サブコンポーネント' に分解可能な,新しいフレームワーク DRIFT を紹介する。 これは、Mathlibのような数学的ライブラリからの前提の検索を容易にする。 さらに、DRIFTは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、図解定理を回収する。 我々は様々なベンチマーク(ProofNet、ConNF、MiniF2F-test)でDRIFTを評価し、ProofNetのDPRベースラインと比較してF1スコアをほぼ倍増させ、常に前提検索を改善することを発見した。 DRIFTは、それぞれGPT-4.1とDeepSeek-V3.1を使用してBEq+@10の改善を37.14%、42.25%に改善した。 解析の結果,数学的自己形式化における検索の有効性は,モデル固有の知識境界に大きく依存しており,各モデルの能力に適合した適応的検索戦略の必要性が示唆された。

関連論文リスト

• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMFは概念駆動のRetrieval-Augmented Mathematical Formalizationフレームワークである。 概念定義知識ベースをMathlib4から自動構築するフレームワークを提案する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合できることが示されている。
  論文  参考訳（メタデータ） (2025-08-09T10:54:25Z)
• SPaRFT: Self-Paced Reinforcement Fine-Tuning for Large Language Models [51.74498855100541]
  大規模言語モデル(LLM)は、強化学習(RL)による微調整時に強い推論能力を示す。 トレーニング対象のモデルの性能に基づいて,効率的な学習を可能にする自己評価学習フレームワークである textbfSPaRFT を提案する。
  論文  参考訳（メタデータ） (2025-08-07T03:50:48Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
  本研究では,Mathlibから抽出したデータを利用して,軽量で効果的な前提条件検索モデルを訓練する手法を提案する。 このモデルは、微粒な類似性計算法と再ランクモジュールを応用した、対照的な学習フレームワークで学習される。 実験により,本モデルが既存のベースラインより優れており,計算負荷の低減を図りながら高い精度を実現していることが示された。
  論文  参考訳（メタデータ） (2025-01-21T06:32:25Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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