MathForm: 知識検索と検証誘導型改良による数学自動形式化のスケーリング

要旨

自動形式化は、自然言語の数学的記述をLean 4のような機械検証可能な形式言語へ翻訳することとして一般に捉えられている。しかし、忠実な形式化には翻訳以上のものが求められる。モデルは、生成された文が元の命題の意味を保持することを保証しつつ、数学的概念をMathlibのような形式ライブラリ内の複雑な型と定義の階層に対応付けなければならない。既存のアプローチは、ライブラリ固有の知識をモデルのパラメトリック記憶に大きく依存しているため困難に直面しており、また一般的なデータ構築パイプラインは単一パス出力のフィルタリングに頼ることが多く、フィードバック駆動の修正メカニズムを欠いている。これらの課題に対処するため、我々はMathlib知識検索と検証誘導型の反復的改良を通じて検証済みトレーニングデータを構築する自動形式化フレームワークMathFormを導入する。生成前に、検索プランナーがMathlibから関連する定義と既存の形式化を収集し、形式化生成器を誘導する。生成された文は、その後、コンパイラ診断と意味的整合性フィードバックを用いて修正される。このフレームワークを用いて、多様な数学分野と出典にわたる約367,000件の検証済み例を含むLean 4データセットFormalVerseを構築した。次に、教師ありファインチューニングに続いて強化学習を行うことでMathForm-8Bを訓練した。6つのベンチマークにわたり、MathForm-8Bは構文チェック(SC)で平均Pass@8率88.06%、整合性チェック(CC)で平均Pass@8率72.37%を達成し、複数の専用32B自動形式化システムを上回った。困難なFATE-HおよびFATE-Xサブセットでは、CC合格率63%および37%を達成し、いずれの場合も最強の専用ベースラインを上回った。

English

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.