論文の概要: M2F: Automated Formalization of Mathematical Literature at Scale

• arxiv url: http://arxiv.org/abs/2602.17016v1
• Date: Thu, 19 Feb 2026 02:25:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-20 15:21:28.603463
• Title: M2F: Automated Formalization of Mathematical Literature at Scale
• Title（参考訳）: M2F: 大規模数学文学の形式化の自動化
• Authors: Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen,
• Abstract要約: M2F(Math-to-Formal)は、リーンにおけるエンドツーエンドのプロジェクトスケールの自動形式化のための最初のエージェントフレームワークです。 約3週間で、M2Fは479ページの教科書から153,853行のリーンライブラリに変換する。 これは、通常数ヶ月または数年の専門的な努力を必要とするペースで教科書スケールの形式化を表す。
• 参考スコア（独自算出の注目度）: 24.360952996585045
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.
• Abstract（参考訳）: 数学の自動形式化は機械的な検証を可能にするが、孤立定理や短いスニペットに限られる。 教科書や研究論文へのスケーリングは、ファイル間の依存関係の管理、インポートの解決、プロジェクト全体がエンドツーエンドのコンパイルを確実にする必要があるため、ほとんど適応していない。 M2F(Math-to-Formal)は、リーンにおけるエンドツーエンドのプロジェクトスケールの自動形式化のための最初のエージェントフレームワークです。 フレームワークは2段階で動作する。 ステートメントコンパイルステージは、ドキュメントをアトミックブロックに分割し、推論された依存関係を通じて命令し、プロジェクトがコンパイルされるまで宣言スケルトンを修復し、プレースホルダーが証明できる。 証明修復段階は、ゴール条件の局所的な編集を用いて、固定された署名の下でこれらの穴を閉じる。 どちらの段階も、M2Fは検証結果をループに保持し、ツールチェーンフィードバックが改善を確認する場合にのみ編集をコミットする。 約3週間で、M2Fは、長い形式の数学的ソースを、実際の分析と凸解析に関する教科書479ページから153,853行のプロジェクトスケールのLeanライブラリに変換する。 これは、通常数ヶ月または数年の専門的な努力を必要とするペースで教科書スケールの形式化を表す。 FATE-H では 96 % の証明成功 (vs) を達成する。 は、強いベースラインに対して80\%$である。 これらの結果は、数学文学の実用的かつ大規模な自動形式化が到達範囲内にあることを示している。 私たちのランニングから生成されたリーンコードはhttps://github.com/optsuite/ReasBook.git.comで入手できる。

関連論文リスト

• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。 Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
  論文  参考訳（メタデータ） (2025-04-27T05:04:02Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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