論文の概要: MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

• arxiv url: http://arxiv.org/abs/2608.14221v1
• Date: Fri, 14 Aug 2026 11:51:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-17 20:14:29.370995
• Title: MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
• Title（参考訳）: MathForm:知識検索と検証ガイドによる数学的オートフォーマル化のスケーリング
• Abstract要約: 検証されたトレーニングデータを構築するための自動形式化フレームワークであるMathFormを紹介する。 約367Kの検証例を含むLean 4データセットであるFormalVerseを構築します。 MathForm-8Bは、Syntax Checkで88.06%、Consistency Checkで72.37%の平均パス@8レートを達成した。
• 参考スコア（独自算出の注目度）: 28.062085562858098
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.
• Abstract（参考訳）: 自動形式化は、自然言語の数学的ステートメントをLean 4のような機械で検証可能な形式言語に翻訳する、という枠組みが一般的である。 しかし、忠実な形式化は翻訳以上のものを必要とする。 モデルは、Mathlibのような形式ライブラリの型と定義の複雑な階層に数学的概念をマッピングし、生成したステートメントが元命題の意味を保存することを保証する必要がある。 既存のアプローチは、ライブラリ固有の知識のためにモデルのパラメトリックメモリに大きく依存しているのに対して、一般的なデータ構築パイプラインはシングルパス出力をフィルタリングし、フィードバック駆動リビジョンのメカニズムを欠いている。 これらの課題に対処するために、Mathlibの知識検索と検証誘導反復改善を通じて、検証済みのトレーニングデータを構築するための自動形式化フレームワークMathFormを紹介した。 生成前に、検索プランナーは、Mathlibから関連する定義と既存の形式を収集し、形式化ジェネレータを誘導する。 生成されたステートメントは、コンパイラの診断とセマンティック一貫性フィードバックを使って修正される。 このフレームワークを使用して、さまざまな数学的ドメインやソースにわたる約367万の検証済みサンプルを含む、Lean 4データセットであるFormalVerseを構築します。 次に、教師付き微調整と強化学習によりMathForm-8Bを訓練する。 6つのベンチマークで、MathForm-8Bは、Syntax Check (SC) で88.06%、Consistency Check (CC) で72.37%の平均パス@86%を達成する。 挑戦的なFATE-HおよびFATE-Xサブセットでは、CCパス率は63%と37%に達し、どちらのケースでも最強の特殊ベースラインを超えている。

関連論文リスト

• AMTFV: Agentic Mathematical Tool-Flow Verification for LLM Self-Correction [58.27846292449026]
  大規模言語モデルは強力な数学的問題解決能力を示してきたが、その答えを確実に検証することは依然として困難である。 本稿では,具体的な実行から検証モデリングを分離するAMTFV(Agentic Mathematical Tool-Flow Verification)を提案する。 AMTFVをDeepSeek, GPT, Geminiの7つのモデル構成を持つ難解な数学的推論データセットで評価した。
  論文  参考訳（メタデータ） (2026-07-31T15:42:00Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-30T05:05:03Z)
• Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance [0.3624700141426058]
  コーディングエージェントはLean 4で高度な数学教科書全体を形式化できます。 本稿では,コンパイラを超えてエージェント生成形式の品質を評価するためのフレームワークを提案する。 以上の結果から,コンパイルベースのメトリクスは形式化品質を大幅に上回っていることが示唆された。
  論文  参考訳（メタデータ） (2026-06-12T00:45:42Z)
• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。 本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
  論文  参考訳（メタデータ） (2026-03-13T07:39:47Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
  論文  参考訳（メタデータ） (2025-10-12T21:42:04Z)
• 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)
• FMC: Formalization of Natural Language Mathematical Competition Problems [12.86616278136374]
  本稿では,誤りフィードバックを伴う大規模言語モデルに基づく自動形式化パイプラインを提案する。 Olympiadレベルのデータセットを、自然言語の問題をリーンの形式化と整合させます。 少数ショット学習,エラーフィードバック,サンプリング数の増加により,自動形式化プロセスが促進されることを示す。
  論文  参考訳（メタデータ） (2025-07-15T12:52:47Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。 創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)

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

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