現代数学と人工知能の交差分野において、機械が正確に「読解」し、形式的検証を通じて数学定理を扱うことが、汎用人工知能（AGI）の核心的な課題の一つです。OpenBMBチームは近日、新たな数学自動形式化オープンソースフレームワーク、データセットおよびモデルであるMathFormを正式にオープンソース化しました。

長年にわたって、数学の形式化（例えばLean4言語に基づくもの）は、自然言語をコードに翻訳するだけでなく、より厳密なモデルがMathlibライブラリ内の正しい型や定義にそれぞれの数学的概念を正確にマッピングする必要があります。業界ではよくある問題として、形式化された文がコンパイラによって正常にコンパイルされても、意味的に元の問題を正確に記述できないことがあります。

image.png

この難題を克服するために、MathFormフレームワークは検索拡張と検証誘導のデータ構築メカニズムを革新的に導入しました。そのコアロジックは、システムがまず検索プランナーを通じて文に必要なMathlibの定義と既存の形式化モデルを抽出することです。その後、ジェネレーターはLeanコンパイラの診断結果および意味的一貫性フィードバックに基づいて、出力内容を最大で3ラウンド修正することで、コード品質と数学的意味の一貫性を大幅に確保します。

データとモデルの面では、OpenBMBは36万7千以上の検証済みLean4例を含むFormalVerseデータセットを発表しました。これは多様な数学の分野とソースをカバーしています。実験結果によると、同等のトレーニング予算と初期条件の下で、FormalVerseでトレーニングされたモデルの整合性チェック率は60.32％に達し、FineLeanCorpusの46.53％やNuminaMath-LEANの41.49％を大きく上回っています。

主要成果の一つとして、MathForm-8Bモデルは6つのベンチマークテストで優れた成績を収め、文法チェック通過率は88.06％、整合性チェック通過率は72.37％（8点満点）でした。特に注目すべきは、対手の四分の一のパラメータ量で、ReForm-32BやGoedel-Formalizer-V2-32Bなどの大規模モデルを逆転したことです。特に難しいFATE-HおよびFATE-Xサブセットにおいて、整合性チェック成功率はそれぞれ63％および37％に達し、最強の専門ベンチマークに対してそれぞれ10ポイントおよび12ポイント高いことを示しており、非常に強い推論と形式化エラー修正能力を示しています。

プロジェクトのアドレス: https://github.com/openbmb/MathForm