MathForm、検索と検証で数学の自動形式化を反復改善

導入

「任意の実数について」といった数学の文章を Lean 4 で表現する作業は、単純な翻訳ではない。モデルは Mathlib に存在する複雑な型、定義、既存の形式化を見つけ、適切に組み合わせなければならない。同時に、生成された命題が自然言語の元の意味を保っているかも確認する必要がある。MathForm は、この知識検索と検証を含む一連の問題に取り組むフレームワークである。

仕組みの要点

従来のパイプラインは、モデル内部のライブラリ知識に大きく依存し、1回だけ生成した結果をフィルタリングすることが多かった。コンパイルに成功したかどうかは重要だが、それだけでは定義の選択ミスや意味のずれを十分に検出できない。MathForm は次のような反復ループを導入する。

• 生成前の検索：検索プランナーが Mathlib から関連する定義、型情報、既存の形式化を集め、生成器に与える。
• 診断を使った修正：生成された Lean 4 の文をコンパイルし、コンパイラの診断情報を次の修正に利用する。
• 意味的一貫性の確認：コードが通るかだけでなく、形式化された命題が元の自然言語の内容を保っているかを評価する。
• 検証済みデータへの変換：修正と検証を経た例を FormalVerse にまとめる。

研究チームによれば、FormalVerse には複数の数学分野と情報源から集めた約 367K 件の検証済み Lean 4 例が含まれる。このデータを使い、教師ありファインチューニングの後に強化学習を行って MathForm-8B を訓練した。

結果と意義

6つのベンチマークにおける平均 Pass@8 は、Syntax Check で 88.06%、Consistency Check で 72.37% だった。論文では、複数の専用 32B 自動形式化モデルを上回ったとしている。難度の高い FATE-H と FATE-X では、Consistency Check の通過率がそれぞれ 63% と 37% となり、両方で最も強い専用ベースラインを超えた。

重要なのは、モデルサイズだけで結果を説明するのではなく、ライブラリ知識の取得、コンパイル可能なコードの生成、命題の意味の保持を一つの流れとして扱っている点だ。形式数学では、コンパイル成功は必要条件であって十分条件ではない。証明支援系が受理できる形でも、元の主張を正確に表していなければ、忠実な形式化とは言いにくい。検索と反復修正は、この差を縮めるための実装上の方向性を示している。

提供された素材には、詳細な実験条件、比較モデルの設定、意味評価の手順までは含まれていない。そのため、数値の解釈には論文全文の確認が必要である。一方、コード、モデル、データセットが公開されていることは、再現実験や後続研究への入口になる。MathForm は、モデルの記憶だけに頼らず、形式ライブラリと検証器の制約の中で数学データを改善するアプローチを示した。

出典：Hugging Face Daily Papers