OpenBMBは数学の自動形式化パイプライン「MathForm」一式をオープンソース化した。8Bモデルの重み、検証済みのLean 4データセット約36.7万件、評価コードとPass@kスクリプトをまとめて公開している。モデルはHugging Faceに置かれ、ライセンスはApache 2.0、ベースモデルはQwen3-8B、重みの精度はBF16。プロジェクトは清華大学自然言語処理研究室と面壁智能(ModelBest)が共同で支援するOpenBMBチームが手がけ、同名の論文が今月中旬にarXivへ投稿された。著者は計10名。
自動形式化とは、自然言語で書かれた数学の命題をLean 4のような機械検証可能な形式言語に翻訳する作業を指す。難しいのは字面の翻訳ではない。Mathlibの型階層と定義体系は極めて巨大で、命題中の『連続関数』や『有限群』といった語を、ライブラリ内の対応する定義に正確に落とし込みつつ、形式化後の命題が元の命題と同じ意味を保っている必要がある。どちらか一方でもずれれば、コンパイラはそれでも通してしまうことがある。
データはどう作られたか
MathFormのパイプラインは4段階からなる。まずプランナーが命題中の数学概念についてMathlibを検索し、検索ツールのLeanExploreが毎回上位22件の結果を返す。モデルはこの検索結果を条件としてLean 4の命題を生成する。候補は形式チェックとコンパイルテストを順に通過し、さらに大規模モデルによる意味的整合性の判定を経る。合格した経路は逆にたどってクリーンな学習トラジェクトリに再構成される。
論文中のある数字が反復の必要性を物語っている。後続ラウンドが、保持された全サンプルのうち追加で31.0%を占めた。つまり1回きりの生成で不合格をすべて捨てていたら、使えるデータの3分の1近くを失っていたことになる。
検索の導入は、この設計の中で最もコストを抑えている部分だ。モデルに記憶だけでMathlib内のある定義の正確な名前とシグネチャを思い出させることは、実質的には常に更新され続けるライブラリをどれだけ暗記しているかを試しているに等しい。ライブラリの参照を検索ツールに任せ、モデルには組み立てだけを担わせれば、必要なパラメータ数は自然と下がる。8Bが32Bと渡り合える理由もここにある——両者はそもそも同じ課題を解いているわけではない。
生成されたデータセットは「FormalVerse」と名付けられ、検証済みサンプルは約36.7万件。出典はDeepTheorem、NuminaMath、AceReason-Math、Lean Workbook、Principia-Collection、DeepMath、OpenR1-Mathにまたがり、さらに定番教科書の内容も加えられている。このデータセットはHugging Faceですでに358件の「いいね」を集めている。
成績表と2つの見方
学習は教師ありファインチューニングの後に強化学習を行う構成。評価は6つのベンチマークにわたり、FormalMATH-LiteとDeepSeek-ProverBenchは競技数学、CombiBenchは組み合わせ数学、FATEシリーズは代数の難易度別にM・H・Xの3段階に分かれる。
MathForm-8Bは構文チェックの平均Pass@8が88.06%、一致性チェックの平均が72.37%。FATEの3段階での一致性通過率はM・H・Xの順に97.33%、63.00%、37.00%だった。比較対象にはHerald Translator-7B、Kimina-Autoformalizer-7B、Mathesis-HPO-7Bのほか、StepFun-Formalizer、Goedel-Formalizer-V2、ReFormそれぞれの7B/8B版と32B版が含まれる。8Bは複数のテストセットで32B専用形式化モデルの成績を上回った。
この2つの指標の差は、絶対スコアそのものより多くを語る。構文チェックはコンパイルが通るかどうかしか見ていないが、一致性チェックは形式化後の命題が元の問題と同じ意味かどうかを問う。88%と72%、その差の十数ポイントこそが、このパイプラインが今抱える本当のボトルネックだ。コンパイルが通ることと、証明したかった定理そのものであることは別の話になる。
ハードルはワークステーション1台まで下がった
本サイトは先日、テレンス・タオが発した『AIが生成する証明は誰も読み切れない量になる』という警告を取り上げた。形式化はその問いに対するもう半分の答えだ——証明がLeanのコンパイラを通りさえすれば、人間が読んで理解できるかどうかはもはや受け入れの前提ではなくなる。ただし前提として命題自体が正しく翻訳されている必要があり、FATE-Xでの37%という数字は、そこにまだ相当な距離が残っていることを示している。
ざっくり試算すると、8BモデルをBF16で読み込むにはおよそ16GBのVRAMが必要で、32Bの同精度モデルではおよそ64GB前後が必要になる。前者は24GBクラスのコンシューマー向けGPU1枚で動かせるが、後者は複数枚か業務用カードが要る。大学の数学科、証明支援ツールのコミュニティ、小規模チームにとって、形式化パイプラインを動かすためのハードルはクラスタ級から単一マシン級まで下がったことになる。データセットと評価スクリプトも同時に公開されているため、第三者による再現や検証のコストも合わせて下がっている。
比較表に並ぶ名前の顔ぶれも、この分野がどれだけ混み合っているかを物語る。Herald、Kimina、Mathesis、StepFun-Formalizer、Goedel-Formalizer-V2、ReForm——いずれもここ1、2年で登場した専用形式化モデルで、すべてオープンソースだ。形式化は一般的な対話モデルのように計算資源をつぎ込めば差がつく分野ではなく、勝負を分けるのはデータ構築の工夫と検証ループの完成度で、パラメータ規模はむしろ副次的な変数になっている。論文でのデモから実際にオープンソースとして届けられるまでのペースは、多くの人の予想より速い。
参考資料：OpenBMBのリポジトリとモデルカード、CocoLoop、arXivプレプリント2608.14221、Hugging Faceデータセットページ。パラメータ規模、ライセンス、FormalVerseのサンプル数、各ベンチマークのPass@8算出方法を確認済み。