論文の概要: 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で入手できる。
関連論文リスト
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs [32.234133057592935]
Hermesはツール支援エージェントで、リーンシステムにおける検証段階と非公式な推論をインターリーブする。
パラメータスケールの異なる LLM を用いて,Hermes を4つの挑戦的数学的推論ベンチマークで評価する。
論文 参考訳（メタデータ） (2025-11-24T04:50:18Z) - CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
$rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。
それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
論文 参考訳（メタデータ） (2025-05-20T05:15:47Z) - 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) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。
LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。
我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
論文 参考訳（メタデータ） (2023-10-01T12:47:59Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。